feat(l13): region-imports carrier — proposal 0003 accepted, codec + link-graph verifier + producer emission (#140)#198
Merged
Conversation
…ink-graph verifier + producer emission (#140) L13 positive form on emitted bytes: one module exports a region schema, others import subsets, and agreement is certified at link time — the examples/02 killer feature, previously spec-only (noSpoofing fired only in Idris2, never on wire). typed-wasm-verify (new `unstable-l13-imports` feature, implies l2): - section.rs: RegionImportEntry + parse/build for typedwasm.region-imports (u16le version, LEB128 lengths, UTF-8; expected fields reuse FieldEntry, scalar-only v1). 5 codec tests incl. UTF-8 + truncation-leniency sweeps. - verify.rs: verify_region_imports_from_module (dependent-regions presence, unique (producer,region) pairs, v1 pointer restriction, high-bit target_region FKs in import-table bounds; TARGET_REGION_IMPORT_BIT) + verify_link_graph (SchemaSub expected vs actual per import, subset semantics -> CompatCertificate per MultiModule.idr; full RegionImportsError taxonomy). - tests/link_graph.rs: 11 tests mirroring example-02's physics/ai/ render trio + every error variant. typed-wasm-codegen: - parser: `import region X from "mod" { fields }` -> expected-schema entries; repeated imports of one (producer, region) pair union-merge (a single .twasm file holds several conceptual modules); conflicting field types are a source error. Pointer-typed expected fields rejected (v1). - emit(): writes the carrier via the verifier's own encoder; always emits the dependent typedwasm.regions section alongside. - tests/example02.rs: 4 tests — union-merged import table, emitted carrier + self-link certificate, mutated-expectation rejection, absent-producer rejection. Docs: proposal 0003 draft->accepted (impl note: sibling-codec conventions); promoted to ADR-0007; LEVEL-STATUS L13 positive form -> YES (import-bound); spec carrier table + target_region v1.1 high-bit note; codegen README; parser header rewritten per ADR-0006 (was still "stopgap until AffineScript front-end"). Cross-repo adoption issue drafts in docs/developer/cross-repo-issues-proposal-0003-adoption.adoc (automated filing permission-blocked). Workspace: 162 tests, 0 failures. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Increment 1 of 3 on the independence construction path (owner-ratified sequence).
Closes the L13 positive-form gap:
typedwasm.region-importsnow exists end-to-end — codec + module-local pass +verify_link_graphcross-moduleSchemaSubcertification intyped-wasm-verify(behindunstable-l13-imports), and producer emission from real.twasmsource (import region Entity from "physics" { … }) intyped-wasm-codegen. The examples/02 killer feature — one module exports a schema, others import subsets, agreement certified before anything runs — round-trips in-process for the first time.[draft]→[accepted](2026-07-07) → ADR-0007; wire format as specced (LEB128 + u16le version), with an implementation note pinning sibling-codec conventions.target_regionv1.1 high-bit value-space extension implemented (TARGET_REGION_IMPORT_BIT), non-breaking for v1 consumers.RegionImportsErrortaxonomy from the proposal's §Consumer obligations; 15 new L13 tests + 5 codec tests; 162 workspace tests, 0 failures.(producer, region)imports in one file (examples/02 holds three conceptual modules) — keeps the carrier's uniqueness obligation.docs/developer/cross-repo-issues-proposal-0003-adoption.adoc(automated filing was permission-blocked — ready to paste).Part of #140 (remaining there: producer-emitted c5_real differential fixture pair; per-module split of multi-file sources).
🤖 Generated with Claude Code