Inferara · 0xGeorgii · Aug 16, 2026
diff --git 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 <u N` **first**, then one implication per element, which is what makes bounded iteration expressible: a `forall` binding an array and an index, assuming a bound on every element and a range for the index, and asserting the bound at that index emits a real obligation that discharges against the verifier (`tests/test_data/inf/spec_bounded_iteration.inf`). 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 rather than 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 exactly what **P010** rejects elsewhere. Constant steps of a chain descend first, so `m[1][j]` splits over the selected row, while two non-constant steps in one chain are **P002**. A `forall` block inside an `exists`/`assume` block of a `forall`/plain spec function now 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` (section version stays **2**: the change is additive, an older decoder fails loudly with `UnknownHassertTag(0x0B)`, the linker decodes hspecs only from the main module, and recompilation rather than migration is the compatibility story) and declared in the vendored `coqc` 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`-quantified bodies, where every `@` is a hidden choice parameter the judgment quantifies operationally. Two new fatal diagnostics come with the encoding: **P013**, a per-spec-function running budget of 64 quantified scalar leaves (each leaf costs a binder level and a guard level, and the levels accumulate across every introduction in the function, so a per-introduction cap would not bound the shared assertion-depth budget; checked from the declared type before any leaf is materialized), and **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. One usability trap is inherent to the definedness rule and is documented rather than diagnosed: the emitted range bound is unsigned, so a *signed* index needs both `0 <= i` and `i < N` before its element denotes at all — supplying only the upper bound compiles clean and yields an obligation that is false, surfacing later as an unprovable Rocq goal. The two bounds are necessary, not sufficient: they make the element exist, while a claim about its *value* still needs hypotheses about the element's value, since a compound `@` states only the typing of its leaves. A `u32` index needs no lower bound and yields a simpler obligation. Unaffected: 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. Migration: none — programs that compiled still compile, and programs that were rejected may now translate ([#355])
 - A data byte with no `byte_scope` notation now reaches the emitted `.v` as `(encode 18%Zst)` instead of `(encode 18%Z)`, and a module carrying a data segment claims that key in its preamble with a second conditional line — `Local Delimit Scope Z_scope with Zst.`, next to the `Open Scope byte_scope.` it already emitted. `%Zst` is a private delimiting key for the same standard `Z_scope` the literal always lived in (a Rocq scope may carry several keys), so the term denotes exactly what it denoted before. It is claimed because the `Z` key is not reliably `Z_scope`'s: mathcomp's algebra library delimits its own `int_scope` with it (`ssrint.v`, alongside a `Number Notation` on `int`), so in any file whose `Import`/`Export` chain applies that `Delimit` the argument of `(encode 18%Z)` re-reads as mathcomp's `int` and stops elaborating against `encode : Z -> byte`. Two files can be that file — the emitted `.v` itself, should the backend build behind its preamble ever re-export mathcomp algebra, and a consumer that imports it and restates emitted data bytes in its own text. Delimiting is last-writer-wins — whichever `Delimit` the chain applies last decides the key; an explicit `%Z` is read through the key regardless of which scopes are open, so `Open Scope Z_scope.` recovers nothing, and nothing a consumer writes downstream repairs a file that failed to compile on its own. Re-delimiting is the one measure that works, and taking a private key rather than taking `Z` back leaves mathcomp's own `%Z` intact for anything read alongside the module, while `Local` keeps the key from leaking to consumers that import the file. Unaffected: the 244 byte values that have a notation keep their `#78` spelling, and every module without a data segment is byte-identical, preamble included — Inference codegen emits no data segment, so no committed `.v` golden or corpus output moves and only foreign or statically-linked `.wasm` reaches the changed spelling. A downstream file that restates emitted data bytes in its own text must carry the same `Local Delimit` line ([#416])
 - The emitted `Ma` memarg helper in every Rocq `.v` file now binds `ofs al` instead of `of al` (`Definition Ma ofs al := {|memarg_offset := ofs; memarg_align := al|}.`): `of` is an ordinary identifier in vanilla Rocq but a keyword under ssreflect, so a consumer importing mathcomp ahead of the emitted definitions hit a parse error on that preamble line before reaching anything the file states. `Ma` is always applied positionally (`Ma 0%N 2%N`), so no call site or downstream proof changes, and every emitted `.v` differs by exactly this one line ([#412])
 - `wasm-to-v` no longer drops a table import's element type. `translate_module_import_desc`'s `TypeRef::Table` arm applied the contract's `MID_table : table_type -> module_import_desc` to a bare `limits` record instead of the two-field `table_type` (`{|tt_limits; tt_elem_type|}`) the constructor actually takes — the shape looked right because its neighbour `MID_mem` really does take a bare `limits`, since the contract's `memory_type` *is* `limits`. `coqc` rejects the result outright (`The term "{| lim_min := …; lim_max := … |}" has type "limits" while it is expected to have type "table_type"`), so any table import produced a `.v` that does not type-check. No fixture in the `coqc` gate had ever imported a table — Inference codegen does emit an import for every `extern fn`, but the static-merge linker (`inference-wasm-linker`) is fail-closed on imports (`LinkError::UnsatisfiedImport`), and `infc` runs that link, aborting on failure, before `-v` translation starts, so no import from the normal pipeline ever reaches the translator — so the arm was reachable only from a foreign or hand-assembled `.wasm` fed to `wasm_to_v` directly, and the defect went uncaught until the [#401] coverage work's `module_surface` fixture became the first gated module to import one. `MID_table` is now applied to `{|tt_limits := <limits>; tt_elem_type := <reference_type>|}`, pinned by both a `funcref` and an explicit-max `externref` table import in a new unit test (`an_imported_table_carries_its_element_type`, `core/wasm-to-v/src/lib.rs`) and by the `module_surface` gate fixture. Unaffected: every other import descriptor, and every committed corpus `.v` golden, since none of Inference codegen's own imports reach `wasm_to_v` — the fail-closed linker resolves them, or the build aborts, before translation runs ([#402])
@@ -193,6 +194,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Documentation
 
+- New `core/wasm-codegen/docs/specification-obligations.md` for readers of an emitted `.v` — usually someone whose proof did not close: the two kinds of obligation and the asymmetry between them, aggregates as ordered scalar leaves with the enumeration and allocation rules that fix every `T_local` index in a goal, one fully expanded three-leaf obligation, the definedness reading of `a[i]` beside the both-bounds requirement a signed index carries, quantifier alternation, the caps, and a table of every kept rejection with its reason. `core/wasm-to-v/ROCQ_CONTRACT.md` gains the matching contract rows (aggregate introduction, aggregate copy, constant and non-constant access, leafwise aggregate comparison) and its **P001**–**P014** registry is brought current ([#355])
+- Proof-mode diagnostics reworded now that the aggregate encoding makes several of them inaccurate. **P004**'s tail said "only bool, integer, and enum values can" at every site, which read as a rule the language no longer has — the parameter position accepts `[i32; 3]` and rejects `[Point; 2]`, and the reason is the shape rather than aggregation — so all its sites now name the representable surface exactly, and an aggregate read *whole* where a term is required (an aggregate call argument, most often) gets its own wording instead, since the shared one would have rejected `[i32; 2]` while listing arrays of integers as nameable. **P003**'s "is not supported" read as a schedule for a decision that is permanent, and now states the rule: a specification names values, not storage. `loop` is lifted out of the shared no-encoding template — the constructs sharing it have nothing to be rewritten *as*, while a loop's purpose in a specification is exactly what quantifying an index and constraining it says directly — and its message names that idiom. **P007**, **P008** and **P004** in an `exists`/`unique` body now name the quantifier that makes the construct impossible, because the identical declaration translates in a `forall` body, and they point at the `forall`-bodied alternative. Every message naming a quantifier takes the article that word is spoken with, which also corrects **P011**'s "an `unique`-quantified" ([#355])
 - New `core/wasm-to-v/ROCQ_CONTRACT.md` documenting the external Rocq predicates (`ValidModule` 1-arg, new `ValidSpec`), the emitted proof-skeleton shape, and spec-map precedence rules ([issue#17])
 - Rewrite `core/wasm-to-v/ROCQ_CONTRACT.md` for the wasm-verifier/vanilla-WasmCert target (hassert-valued `ValidSpec`, worked `.v` example, migration section); also rewrite `rocq-stub/README.md` and the `core/wasm-to-v/README.md` non-det section
 - Add compilation targets matrix documentation (`book/compilation_targets.md`): Compile/Proof x Debug/Release x with/without non-det operations ([issue#97])
@@ -242,6 +245,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ### Testing
 
+- Three new `coqc`-gate corpus fixtures cover the aggregate work end to end — `spec_aggregate_values.inf` (leaf encoding, enumeration order across ranks and struct field widths, literals, copies, leafwise comparison, existential leaves), `spec_bounded_iteration.inf` (the symbolic-index witness, a constant step descending before a symbolic one, a field step, and both the signed and unsigned index spellings) and `spec_quantifier_alternation.inf` (∃∀ nesting, with `"Hall "` added to `REQUIRED_CONSTRUCTS` as a needle the alternation fixture uniquely produces). Every obligation of all three was additionally proved `Qed` against real wasm-verifier before the goldens were committed, which 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` — and was rewritten rather than shipped as the documented example of the encoding ([#355])
 - The `coqc` gate now also audits, mechanically, that every constructor the vendored stub declares is elaborated by some module the gate compiles, closing what a hand-maintained needle list alone could not catch — the exact gap the [#230] `BI_forall` arity bug shipped through. New fixtures take obligation-printer operator coverage from 3 of 23 arms reachable at both `i32` and `i64` to full coverage, plus WASM module/instruction and `hassert`-printer surfaces no Inference source reaches. Seven stub declarations the emitter can never produce were deleted rather than exempted (see `rocq-stub/README.md`). This proves the stub is fully exercised, not that it still matches wasm-verifier's real `Assertions.v` ([#359]) ([#401])
 - `infs` unit tests that write an executable stub and spawn it no longer fail intermittently with `ETXTBSY`; a shared `retry_while_exec_busy` helper retries spawns racing fork-inherited write descriptors ([#345])
 - Tests outside `apps/infs` no longer race on fixed temporary paths — the class [#331] closed inside `apps/infs` and left standing elsewhere; every scratch path now comes from a `tempfile::TempDir`, fixing two live defects in codegen and cross-compiler tests ([#343])
@@ -594,3 +598,4 @@ Initial tagged release.
 [#412]: https://github.com/Inferara/inference/issues/412
 [#413]: https://github.com/Inferara/inference/issues/413
 [#416]: https://github.com/Inferara/inference/issues/416
+[#355]: https://github.com/Inferara/inference/issues/355
diff --git a/core/hassert/README.md b/core/hassert/README.md
@@ -29,10 +29,13 @@ pub enum HAssert {
     Ex(Box<HAssert>),
     TermEq(HTerm, HTerm), HasType(HTerm, HNumType), Defined(HTerm),
     AppOk(HFnRef, Vec<HTerm>),
+    All(Box<HAssert>),
 }
 ```
 
-Each variant mirrors a wasm-verifier inductive (`HA_not`, `HA_and`, `Himpl`, `Hor`, `HA_ex`, `term_eq`, `HA_has_type`, `HA_defined`, `HA_app_ok`) — the variant doc comments name the counterpart.
+Each variant mirrors a wasm-verifier inductive (`HA_not`, `HA_and`, `Himpl`, `Hor`, `HA_ex`, `term_eq`, `HA_has_type`, `HA_defined`, `HA_app_ok`, `Hall`) — the variant doc comments name the counterpart.
+
+`All` sits last against its meaning: the wire tags follow declaration order and are part of the format, so a new variant is appended rather than filed beside the relative it reads like.
 
 Each obligation entry carries its quantifier kind alongside the tree:
 
@@ -53,7 +56,9 @@ The IR omits everything an Inference specification can never contain, so an ill-
 - **No heap fragment.** `HA_emp`/`HA_star`/`HA_iter`/`HA_pto`/`HA_size` are absent; memory constructs are not translatable.
 - **No general `HA_pred`.** `TermEq` is the only predicate form, enforcing wasm-verifier's `pred_eq`/2 discipline by construction.
 
-**Implication and disjunction are explicit nodes** (`Imp`, `Or`), not their classical De Morgan encodings. wasm-verifier's `Himpl`/`Hor` are definitionally-transparent `Definition`s, so a downstream printer can render these nodes as `Himpl`/`Hor` without ever pattern-matching an encoding.
+**Implication, disjunction and universal quantification are explicit nodes** (`Imp`, `Or`, `All`), not their classical De Morgan encodings. wasm-verifier's `Himpl`/`Hor`/`Hall` are definitionally-transparent `Definition`s, so a downstream printer can render these nodes by name without ever pattern-matching an encoding.
+
+`All` earns its place twice over. Beyond legibility, the downstream `ValidSpec` judgment quantifies the payload's free variables universally from outside, so an inner universal encoded as anything but a binder of its own would be bound out there instead — turning `∃x. ∀y. P` into `∀y. ∃x. P` without a trace.
 
 ### Symbolic function references
 
@@ -69,6 +74,7 @@ Constructors on `HAssert` apply the `True`-simplifications that keep a translate
 | `imp(p, q)` | `⊤ → q = q`, `p → ⊤ = ⊤` |
 | `or(a, b)`  | `⊤ ∨ x = ⊤`, `x ∨ ⊤ = ⊤` (`⊤` absorbing, the dual of its being the identity for `and`) |
 | `ex(body)`  | `∃x. ⊤ = ⊤` |
+| `all(body)` | `∀x. ⊤ = ⊤` (the dual of `ex`, sound because the domain is never empty) |
 | `nz(t)`     | `¬(t = 0)` |
 | `eqz(t)`    | `t = 0` |