feat(array): const-transport laws, dataclass fields and `operator==` for `std::array` by jhaag-skylabs-ai · Pull Request #237 · SkyLabsAI/brick-libcpp

jhaag-skylabs-ai · 2026-10-27T14:04:50Z

Laws that connect std.array.R to the shapes in which a std::array reaches a proof: const transport, element-wise ownership after initialization, and cpp.class … dataclass fields. Also an operator== spec. ProveCode test proofs on const std::array<unsigned char, 16> locals currently restate the const-transport part by hand in each proof (about 80 lines), and those proofs reached 13 GiB.

Laws (proof/array/pred.v):

array_sliceR_wp_const (registered as [CANCEL]): for prim_const_ok ty (an unqualified value type), p |-> array_sliceR ty 0 n (primR ty from ∘ f) xs and a continuation from the to slice give wp_const tu from to p (Tarray ty sz) Q, with n = sz. array_sliceR_wp_const_fold is the per-element induction behind it.
R_wp_const: p |-> R_gen ty n from (primR ty from ∘ f) xs and a continuation from R_gen ty n to … give wp_const tu from to p (T ty n) Q, provided tu.(types) !! N ty n = Some (Gstruct st) and struct_ok ty n st: no bases, no vtable, exactly one non-mutable field _M_elems : ty[n], 0 < n, prim_const_ok ty.
R_wp_const_Vint (registered as [BWD]): R_wp_const for Vint elements, with the layout premises as =[Vm?]=> side conditions, looked up the same way as BRiCk's wp_const_named_struct.
array_sliceR_fold_Vint (registered as [FWD]): at a std::array's element storage p ,, elems ty n, array_sliceR ty i j (primR ty q) vs becomes array_sliceR ty i j (fun x => primR ty q (Vint x)) xs when ints_of_vals vs computes to Some xs. This covers value or aggregate initialization (a{}, a{1,2,3,4}). Slices elsewhere, such as builtin arrays, are left alone. The equivalence behind it is auto's array_sliceR_fmap.
Timeless for spineR (derived in spec.v), and std.array.fieldR with two Elpi rules for skylabs.synth.db: a std::array<ty, n> field of a dataclass gets model list M and representation fieldR ty n Relem, which unfolds to R_gen ty n q (Relem q).

proof/array/spec.v:

operator_eq: a == b returns bool_decide (xs = ys), with \require eq_is_model_eq ty = true: integral (Tnum), character (Tchar_) and bool elements only (see below). This is an assumed specification, like the rest of the file; it is not checked against libstdc++'s std::equal/__builtin_memcmp body. != needs no spec of its own because C++20 rewrites it to !(a == b).
repfor is now a Hint Extern instead of an instance. As an instance it elaborated list ?M before ?M was known and failed with a universe error, so cpp.spec … default found no Rep for std::array.

Why R_wp_const has no type_table_le premise: const.CONST relates the library's translation unit to the client's by type_table_le, and that relation is false between real units. brick-libgtest's TODO.md (U3) measured a library table of 8,389 entries against a client table of 11,525: 0 incompatible entries and 1 missing one (std::align_val_t), so type_table_le was false. Which declarations a unit keeps depends on what it references, so the premise can fail because of unrelated client code. These laws instead read the class layout from the tu in which wp_const is evaluated (tu.(types) !! N ty n) and check it with struct_ok. They are proved, not assumed, so they hold for every client whose unit has the libstdc++ layout.

Tests (test/array/laws.cpp, laws_cpp_proof.v), each proved with plain verify_spec; go and no proof-specific hints:

HolderByte: a dataclass Holder with an array<unsigned char, 16> field.
ConstLocal: a const array<unsigned char, 4> local, which goes through wp_make_const and wp_make_mutable.
ZeroThenFill: a{} followed by a.fill(v).
Eq and Ne: == on array<unsigned char, 16> and != on array<int, 3>.
cpp.spec … default for Eq, which checks the RepFor fix.
fold_Vint_ex: the fold hint under an existential, and a Fail check that it does not fire on a slice outside a std::array.

Built after rebasing on main, with BRiCk and auto at their main: proof/array/{spec,pred}.vo, test/array/laws_cpp_proof.vo, and test/array/test_cpp_proof.vo, the only other file that imports the array specs. test/dune.inc is regenerated by dune-gen.sh.

Revision (`f831190`)

