test: add fast-check fuzz oracle#3
Closed
hyperpolymath wants to merge 1 commit into
Closed
Conversation
|
You have reached your Codex usage limits for code reviews. You can see your limits in the Codex usage dashboard. |
hyperpolymath
added a commit
that referenced
this pull request
Apr 18, 2026
Three pre-existing infrastructure bugs diagnosed and addressed: 1. Directory case-mismatch: `layout/` renamed to `Layout/` so the filesystem path matches the `Layout.*` module names declared inside each file. On case-sensitive Linux the original `layout/` could not be resolved for `import Layout.Types`. 2. Lowercase import typo: `TypedWasm/ABI/Layout.idr` had `import layout.Types` (lowercase) — corrected to `import Layout.Types`. 3. Layout.Types parser + Refl-reduction issues: investigated `varInjective` parser error and the cascade of issues behind it (mutual recursion not declared between `WasmHeapType`/`WasmValType`, missing `public export` visibility, missing `Decidable.Equality` / `Data.List` imports, nested-`with` pattern-unification failures in the `DecEq` instance, Refl-impossible proofs that require layout values to reduce at unification time but do not under this Idris2 0.8 build). These are non-trivial to fix and are documented as future work in PROOF-NEEDS.md. Until #3 is resolved, the four `Layout.*` modules are commented out of `typed-wasm.ipkg` and the `import TypedWasm.ABI.Layout` line in `TypedWasm.ABI.Proofs` is gated. This unblocks the full ipkg build for the typed-wasm core (TypedWasm.ABI.* — the primary purpose of this repo). The aggregate-library Layout contracts remain in the tree for restoration once Layout.Types is fixed per the remediation plan in PROOF-NEEDS.md. Verified: `idris2 --build typed-wasm.ipkg` completes with exit 0 (silent success). The previous behaviour was `Module Layout.Types not found` failing the build at module 11/16. Note: ipkg build requires `idris2 --build` (not `--check`) to parse the package file properly — `--check` treats the file as Idris2 source. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
5 tasks
hyperpolymath
added a commit
that referenced
this pull request
May 30, 2026
…ss-module) (#112) ## Summary Closes [#95](#95 third acceptance bullet ("if [draft] proposal 0003 is authored, it tracks back here"). Closes the **latent seam** flagged in proposal 0001 §"Open questions" #5 (cross-module region foreign keys) and the symmetric gap noted in proposal 0002 §"Open questions" #3. ## What 0003 specifies A third producer-neutral carrier (slotting between 0001's regions/capabilities and 0002's access-sites): - **`typedwasm.region-imports`** carries per-module table of imported regions: source module name, region name, expected schema (for cross-module schema-agreement verification). - **Companion non-breaking extension to `typedwasm.regions`**: `target_region` foreign keys gain a high-bit convention for import-table indices: - `0x00000000..0x7FFFFFFE` — local region index - `0x80000000..0xFFFFFFFE` — imported region (index = value - `0x80000000`) - `0xFFFFFFFF` — `Scalar` sentinel (unchanged) v1 typedwasm.regions consumers see "region_id out of range" on high-bit values and recover via lenient codec; v1.1 consumers interpret the high bit as import-table indicator. **No wire breaking change.** ## Wire format Mirrors 0001/0002/0004 conventions (LEB128 per field, UTF-8 strings, lenient on truncation): ``` u16le version (= 1) u32le_leb128 import_count for each import: u32le_leb128 producer_module_name_len u8[] producer_module_name (wasm module name) u32le_leb128 region_name_len u8[] region_name (exported region name) u32le_leb128 expected_field_count for each expected field: u32le_leb128 field_name_len u8[] field_name u8 kind (FieldKind: Scalar only in v1) u8 wasm_ty (same enum as regions) u8 nullability u32le_leb128 cardinality ``` ## Section structure | Section | Coverage | |---------|----------| | Context | L13 cross-module gap in 0001, `MultiModule.idr` spec already covers it, latent-seam framing | | Proposal | high-bit `target_region` extension; wire format; spec-type mapping; versioning; producer/consumer obligations; coordination | | Producer obligations | 6 items (companion regions section mandatory, high-bit convention, wasm-module-name matching, omit-if-empty, no-pointer-fields-in-v1, only-real-imports) | | Consumer obligations | `verify_region_imports_from_module` pass + 7 error variants (`MissingDependentRegions`, `DuplicateImport`, `UnresolvedProducerModule`, `UnresolvedExportedRegion`, `SchemaImportMismatch`, `ImportTargetOutOfRange`, `PointerInImportNotSupportedInV1`) | | Alternatives considered | B extend-regions (rejected — conflates concerns); C component-model (deferred); D wasm-imports (rejected — confuses linkers); E string-table (deferred to v2) | | Open questions | (1) pointer-typed expected fields (deferred); (2) cross-module access sites — recommend folding 0002 §OQ3 in; (3) cross-module capability grants (0004 §OQ4 — may differ); (4) link-time vs verify-time (default: separate `verify_link_graph` pass); (5) producer module name normalisation (NFC deferred); (6) empty import table semantics | | Acceptance criteria | 6 gates mirroring 0001/0002/0004 | ## Spec-side mapping Realises `MultiModule.idr`'s: | Idris2 type | Wire realisation | |------------|------------------| | `ImportedRegion.source` (line 54) | `producer_module_name` | | `ImportedRegion.regionName` (line 56) | `region_name` | | `ImportedRegion.expectedSchema` (line 57) | per-field table | | `SchemaSub` (line 249) | verifier reconstructs from wire + producer's regions | | `ModuleCompat from to imp exp` (line 318) | verifier output (one per resolved import) | | `noSpoofing` (line 374, flagship) | the L13 property the verifier realises on emitted bytes | | `CompatCertificate` (line 142) | verifier-emitted per resolved import | | `SchemaMismatch` (line 185) | `SchemaImportMismatch` error variant | ## Why `[draft]` not `[review]` Neither producer can emit `typedwasm.region-imports` today: - **AffineScript** — `lib/tw_interface.ml` has cross-module verification scaffolding for L10/L13 boundary (reads `typedwasm.ownership` cross-module), but Roadmap C3 (multi-module region emission) is the prerequisite. - **Ephapax** — cross-module region emission isn't on the roadmap yet; `src/ephapax-wasm/` is single-module. ## README update Adds 0003 entry to `docs/proposals/README.adoc`'s "Current proposals" table; removes the "Proposal 0003 ... reserved" note (now occupied). ## Test plan - [x] AsciiDoc renders cleanly (cols-tables, code-blocks, cross-refs). - [x] Cross-references resolve (`MultiModule.idr` line numbers; sibling proposal links; tracker issue links). - [x] Rebased onto `main` after PR #111 merge (no conflicts). - [x] No code changes — no Cargo build required. - [ ] Reviewer cross-check: confirm the high-bit `target_region` convention doesn't break any v1 consumer (existing tests). ## Related - #95 (tracker — this PR closes the [draft] acceptance bullet) - #34 (proposal 0001 umbrella) - #106 (acceptance roadmap tracker for 0001/0002) - PR #76 (proposal 0001 — source of the deferral) - PR #37 (L13 single-module isolation — positive companion is 0003's cross-module) - PR #111 (proposal 0004 draft — sibling cross-module question for capabilities) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <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.
Summary
Changes
RSR Quality Checklist
Required
just testor equivalent)just fmtor equivalent)unsafeblocks without// SAFETY:commentsbelieve_me,unsafeCoerce,Obj.magic,Admitted,sorry).envfiles includedAs Applicable
.machine_readable/STATE.a2mlupdated (if project state changed).machine_readable/ECOSYSTEM.a2mlupdated (if integrations changed).machine_readable/META.a2mlupdated (if architectural decisions changed)TOPOLOGY.mdupdated (if architecture changed)CHANGELOGor release notes updatedsrc/interface/abi/andsrc/interface/ffi/consistent)Testing
Screenshots