Initialize native package environment before Scheme test imports

Justfile

@@ -46,7 +46,8 @@ test-file path pattern=".*":
     fi
     mkdir -p .data/test-logs
     log="$(mktemp .data/test-logs/test-XXXXXX)"
-    timeout --signal=TERM --kill-after=5s 120s {{ gerbil_darwin_env }} gerbil -:max-heap=2G,debug=q test -v 5 -r "{{pattern}}" "{{path}}" 2>&1 | tee "$log"
+    # Establish the native package environment before gxtest initializes imports.
+    timeout --signal=TERM --kill-after=5s 120s {{ gerbil_darwin_env }} gerbil -:max-heap=2G,debug=q env gxtest -v 5 -r "{{pattern}}" "{{path}}" 2>&1 | tee "$log"
     if rg 'ERROR (MODULE|CHECK|CASE|HARNESS)|Heap overflow|Stack overflow' "$log"; then exit 1; fi
     rg -F -x 'MODULE-OK {{path}}' "$log" >/dev/null
     rg -F 'HARNESS-OK' "$log" >/dev/null

docs/10-19-design/10-architecture/10.147-source-bound-c-and-cpp-contract-verification.org

@@ -10,24 +10,28 @@
 #+BEGIN_QUOTE
 The later [[file:10.148-flat-declarative-library-boundary.org][10.148 Library boundary]] supersedes this proposal's placement of source
 capture, process execution and evidence issuance. They are consumer/test duties,
-not a Runtime implemented by this Library. The contract obligations below remain
-design requirements, not executed proof claims.
+not a Runtime implemented by this Library. The general contract obligations remain
+requirements. The bounded C/C++ subjects and observed acceptance are identified
+explicitly below; they do not establish arbitrary-project correctness.
 #+END_QUOTE
 
 * Goal and decision boundary
 :PROPERTIES:
 :JD_ID: 10.147
 :CUSTOM_ID: source140-goal
-:STATUS: design-proposed-not-implemented
+:STATUS: bounded-real-source-qualified-cold-install-open
 :END:
 
 Extend the existing Library, POO and ASCENT architecture so that a domain
 obligation can be checked against actual C/C++ function bodies, their callers
 and the native artifact that uses them. The subject is reusable C/C++ engineering
 capability across projects, not an SMP integration project. SMP illustrates one
 possible application of capacity and resource-lifecycle contracts. This document
-defines the design and per-project implementation gates; it reports no executed
-C/C++ verification. Acquiring SMP source is not a prerequisite for this work.
+defines the reusable design and per-project implementation gates. Maintained C
+capacity/caller and C++ resource-lifetime subjects now have actual CBMC/native
+results and ASCENT integration controls. Other families and consuming projects
+still require their own captures and evidence. Acquiring SMP source is not a
+prerequisite for this work.
 
 #+BEGIN_QUOTE
 A checked model is not a checked implementation. A checked function under a
@@ -389,20 +393,22 @@ reasoning without inheriting unsupported implementation conclusions.
 
 | Gate | Completion condition | Current state |
 |------+----------------------+---------------|
