From 9919c270092ea77a633af5fc70d5531242ed8096 Mon Sep 17 00:00:00 2001 From: 0xGeorgii Date: Mon, 17 Aug 2026 08:19:36 +0900 Subject: [PATCH] HAssert aggregates Closes #355 --- CHANGELOG.md | 5 + core/hassert/README.md | 10 +- core/hassert/src/codec.rs | 76 +- core/hassert/src/ir.rs | 46 +- core/hassert/src/lib.rs | 16 +- core/wasm-codegen/README.md | 18 +- .../docs/specification-obligations.md | 303 +++ core/wasm-codegen/src/hassert/diag.rs | 79 +- core/wasm-codegen/src/hassert/mod.rs | 15 + core/wasm-codegen/src/hassert/tests.rs | 1834 ++++++++++++- core/wasm-codegen/src/hassert/translate.rs | 2260 +++++++++++++++-- core/wasm-to-v/ROCQ_CONTRACT.md | 80 +- core/wasm-to-v/rocq-stub/README.md | 61 +- .../rocq-stub/wasm_verifier/Assertions.v | 12 +- core/wasm-to-v/src/hassert_print.rs | 10 +- tests/src/codegen/wasm/multi_file.rs | 16 +- tests/src/hassert_translation.rs | 281 ++ tests/src/rocq_typecheck.rs | 242 +- tests/src/spec_propagation.rs | 43 +- tests/test_data/inf/spec_aggregate_values.inf | 61 + .../test_data/inf/spec_bounded_iteration.inf | 75 + .../inf/spec_quantifier_alternation.inf | 118 + tests/test_data/rocq/spec_aggregate_values.v | 104 + tests/test_data/rocq/spec_bounded_iteration.v | 87 + .../rocq/spec_quantifier_alternation.v | 115 + 25 files changed, 5593 insertions(+), 374 deletions(-) create mode 100644 core/wasm-codegen/docs/specification-obligations.md create mode 100644 tests/test_data/inf/spec_aggregate_values.inf create mode 100644 tests/test_data/inf/spec_bounded_iteration.inf create mode 100644 tests/test_data/inf/spec_quantifier_alternation.inf create mode 100644 tests/test_data/rocq/spec_aggregate_values.v create mode 100644 tests/test_data/rocq/spec_bounded_iteration.v create mode 100644 tests/test_data/rocq/spec_quantifier_alternation.v diff --git a/CHANGELOG.md b/CHANGELOG.md index 4f6dfc5f..7fe57005 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -180,6 +180,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 ### Rocq Translation +- Specifications can now state aggregate, element-wise and alternating-quantifier properties directly, instead of being rejected outright. A compound `@`, a compound parameter, an array or struct literal, and a copy of one are translated 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 in an existential context), enumerated arrays row-major and struct fields in layout order, allocated parameters-first-in-declaration-order then each `@` in binding order. So `let a: [i32; 3] = @; assert(a[0] <= a[0]);` produces a real obligation where it was **P008**, `a[0]` and `p.x` resolve against that tree at translation time where they were **P002**, and aggregate `==`/`!=` in assertion position is the leafwise conjunction (or its De Morgan dual) — `==` compares values, and an aggregate's value is exactly its ordered leaves. 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 — `@`, parameters and literals alike — so neither surface is wider than the other. An index the translation cannot fold binds a witness pinned by the unsigned range bound `i