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