[aa755]

Summary

Add the existing packed-bit std::vector<bool, std::allocator<bool>> interface as a focused change based on upstream main d745fecc7cc7322c2269b7a16bb04fd052ccf779.

This is one cherry-picked commit and two new files. It does not include, or depend on, the pending shared-pointer changes in #10.

• Abstract VectorBoolR for the descriptor and packed storage, with a documented concrete-definition sketch and explicit type-pointer observation assumption.
• Concrete BitReferenceR for libstdc++'s pointer/mask proxy fields.
• Fill construction, move construction, destruction, mutable/const indexing, proxy read/write, and proxy destruction specs.
• A checked C++ client that constructs a vector, changes one bit, moves the vector, reads the bit and destroys both the moved-from and live objects.

Ownership and scope

This is an explicitly assumed library interface, not a verification of the standard-library method bodies. VectorBoolR and its type observation remain abstract/assumed. The client theorem is proved using the library specs.

The interface targets libstdc++'s default allocator on LP64. The fill-size bound is 2^63 - 64. Custom allocators and other layouts are outside this interface.

A proxy owns only its descriptor. Reading also requires fractional ownership of the matching live vector storage; writing requires full mutable ownership and an in-range index. The specs do not expose independently writable ownership for separate bits, which may share a machine word.

Validation

• dune build fmdeps/brick-libcpp/rocq-brick-libstdcpp/proof/vector/bool_test.vo monad/monadproofs/proofs/all.vo passes in the composed development workspace.
• Separately compiled this upstream-based branch's unchanged allocator/spec.v, then vector/bool_spec.v and vector/bool_test.v, using the same built BRiCk/auto/Rocq dependencies and remapping the library load path to this branch. All three passed. Thus the client does not rely on our unrelated allocator or shared-pointer patches.
• Those focused checks used Rocq 9.2 / OCaml 5.5.1, Clang 22 and local libstdc++; they are not a claim of testing every supported platform.
• A standalone Dune invocation against the local installed dependency tree was blocked by broken installation symlinks; it is not being reported as passing. The focused checks above and the composed-workspace Dune build are the completed local validation.
• git diff --check passes.

Original local commit: e877ee834e51406b2f64945c62507765259489d8.

[aa755]

CI note: the initial Trigger run failed before compilation while checking out SkylabsAI/ci: Input required and not supplied: token. This is a CI checkout/authentication failure, not a Rocq test result. The completed local validation is documented in the PR description; a maintainer-side CI run is still needed.