Specified in .design/build/aggregate-array-relations.md under "Quantified logical-index relations". Nothing is implemented today.
thermite-syntax has no #[logical(bound = "...", observe = "...")] struct attribute; fn parse_attribute in parser.rs accepts only slag, boundary, sealed, opaque.fn check_array_relation_call in thermite-spec/src/validator.rs requires both operands to be Type::Array, so the relation family cannot apply to a collection state.fn lower_inv_expr in thermite-lower/src/lower.rs recognises array_eq, array_same_except, and array_same_except_two only.- No TV encoder derives a logical index space;
thermite-tv/src/ref_encode.rs and thermite-tv/src/exec_encode.rs model the storage view.
Scope of this blocker is the index-transparent observer subset: every occurrence of the observer's index parameter is a direct index of a fixed-array field of the receiver, with no arithmetic applied to the index. That subset covers the slot views of FixedRing64, FixedVec64, FixedSlab64, FixedFreelist64, FixedIntrusiveList64, FixedDirectMap64, and FixedOpenMap64, and it is the form an opaque collection needs to export a public all-index contract without exposing field names.
Derived-index (packed) observers such as fixed_bitmap_contains_spec are tracked separately.
Specified in
.design/build/aggregate-array-relations.mdunder "Quantified logical-index relations". Nothing is implemented today.thermite-syntaxhas no#[logical(bound = "...", observe = "...")]struct attribute;fn parse_attribute in parser.rsaccepts onlyslag,boundary,sealed,opaque.fn check_array_relation_call in thermite-spec/src/validator.rsrequires both operands to beType::Array, so the relation family cannot apply to a collection state.fn lower_inv_expr in thermite-lower/src/lower.rsrecognisesarray_eq,array_same_except, andarray_same_except_twoonly.thermite-tv/src/ref_encode.rsandthermite-tv/src/exec_encode.rsmodel the storage view.Scope of this blocker is the index-transparent observer subset: every occurrence of the observer's index parameter is a direct index of a fixed-array field of the receiver, with no arithmetic applied to the index. That subset covers the slot views of
FixedRing64,FixedVec64,FixedSlab64,FixedFreelist64,FixedIntrusiveList64,FixedDirectMap64, andFixedOpenMap64, and it is the form an opaque collection needs to export a public all-index contract without exposing field names.Derived-index (packed) observers such as
fixed_bitmap_contains_specare tracked separately.