-| G0 Source | The selected consuming project's actual functions/callers and full configuration captured | Required when verifying that implementation; no project selected here |
-| G1 Scope | Reviewed local contract, parent refinement, reachable-state assumptions and independent oracle | Designed; source-specific review pending |
-| G2 Static | Real-body checks, caller premises, nonvacuity controls and explicit completeness classification | Not implemented |
-| G3 Counter | Historical reproduction where available, fixed replay and negative controls for excluded failure/units | Not executed |
-| G4 Native | Same-source real build, artifact lineage, regression and propagation behavior | Not executed |
-| G5 Integration | Native POO selection, actual ASCENT registration/queries, invalidation and reuse controls | Not implemented |
-| G6 Review | Scoped closure of findings and required authorization under existing Aitia policy | Not executed |
+| G0 Source | Actual functions/callers, harnesses and declared configuration captured | Observed for maintained C bounded-capacity and C++ resource-lifetime subjects; no SMP or arbitrary consumer capture claimed |
+| G1 Scope | Local contract, parent refinement, reachable-state assumptions and independent oracle | Explicit for these subjects; C caller premises and C++ constructor/counter premises remain part of applicability |
+| G2 Static | Real-body checks, caller premises, nonvacuity controls and explicit completeness classification | Actual C body/contract/caller and C++ bounded checks pass; bounded solver results are not universal language proofs |
+| G3 Counter | Real negative controls for the selected failure semantics | Actual missing-overflow-guard and occupied-transfer source mutants produce counters; no historical SMP repair claimed |
+| G4 Native | Same-source build, artifact lineage and native regression | Actual C and C++ native artifacts execute successfully; full compiler backend/SDK attestation remains unsupported |
+| G5 Integration | Native POO selection, actual ASCENT registration/queries, invalidation and reuse | Eight real-source cases plus native language-owner controls pass; reuse shares an identical implementation capture, not unrelated code |
+| G6 External review | Consumer-required findings disposition and current-use authorization | Owned by the consuming ecosystem; Library support is not an Aitia approval or application permit |
+| G7 Package qualification | Native package identities, compiled ABI and complete cold dependency installation | Earlier local manifests/compiled consumers and root source build pass; subsequent ordinary Core/root deadline failures require requalification; full cold installation remains open |
 
 Implementation tests for Scheme integration belong in =t/*-test.ss=. Future
 verifier harnesses remain C/C++ assets. Preserve the established per-process
 2 GiB heap and 180-second acceptance budget for applicable Gerbil processes;
 derive concurrency from machine resources. Before any solver run, record a
 method-specific resource policy; a budget termination is pending, never proof.
-This design does not change existing budgets or claim a solver run occurred.
+These results do not change existing budgets. Their authority is limited to the
+actual maintained subjects, declared tool/method inputs and observed runs.
 
 The maintenance cost is contracts, environment models, tool qualification and
 representation mappings. A consuming project can begin with a critical boundary
@@ -421,22 +427,27 @@ defect detection and review effort before expanding a project's verified scope.
 - [X] Define historical counter retention, current applicability and reuse boundaries.
 - [X] Use existing Module, Profile, Scenario, Catalog and evidence/review owners.
 - [X] Separate generic C/C++ adoption from optional SMP illustration.
-- [ ] For a later selected consumer, capture its source before claiming implementation evidence.
-- [ ] Validate the proposed mapping with actual Yuanxu/ASCENT APIs and real results.
+- [X] Capture maintained C/C++ subjects before issuing their implementation evidence.
+- [X] Exercise native Yuanxu selection and actual ASCENT registration/query with real results.
+- [ ] Capture and qualify each additional consuming implementation before transferring a claim.
+- [ ] Complete cold dependency installation without treating incremental recovery as a cold pass.
 
 * Documentation verification
 :PROPERTIES:
 :CUSTOM_ID: source140-documentation-checks
 :END:
 
-The new Org document passes =org-lint= with no findings. Local file links,
+The original design revision passed =org-lint= with no findings. Local file links,
 English-only text, unique CUSTOM_ID values, eight SG gold rows and eight SC-R
 rule rows were checked. D2 was formatted and rendered with =--layout elk
 --theme 0 --pad 24=; the SVG was visually reviewed after simplifying long
 feedback edges. README and both indexes link the new design and view.
 
-These checks establish document structure and navigability only. All source,
-tool execution and integration gates above retain their stated pending status.
+Those historical checks establish document structure and navigability only.
+The current view is maintained by the repository's TypeScript rendering and
+source-receipt checks. Actual source/tool/integration results are qualified
+separately in the gate table and current real-source controls; rendering never
+promotes a pending package gate to acceptance.
 
 * Primary references
 :PROPERTIES:

docs/10-19-design/10-architecture/10.149-unified-language-engineering-configuration.org

@@ -186,3 +186,102 @@ ASCENT evidence and application authorization are not issued by these views.
 PNG export uses the existing lossless compression path. The separate raster
 comparison checks decoded PNG/WebP pixels against each source image; compressed
 output is not substituted beneath an unchanged image digest.
+
+** Native package startup and build-projection acceptance
+:PROPERTIES:
+:CUSTOM_ID: package-startup-projection
+:ENTRY_OWNER: Justfile::test-file
+:CONSUMER: t/project-formation-build-test.ss
+:END:
+
+The native test entry is =gerbil env gxtest=. Package environment selection must
+precede test-tool initialization. With this selected SDK/cohort, plain
+=gerbil test= failed while expanding Core's generated POO import, even after a
+native Core clean/rebuild. Establishing =GERBIL_PATH= before process startup
+removed that import failure; the maintained entry delegates that selection to
+Gerbil's =env= command rather than constructing another load path or resolver.
+The independent compiled POO consumer also imports successfully. This evidence
+does not establish a general POO export defect or a stale-product-only cause.
+
+The real compiled-root consumer checks the maintained formation Profile target,
+one canonical =(gxc: "config")= row, identical specification identity on repeated
+reads and refusal to change retained roots within one init epoch. Config is
+already selected through the Profile dependency graph; it must not also appear
+as a duplicate ordinary retained target. The separate native root source build
+passes; switching the consumer to its public compiled import does not substitute
+for that source build. The removed =profiles/library-formation= path is no longer
+an asserted product.
+
+All test markers and error scanning remain mandatory. The 120-second test fence,
+180-second build fence, per-process 2 GiB heap and machine-derived compiler
+concurrency are unchanged. A zero-exit incremental package build was insufficient
+to repair the startup failure and is not treated as consumer acceptance.
+
+A real native Core clean followed by a rebuild exceeded 180 seconds (exit 124).
+The subsequent incremental recovery completed and the root source build passed;
+neither result converts the failed cold rebuild into a pass. Complete cold
+dependency installation remains open. Remote Linux rendering failed during
+Chromium system-dependency installation with Ubuntu mirror DNS errors; macOS
+passed at 4f43d48. Those infrastructure observations do not qualify Linux tests.
+
+*** Cold-build measurement and control
+:PROPERTIES:
+:CUSTOM_ID: core-cold-measurement-control
+:END:
+
+The subsequent Core diagnostic build completed naturally in 127.41 seconds with
+=GERBIL_BUILD_VERBOSE=2=. Its native stage clocks place specification completion
+at 20.30 seconds, Make entry at 21.57 seconds and main return at 122.47 seconds.
+It generated 274 distinct Scheme targets and scheduled 587 Gambit compilation
+jobs; no repeated target-generation row was observed. This does not rule out
+repeated internal expansion or metadata work. A
+process observation found twelve =gsc= children, matching machine-derived
+concurrency; the single/dual-worker hypothesis is not supported for this run.
+
+The ordinary-entry control used native clean again. Before starting, an inventory
+found zero remaining Core =.ssi=, =.ssxi.ss=, dynamic objects or static Scheme
+products, including the off-prefix Yuanxu prelude. Prerequisite packages and the
+SDK remained installed; this is a Core-product cold control, not a fresh Parent
+dependency installation or an operating-system cache reset.
+
+That ordinary control did not pass: the 180-second timeout escalated after the
+unchanged five-second termination grace and the command ended with signal 9 at
+185.32 seconds. No natural completion marker was observed. The diagnostic pass
+therefore cannot establish ordinary cold-build acceptance. Instrumentation,
+scheduling, input order and host load remain candidate explanations; neither a
+GC diagnosis nor an accounting-based optimization has been established. The
+captured resource sample and job count do not justify a heap or worker change.
+
+The installed Core also differs from its current open upstream PR by 188
+commits, and that PR declares a different POO revision. The candidate must be
+qualified as a coherent native dependency set; upstream success cannot be
+transferred to the installed cohort. Package management remains the dependency
+owner. No isolated leaf pin, fabricated manifest or compatibility layer is used
+to hide this outstanding qualification.
+
+The observed native manifest chain is:
+
+#+NAME: native-cohort-upgrade-owners
+| Existing owner | Observed declaration | Upgrade obligation |
+|----------------+----------------------+--------------------|
+| Core PR 19 | A newer POO revision than the installed Core | Qualify the exact declared POO/Core pair |
+| Parser PR 23 | Still selects the installed older Core | Change its own declaration and qualify its native consumers before publishing a replacement revision |
+| ASCENT PR 1 | Still selects the same older Core | Qualify native rules/queries against the candidate Core before publishing its revision |
+| Orgize PR 18 | Selects the older Parser candidate | Consume the qualified Parser revision and exercise real generated parser build/consumer paths |
+| Parent PR 34 | Selects Parser, Orgize and ASCENT candidates | Compose their published compatible revisions through native package management |
+| This Library | Selects only Parent | Promote Parent only after native install, build, metadata and actual C/C++/ASCENT consumer gates |
+
+An open PR name is not a version-selection instruction. Each declaration belongs
+to its existing package owner; the root must not add a competing direct Core or
+POO pin. Parent's optional source Core gitlink is a separate source ownership
+declaration and must not silently replace the selected native package identity.
+The table records investigation and required validation, not completed upgrades.
+
+The instrumented incremental recovery subsequently completed, but the ordinary
+root source rebuild after recovery also exceeded its unchanged deadline. Earlier
+successful root/consumer results remain historical observations at the recorded
+baseline; they do not establish current whole-package acceptance after this
+control sequence. Requalification requires a naturally completed ordinary root
+build and its native metadata/consumer checks. The sampled shared host had load
+averages above thirty on twelve cores; this is relevant context, not proof that
+host contention alone caused the failures. No unrelated process was stopped.

docs/90-99-views/90-architecture-views/90.139-source-bound-c-and-cpp-contract-verification.d2

@@ -62,7 +62,7 @@ plans: "Scheme method declarations\nTyped verification plans; no execution"
 methods: "Development verification\nReal body + callers; bounded CBMC / native tests"
 math: "Lean / Quint correspondence\nNumeric lemmas / state-order assumptions"
 oracle: "Independent checks\nLiteral gold and actual source mutants\nOccupied refusal / self transfer"
-closure: "Captured evidence inputs\nSource, harness, tools, bounds and configuration\nSix retained real results; five full test cases"
+closure: "Captured evidence inputs\nSource, harness, tools, bounds and configuration\nEight real-source cases; independent native owner controls\nCold dependency installation remains unqualified"
 ascent: "ASCENT relations\nSupport, counter, pending and reuse premises"
 consumer: "External consuming ecosystem\nReview and current-use authorization"
 change: "Changed source or assumptions\nNew capture; retain old witnesses and frozen queries"