Implement extension resolution and lowering

[alexlopashev]

Closes #110

Outcome

• resolves derived extension descriptors to concrete total-pure BHCP meta lowerers and removes descriptor/lowerer presentation after checked core lowering
• retains supported native extensions as sorted unique must-understand semantic-IR nodes with exact descriptor, schema registration, deterministic payload, inspection, and identity
• rejects missing or invalid lowerers, reducer declaration/specialization/bound mismatches, mixed modes, unsupported/schema-mismatched native extensions, policy/core overrides, non-record composition calls, and malformed or tampered retained nodes before planning
• advertises the implemented extension feature and updates README, VISION, SEMANTICS, conformance, feature-manifest, and hosted-test coverage

Red to green

Initial focused development started with missing extension APIs and retained nodes. Dedicated meta/reducer evaluators made the initial implementation green.

The first independent review found two coverage gaps. Regressions failed because concrete reducer declarations were silently retyped during specialization and because retained native payload envelopes were not structurally revalidated. Signature unification and closed envelope/descriptor agreement checks made both regressions green.

The second exact-head rereview confirmed those fixes and found two adjacent fail-open boundaries. New regressions proved a generic reducer bound such as I: Text was ignored when specialized with I = Unit, and a retained node plus agreeing descriptor could be forged to a reserved bhcp/ core symbol. Specialization now checks every inferred argument against its substituted declared bound using project refinement relations, with a satisfied-bound positive control. Retained validation independently rejects reserved core extension symbols even when descriptor and node agree.

Focused evidence on exact head 795f10ce12cb63c91e46d08963e0df55ce90551c:

• cargo test --test extension_lowering: 10 passed
• cargo test --test graph_model: 13 passed
• includes the checked-in conformance/v0/reference-program/extension.bhcp
• includes reducer input/observation/result mismatch, generic bound rejection and acceptance, source-order/identity, must-understand, duplicate/malformed/tampered IR, descriptor disagreement, reserved-core retained forgery, mixed-mode, policy/core override, unsupported/schema mismatch, and stable-diagnostic cases

Full validation

Exact head 795f10ce12cb63c91e46d08963e0df55ce90551c, based on current main, passed:

• cargo fmt --check
• cargo clippy --all-targets -- -D warnings
• cargo test --all-targets
• cargo build --release
• cargo test --test schema_fixtures

Documentation impact

Updated the normative implementation note in SEMANTICS.md, public maturity statements in README.md and VISION.md, executable conformance evidence, the example feature manifest, native inspection output, and the CI test plan. Reconciliation retained the graph-model feature and test shard added by #113.

Residual risk

Native support remains deliberately closed and process-local: a host registration supplies a deterministic payload and the exact content-reference schema claimed by the descriptor. This slice does not fetch or execute arbitrary native schema/rule artifacts, and no unknown or core-overriding native node reaches planning. Obligation/capability/state graph construction beyond the shared model and runtime interpretation remain with assigned downstream issues.

Review head

795f10ce12cb63c91e46d08963e0df55ce90551c

[alexlopashev]

BLOCKING CHANGES REQUESTED — GitHub cannot attach the formal CHANGES_REQUESTED state because this independent task shares the PR author account (Review Can not request changes on your own pull request).

Independent review by Codex task /root at exact head 39719a9e450c547eef39edd610122f4d672068de.

The ordinary focused suite (9/9), the complete canonical local gate, and every hosted check pass, but two reviewer-only adversarial tests fail:

1. [P1] Validate the source reducer signature before specialization (src/prelude.rs, Prelude::reducer; src/pipeline.rs, instantiate_reducer). Prelude::reducer checks only arity and that the result is some Reduction<_>, then instantiate_reducer discards the declared parameter/result types and constructs new ones from the extension specialization. Reproduction: change the test reducer declaration from parent: Unit to parent: Text; compile_source still succeeds and emits a reducer whose parent is Unit. This silently retypes an ill-declared function instead of checking the S8.2 network shape and checked-core boundary. Require exact/conforming declared parameter and result types (including supported generic substitution) before instantiation, and add the failing mismatch cases.

2. [P1] Validate the retained native descriptor/payload envelope (src/model.rs, SemanticIrDocument::validate). The validator currently checks only node ID, symbol, must_understand, uniqueness, ordering, and deterministic encoding. Reproduction: compile the supported native fixture, replace extensions[0].payload wholesale with Value::Text("forged"), and ir.validate() still returns Ok(()). That permits descriptor/version/schema/rule identity to be removed from a must-understand retained node, contrary to S9.3, EXT-02, and this issue’s tampered-retained-node acceptance claim. Require the retained envelope shape, validate its descriptor as a native extension descriptor, require descriptor symbol/mode/must-understand to agree with the node, and retain a permanent adversarial test.

No author-branch edits were made; the detached review worktree was restored clean to the exact head after reproduction. This is a blocking review and the PR was not merged.

[alexlopashev]

Author update for the blocking independent review on prior head 39719a9e450c547eef39edd610122f4d672068de:

