Aggregates, symbolic index and quantifier alternation in specification obligations (#355)

[0xGeorgii]

Closes #355.

Specification bodies can now state aggregate, element-wise and alternating-quantifier properties directly, instead of being rejected outright.

What changed

Aggregates as ordered scalar leaves. A compound @, a compound parameter, an array or struct literal, and a copy of one translate to a shape-preserving tree of scalar leaves — one universal slot with its own HA_has_type guard per leaf (one HA_ex binder per leaf existentially), arrays enumerated row-major and struct fields in layout order, allocated parameters-first-in-declaration-order then each @ in binding order. Field and constant-index access resolve against that tree at translation time, and aggregate ==/!= in assertion position is the leafwise conjunction or its De Morgan dual.

The supported surface is deliberately equal to the executable aggregate @ surface, since proof mode lowers spec bodies through the same unrolling: arrays of scalars at any rank, and structs whose fields are scalars or one-dimensional scalar arrays. Arrays of structs (A028) and structs with struct or multidimensional-array fields (A027) stay rejected on every specification path.

Symbolic index. An index the translation cannot fold binds a witness pinned by the unsigned range bound i <u N first, then one implication per element. Out of range that definition is unsatisfiable and the enclosing atom is refuted: a[i] denotes the element at index i, which exists — a definedness rule, not a mirror of any runtime check, since proof mode emits no bounds check at all. The alternative, a guarded implication leaving an out-of-range read vacuously satisfied, is what P010 rejects elsewhere. Constant steps of a chain descend first, so m[1][j] splits over the selected row; two non-constant steps in one chain are P002.

Quantifier alternation. A forall block inside an exists/assume block of a forall/plain spec function emits a real universal binder — new IR node HAssert::All, printed as wasm-verifier's derived Hall, carried on new inference.hspecs assert tag 0x0B, declared in the vendored stub. A free slot there would have been quantified by ValidSpec's outer universal, turning ∃k. ∀x. P into ∀x. ∃k. P silently — which is why P007 is lifted only for that nesting and kept inside exists/unique bodies, where every @ is a hidden choice parameter the judgment quantifies operationally.

Two new fatal diagnostics. P013, a per-spec-function running budget of 64 quantified scalar leaves, checked from the declared type before any leaf is materialized (levels accumulate across introductions, so a per-introduction cap would not bound the shared assertion-depth budget). P014, a constant-folded out-of-bounds index (const K: i32 = 5; a[K], a[1 + 4]), stating the same fact A037 states for a direct-literal index at the spellings A037's pattern cannot see.

Diagnostics reworded now that the encoding makes several of them inaccurate — P004's blanket tail at all eight sites, P003's schedule-sounding wording for a permanent rule, loop lifted out of the shared no-encoding template to name the quantifier idiom, and the reach-mode P007/P008/P004 messages naming the quantifier that makes the construct impossible.

Verification

Every obligation of all three new corpus fixtures was proved Qed against real wasm-verifier before the goldens were committed — 19 obligations plus the emitted ValidModule/ValidSpec theorems, zero Admitted, with neutralization runs confirming each green is live. The proofs are staged in a companion wasm-verifier PR.

That is how the bounded-iteration fixture's first draft was caught: it emitted a false obligation — an index constrained only from above, refutable at i = -1, since the emitted range bound is unsigned while a signed source comparison is not its complement — and was rewritten rather than shipped as the documented example of the encoding. The coqc gate cannot catch this class of defect on its own, because it rewrites Qed to Admitted and so only elaborates statements.

One usability trap is inherent to the definedness rule and is documented rather than diagnosed: a signed index needs both 0 <= i and i < N before its element denotes at all, and those bounds are necessary rather than sufficient — a claim about the element's value still needs hypotheses about that value. A u32 index needs no lower bound and yields a simpler obligation.

Compatibility

Every committed .v golden is byte-identical, as is every proof-mode .wasm (the pass is read-only over the typed AST), and compile mode has no obligations. No previously emitted obligation shape changes, so no downstream proof needs restating. HSPECS_SECTION_VERSION stays 2: the new tag is additive, an older decoder fails loudly with UnknownHassertTag(0x0B), and recompilation rather than migration is the compatibility story. Programs that compiled still compile; programs that were rejected may now translate.

cargo test --no-fail-fast: 5838 passed, 0 failed, 51 suites.

Confidence Score: 5/5

The PR appears safe to merge; no concrete changed-code failure remains after checking the new producer, codec, printer, verifier-stub, and test paths together.

The aggregate ordering and type guards remain aligned with executable layout, symbolic indexes are constrained to defined scalar elements, and nested universal guards remain scoped inside their corresponding binders.

Important Files Changed

Filename	Overview
core/wasm-codegen/src/hassert/translate.rs	Implements aggregate values, symbolic access witnesses, cumulative leaf accounting, and alternating-quantifier translation with coordinated guard and binder scopes.
core/hassert/src/codec.rs	Adds the append-only All wire tag and consistently includes it in encoding, decoding, validation, depth checks, and symbol traversal.
core/hassert/src/ir.rs	Adds the explicit universal assertion node and its trivial-body smart-constructor simplification.
core/wasm-to-v/src/hassert_print.rs	Prints the new universal assertion node as the verifier contract's Hall construct.
core/wasm-to-v/rocq-stub/wasm_verifier/Assertions.v	Extends the vendored Rocq contract stub with the universal assertion definition used by emitted obligations.
core/wasm-codegen/src/hassert/tests.rs	Adds focused coverage for aggregate ordering, symbolic indexing, diagnostics, guard placement, and mixed existential/universal binder indexing.
tests/src/rocq_typecheck.rs	Extends end-to-end Rocq elaboration coverage to the newly supported obligation forms and fixtures.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart LR
  A["Typed specification AST"] --> B["Aggregate shape and scalar-leaf translation"]
  B --> C["HAssert tree"]
  D["Symbolic index"] --> E["Range-bound existential witness"]
  E --> C
  F["Nested forall"] --> G["HAssert::All binder"]
  G --> C
  C --> H["inference.hspecs codec"]
  H --> I["wasm-to-v HAssert printer"]
  I --> J["Rocq obligation using Hall"]

Loading

_{Reviews (1): Last reviewed commit: "HAssert aggregates" | Re-trigger Greptile}

Context used (4)

• Knowledge Base — WASM Codegen and Linker
• Knowledge Base — WASM-to-V: Translating Compiled WASM into Rocq Proof Obligations
• Knowledge Base — hassert: The Verification-Obligation IR
• Knowledge Base — Test Suite: Integration Fixtures and Fuzzing

[0xGeorgii]

Closing as a duplicate: this content was already merged via #418 (squash-merged as 4052f7a). Opened in error because gh pr list --head lists only open PRs, so the already-merged #418 did not show up.