HAssert aggregates

[0xGeorgii]

Closes #355

Confidence Score: 5/5

The PR appears safe to merge; no concrete changed-code defect remained after reviewing the aggregate, binder, codec, and Rocq contract paths.

The producer, shared IR and codec, Rocq printer and stub, and integration fixtures are updated consistently, with no reachable incorrect obligation or build failure established.

Important Files Changed

Filename	Overview
core/wasm-codegen/src/hassert/translate.rs	Implements aggregate leaf trees, access resolution, symbolic-index witnesses, quantifier alternation, diagnostics, and depth budgeting with extensive focused coverage.
core/hassert/src/ir.rs	Adds the explicit universal-quantifier assertion node and its simplifying constructor.
core/hassert/src/codec.rs	Adds the stable 0x0B universal-binder tag across validation, symbol collection, encoding, decoding, and depth-limit tests.
core/wasm-to-v/src/hassert_print.rs	Prints universal assertion nodes as the verifier's transparent Hall definition and includes them during symbol traversal.
core/wasm-to-v/rocq-stub/wasm_verifier/Assertions.v	Extends the vendored Rocq contract stub with the Hall definition used by generated obligations.
tests/src/rocq_typecheck.rs	Expands end-to-end Rocq elaboration coverage for aggregate obligations and quantifier alternation.
tests/src/hassert_translation.rs	Adds integration assertions for aggregate leaf ordering, indexing, comparisons, diagnostics, and binder structure.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart LR
  A["Typed specification AST"] --> B["Aggregate shape and scalar-leaf translation"]
  B --> C["HAssert IR<br/>Ex / All / guards / terms"]
  C --> D["inference.hspecs v2 codec"]
  D --> E["wasm-to-v hassert printer"]
  E --> F["Rocq ValidSpec obligation"]

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

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!