• Added a red-to-green regression that changes each declared reducer boundary independently: parent input, observations, and Reduction<O> result. Specialization now unifies declared types and generic parameters against the concrete specialization before constructing bindings.
• Added red-to-green retained-native regressions for a forged whole payload, descriptor symbol disagreement, and an extra envelope field. Semantic IR validation now requires the exact {descriptor, value} envelope, validates the native descriptor schema, and checks symbol/kind/must-understand agreement with the node.
• Reconciled onto current main after Implement shared typed graph identities, validation, and deterministic encoding #113/PR Implement shared typed graph identities, validation, and deterministic encoding #144 merged, preserving its graph-model CI and feature-manifest entries.

Focused: extension 10/10 and graph model 13/13. Full canonical local gate passed. New exact review head: 4d145aa1941868163aad9709bc7ba1b6bc65e795.

Retained claim refs remain unchanged:

• refs/heads/codex-locks/issues/110 at c8dff863f56259f1b903080363e0f167ddfaf766
• refs/heads/codex-locks/mutex/semantic-contract at 45cb02ce43fabca7dbe0957904aafa471bbfb906

No self-review or merge.

[alexlopashev]

BLOCKING CHANGES REQUESTED (rereview) — GitHub cannot attach a formal CHANGES_REQUESTED state because this independent task shares the PR author account.

Independent rereview by Codex task /root at exact head 4d145aa1941868163aad9709bc7ba1b6bc65e795. The two prior P1 regressions are fixed, the focused extension suite is 10/10, graph model is 13/13, the complete canonical local gate passes, and every hosted check is green. Two adjacent reviewer-only adversarial tests still fail:

1. [P1] Enforce generic reducer bounds during specialization (src/pipeline.rs, reducer_signature_matches). The matcher unifies declared type parameters with concrete BhcpTypes but never consults source.type_parameter_bounds. Reproduction: make the reducer generic as <I: Text, O: Dynamic, Observations: Dynamic>, declare parent: I, and specialize the extension at Unit; compile_source succeeds even though I = Unit violates the declared Text bound. This bypasses the ordinary generic type checker and makes the dedicated reducer path accept an invalid monomorphization. Validate substitutions against every declared bound (using the existing type relations/substitution machinery where possible) and retain a regression.

2. [P1] Reject reserved-core symbols in retained native IR (src/model.rs, SemanticIrDocument::validate). The new envelope validator proves descriptor/node agreement but accepts any syntactically valid symbol. Reproduction: change a valid retained native node and its descriptor symbol together to bhcp/prelude.all@0; ir.validate() returns Ok(()). Source lowering rejects bhcp/ extension symbols, but adversarial retained IR can still claim a core meaning, contrary to S9.3 and EXT-04. Apply the same reserved-core namespace rule at the retained IR boundary and retain a consistent descriptor/node tampering regression.

The detached worktree was restored clean to the exact head. No author-worktree edits were made. PR not merged; issue and semantic-contract refs remain untouched.

[alexlopashev]

Author update for the second blocking rereview of prior head 4d145aa1941868163aad9709bc7ba1b6bc65e795:

• Added a red-to-green generic-bound regression: a reducer declared with I: Text no longer specializes with I = Unit. Specialization now substitutes all inferred generic arguments, requires every parameter to resolve, and checks each non-dynamic bound using the project type-refinement relations. A matching I: Unit positive control remains green.
• Added a red-to-green retained-IR regression where both the native node and its descriptor are changed consistently to bhcp/prelude.all@0. Semantic IR now independently rejects every retained extension in the reserved bhcp/ namespace.

Focused: extension 10/10 and graph model 13/13. Full canonical local gate passed. New exact review head: 795f10ce12cb63c91e46d08963e0df55ce90551c.

Retained claim refs remain unchanged:

• refs/heads/codex-locks/issues/110 at c8dff863f56259f1b903080363e0f167ddfaf766
• refs/heads/codex-locks/mutex/semantic-contract at 45cb02ce43fabca7dbe0957904aafa471bbfb906

No self-review or merge.

[alexlopashev]

INDEPENDENT APPROVAL

Codex reviewer task /root rereviewed exact head 795f10ce12cb63c91e46d08963e0df55ce90551c. The four prior blocking P1 findings are closed with permanent red-to-green coverage. Generic reducer substitutions now enforce declared bounds through project refinement relations, including a satisfied-bound control; retained native validation independently rejects reserved bhcp/ symbols while preserving descriptor/node agreement checks.

No actionable findings remain after adversarial closure review against S8.2/KRN-12, S9.3, EXT-01..04, retained/native IR, identity, schema, documentation, and workflow. Reproduced evidence: extension_lowering 10/10, graph_model 13/13, the complete canonical local gate, and every hosted check pass on the unchanged exact head. The detached review worktree is clean and the author worktree was not edited.

GitHub cannot attach a formal APPROVED state because this independent task shares the PR author account; this COMMENTED review records the distinct reviewer task and exact approved head.