array_sliceR_Vint is gone: it duplicated auto's array_sliceR_fmap, which the fold law now uses.
spineR_timeless is gone: Timeless is derived with the other spineR instances (#[only(…,timeless)] derive spineR).
operator_eq is restricted to element types whose == is equality of the model (next section).
The [FWD] fold hint only fires on a slice at p ,, elems ty n, not on every concrete list of Vints in any array_sliceR. All tests pass unchanged.

`operator==` scope

The spec states the result as bool_decide (xs = ys), so it is only sound when the element == is equality of the element model. eq_is_model_eq ty accepts the integral, character and bool types (after erase_qualifiers). Their == is builtin and cannot be overloaded, and their prim_BundledRep model is injective. Everything else is excluded:

floating point: NaN != NaN, -0.0 == 0.0;
pointers: == needs ptr_comparable, and distinct pointers (one past the end of one object, the start of the next) can compare equal;
enumerations and classes: == can be overloaded. Enumerations also have no BundledRep in auto.

A version for element types with a proved == spec (an ElemEq ty eqb premise) is a separate follow-up.

Known gaps

Arrays of char, bool, pointers or enumerations get no const hints. R_wp_const_Vint and the fold law are for Vint only. The fold law has to read the model back from vals (ints_of_vals), which needs a decoder, and auto only has encoders (prim_BundledRep Vint/Vchar/Vbool/Vptr). R_wp_const itself is generic in the element encoding, but nothing registers it as a hint for other encodings.

Overlap with auto#592 and auto#537

auto#592 (open, wp_const support for array_sliceR) adds wp_const_array_sliceR_C, a general [CANCEL] hint for wp_const at Tarray ty n over array_sliceR ty 0 n R xs, for any AsCFractional element representation. Each element goes to the existing per-type wp_const hints. This is the hint auto#537 (no wp_const hint for array-typed members) asks for. Once #592 lands:

array_sliceR_wp_const, array_sliceR_wp_const_fold and array_sliceR_wp_const_C become redundant. #592 covers the same goal for every element type, not only primR elements.
R_wp_const and R_wp_const_Vint_B are probably redundant: with spineR unfolded, BRiCk's wp_const_named_struct_C reaches the _M_elems field and #592 handles the array. This has not been tested. R_wp_const_Vint is [BWD] because ownership is often split by the time the array is made mutable again, and it is not checked whether the cancellation route copes with that.
array_sliceR_fold_Vint, fieldR and the dataclass rules, and operator_eq are unaffected.

This PR does not depend on #592. #592 also comments out VcRwDefs.wp_init_initlist_prim_array_implicit_B, which could change the shape a{} leaves behind. ZeroThenFill is the test to rerun against it.

Revision build (pointed targets, from the workspace root, 10 GiB cap): proof/array/pred.vo, test/array/laws_cpp_proof.vo and test/array/test_cpp_proof.vo all pass.

🤖 Generated with Claude Code

skylabs-ai-ci · 2026-10-27T14:20:26Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Branch Tip	Base branch	Base commit	PR
fmdeps/brick-libcpp/	jhaag/std-array-laws	4db68eb	5d7736b	main	8162fea	#237

Passive Repos

Repo	Job Branch	Job Commit
./	main	781c507
fmdeps/BRiCk/	main	cb506b7
fmdeps/auto/	main	4cba1bf
fmdeps/auto-docs/	main	918aa33
bluerock/NOVA/	skylabs-proof	9587b7c
bluerock/bhv/	skylabs-main	42f282b
fmdeps/brick-libgtest/	main	495b855
fmdeps/ci/	main	b480641
vendored/elpi/	skylabs-master	c0b9653
vendored/flocq/	skylabs-master	cf9cc84
vendored/rocq/	skylabs-master	7c6eef8
fmdeps/rocq-agent-toolkit/	main	21eb550
vendored/rocq-elpi/	skylabs-master	7dee592
vendored/rocq-equations/	skylabs-main	9cf8471
vendored/rocq-iris/	skylabs-master	a7af9f7
vendored/rocq-stdlib/	skylabs-master	00897b3
vendored/rocq-stdpp/	skylabs-master	0c5e505
fmdeps/skylabs-fm/	main	4cd041a
vendored/vsrocq/	skylabs-main	03db19e

Changes in Warnings or Errors

	Before	New	Fixed	After
Errors	0	0	0	0
Warnings	77	${\color{red}1}$	0	78

Performance

Relative	Master	MR	Change	Filename
+0.11%	197274.4	197496.5	+222.1	total
+0.10%	-	205.3	+205.3	├ newly appeared files (2)
+0.01%	197274.4	197291.2	+16.8	└ common files
-0.00%	49381.4	49381.4	-0.0	├ translation units
+0.01%	147893.0	147909.8	+16.8	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-0.18%	752.4	751.1	-1.3	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/array/test_cpp_proof.v
+174.47%	10.2	28.0	+17.8	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/array/pred.v

+0.11%	197274.4	197496.5	+222.1	total
+0.10%	-	205.3	+205.3	├ newly appeared files (2)
+0.01%	197274.4	197291.2	+16.8	└ common files
-0.00%	49381.4	49381.4	-0.0	├ translation units
+0.01%	147893.0	147909.8	+16.8	└ proofs and tests

skylabs-ai-ci · 2026-10-27T17:54:02Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Branch Tip	Base branch	Base commit	PR
fmdeps/brick-libcpp/	jhaag/std-array-laws	330bb29	f831190	main	192c9dd	#237

Passive Repos

Repo	Job Branch	Job Commit
./	main	781c507
fmdeps/BRiCk/	main	2ce8ed0
fmdeps/auto/	main	a24e391
fmdeps/auto-docs/	main	918aa33
bluerock/NOVA/	skylabs-proof	02f6828
bluerock/bhv/	skylabs-main	e235791
fmdeps/brick-libgtest/	main	495b855
fmdeps/ci/	main	b480641
vendored/elpi/	skylabs-master	c0b9653
vendored/flocq/	skylabs-master	cf9cc84
vendored/rocq/	skylabs-master	7c6eef8
fmdeps/rocq-agent-toolkit/	main	53fde9a
vendored/rocq-elpi/	skylabs-master	7dee592
vendored/rocq-equations/	skylabs-main	9cf8471
vendored/rocq-iris/	skylabs-master	285745a
vendored/rocq-stdlib/	skylabs-master	00897b3
vendored/rocq-stdpp/	skylabs-master	ba29dba
fmdeps/skylabs-fm/	main	ffa586f
vendored/vsrocq/	skylabs-main	03db19e

Changes in Warnings or Errors

	Before	New	Fixed	After
Errors	0	0	0	0
Warnings	76	${\color{red}1}$	0	77

Performance

Relative	Master	MR	Change	Filename
+0.11%	199093.8	199317.9	+224.1	total
+0.10%	-	208.8	+208.8	├ newly appeared files (2)
+0.01%	199093.8	199109.1	+15.3	└ common files
+0.00%	49396.3	49396.3	+0.0	├ translation units
+0.01%	149697.5	149712.8	+15.3	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
-0.17%	760.7	759.4	-1.3	fmdeps/brick-libcpp/rocq-brick-libstdcpp/test/array/test_cpp_proof.v
+177.27%	10.3	28.5	+18.2	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/array/pred.v

+0.11%	199093.8	199317.9	+224.1	total
+0.10%	-	208.8	+208.8	├ newly appeared files (2)
+0.01%	199093.8	199109.1	+15.3	└ common files
+0.00%	49396.3	49396.3	+0.0	├ translation units
+0.01%	149697.5	149712.8	+15.3	└ proofs and tests

…r std::array `array/pred.v` connects `std.array.R` to the other shapes in which a `std::array` reaches a proof: - Const transport. `R_wp_const` proves `wp_const tu from to p (T ty n) Q` from `R_gen ty n from (primR ty from ∘ f)` for the `tu` that `wp_const` is evaluated in, given that `tu` lays out `std::array<ty, n>` as libstdc++ does (`struct_ok`: no bases, no vtable, one non-mutable field `_M_elems : ty[n]`, `0 < n`, `ty` an unqualified value type). It reads the layout from that `tu`, so it has no `type_table_le` premise and applies in every client. `array_sliceR_wp_const` is the same for the bare `ty[sz]` field. Both are registered as hints (`[CANCEL]` for the slice, `[BWD]` over `Vint` elements for `R`). - Element-wise ownership. Value or aggregate initialization leaves a `val`-indexed `array_sliceR ty i j (primR ty q) vs`; the forward hint `array_sliceR_fold_Vint` rewrites it to the `Z`-indexed slice that `std.array.R` wants when `vs` is a concrete list of `Vint`s. - Dataclass fields. `cpp.class … dataclass` now models a `std::array<ty, n>` field as `list M` with representation `std.array.fieldR`, which unfolds to `std.array.R_gen`. - `spineR` is `Timeless`, needed for `R` as a dataclass field. `array/spec.v` adds an (assumed) `operator==` specification, stated as equality of the element models and excluding floating-point elements, and makes `repfor` a `Hint Extern` instead of an instance: as an instance it elaborated `list ?M` before `?M` was known and failed on a universe constraint, so `cpp.spec … default` found no `Rep` for `std::array`. Motivation: ProveCode test proofs on `const std::array<unsigned char, 16>` locals had to restate these laws by hand in each proof (about 80 lines), and those proofs reached 13 GiB. `test/array/laws.cpp` and `laws_cpp_proof.v` exercise each law with plain `go`: a dataclass with an array field, a `const` array local, value initialization followed by `fill`, `==`, and `!=` (rewritten to `!(a == b)` in C++20). `test/dune.inc` is regenerated by `dune-gen.sh`. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

…fold hint - operator_eq now requires eq_is_model_eq ty = true: integral, character and bool elements only. Pointer elements (== needs ptr_comparable), enumerations and classes (overloadable ==) and floating point are excluded, since for them == is not equality of the model. - Drop array_sliceR_Vint, a duplicate of auto's array_sliceR_fmap. - Derive Timeless for spineR instead of proving it by hand. - array_sliceR_fold_Vint_F only fires on a slice at a std::array's _M_elems field, not on every Vint slice; add a negative test. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

skylabs-ai-ci · 2026-10-27T19:46:29Z

CI summary (Details)

Active Repos

Repo	Job Branch	Job Commit	Branch Tip	Base branch	Base commit	PR
fmdeps/brick-libcpp/	jhaag/std-array-laws	aa60a11	84eb992	main	192c9dd	#237

Passive Repos

Repo	Job Branch	Job Commit
./	main	781c507
fmdeps/BRiCk/	main	2ce8ed0
fmdeps/auto/	main	ff6306c
fmdeps/auto-docs/	main	918aa33
bluerock/NOVA/	skylabs-proof	02f6828
bluerock/bhv/	skylabs-main	e235791
fmdeps/brick-libgtest/	main	495b855
fmdeps/ci/	main	b480641
vendored/elpi/	skylabs-master	c0b9653
vendored/flocq/	skylabs-master	cf9cc84
vendored/rocq/	skylabs-master	7c6eef8
fmdeps/rocq-agent-toolkit/	main	53fde9a
vendored/rocq-elpi/	skylabs-master	7dee592
vendored/rocq-equations/	skylabs-main	9cf8471
vendored/rocq-iris/	skylabs-master	285745a
vendored/rocq-stdlib/	skylabs-master	00897b3
vendored/rocq-stdpp/	skylabs-master	ba29dba
fmdeps/skylabs-fm/	main	ffa586f
vendored/vsrocq/	skylabs-main	03db19e

Changes in Warnings or Errors

	Before	New	Fixed	After
Errors	0	0	0	0
Warnings	76	${\color{red}1}$	0	77

Performance

Relative	Master	MR	Change	Filename
+0.11%	199110.0	199337.8	+227.7	total
+0.10%	-	208.8	+208.8	├ newly appeared files (2)
+0.01%	199110.0	199129.0	+18.9	└ common files
-0.00%	49396.3	49396.3	-0.0	├ translation units
+0.01%	149713.8	149732.7	+18.9	└ proofs and tests

Full Results

Relative	Master	MR	Change	Filename
+177.32%	10.3	28.5	+18.2	fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/array/pred.v

+0.11%	199110.0	199337.8	+227.7	total
+0.10%	-	208.8	+208.8	├ newly appeared files (2)
+0.01%	199110.0	199129.0	+18.9	└ common files
-0.00%	49396.3	49396.3	-0.0	├ translation units
+0.01%	149713.8	149732.7	+18.9	└ proofs and tests

jhaag-skylabs-ai marked this pull request as draft October 27, 2026 17:31

jhaag-skylabs-ai and others added 2 commits October 27, 2026 15:31

jhaag-skylabs-ai force-pushed the jhaag/std-array-laws branch from f831190 to 84eb992 Compare October 27, 2026 19:31

Navigation Menu

Repository navigation

feat(array): const-transport laws, dataclass fields and `operator==` for `std::array` - #237

feat(array): const-transport laws, dataclass fields and `operator==` for `std::array`#237
jhaag-skylabs-ai wants to merge 2 commits into
mainfrom
jhaag/std-array-laws

jhaag-skylabs-ai commented Oct 27, 2026 •

edited

Loading

Uh oh!

skylabs-ai-ci Bot commented Oct 27, 2026

Passive Repos

Uh oh!

skylabs-ai-ci Bot commented Oct 27, 2026

Passive Repos

Uh oh!

skylabs-ai-ci Bot commented Oct 27, 2026

Passive Repos

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

jhaag-skylabs-ai commented Oct 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Revision (f831190)

operator== scope

Known gaps

Overlap with auto#592 and auto#537

Uh oh!

skylabs-ai-ci Bot commented Oct 27, 2026

CI summary (Details)

Active Repos

Passive Repos

Changes in Warnings or Errors

Performance

Uh oh!

skylabs-ai-ci Bot commented Oct 27, 2026

CI summary (Details)

Active Repos

Passive Repos

Changes in Warnings or Errors

Performance

Uh oh!

skylabs-ai-ci Bot commented Oct 27, 2026

CI summary (Details)

Active Repos

Passive Repos

Changes in Warnings or Errors

Performance

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

jhaag-skylabs-ai commented Oct 27, 2026 •

edited

Loading

Revision (`f831190`)

`operator==` scope