From 5b0a3f6240b68749e9cde3239666f88f8040c18d Mon Sep 17 00:00:00 2001 From: "Abhishek Anand (Monad Labs)" Date: Wed, 14 Oct 2026 14:22:21 -0400 Subject: [PATCH] Specify packed vector ownership and proxy access Add the approved default-allocator LP64 interface for fill/move/destruction and bit access/update. Keep the abstract packed-storage Rep and type observation explicit, with a concrete definition sketch. Define the proxy's real fields and require matching live vector ownership for reads and writes. Bound fill sizes by 2^63-64. Add a cpp.prog client exercising construction, update, move, read and cleanup. Checked independently and through Monad all.vo; library bodies remain assumed. (cherry picked from commit e877ee834e51406b2f64945c62507765259489d8) --- rocq-brick-libstdcpp/proof/vector/bool_spec.v | 144 ++++++++++++++++++ rocq-brick-libstdcpp/proof/vector/bool_test.v | 48 ++++++ 2 files changed, 192 insertions(+) create mode 100644 rocq-brick-libstdcpp/proof/vector/bool_spec.v create mode 100644 rocq-brick-libstdcpp/proof/vector/bool_test.v diff --git a/rocq-brick-libstdcpp/proof/vector/bool_spec.v b/rocq-brick-libstdcpp/proof/vector/bool_spec.v new file mode 100644 index 00000000..6ae23eea --- /dev/null +++ b/rocq-brick-libstdcpp/proof/vector/bool_spec.v @@ -0,0 +1,144 @@ +(** libstdc++'s packed-bit specialization with its default allocator. + This library boundary is independent of any application or bytecode model. + These are assumed method specs; allocation failure is not excluded by + their normal-return postconditions. Custom allocators are not covered. *) +Require Import skylabs.auto.cpp.proof. +Require Import skylabs.lang.cpp.parser.plugin.cpp2v. +Require Import skylabs.brick.libstdcpp.allocator.spec. + +Set Default Goal Selector "!". +Set Warnings "+sl-transparent-constants". + +(** Instantiate the library declarations, including the proxy's special + members, for cpp.spec. This function is only an AST fixture. *) +#[elaborate] +cpp.prog source prog cpp:{{ +#include +void vector_bool_interface(std::vector& bits, unsigned long i, bool b) { + std::vector fresh(1, b); + bits[i] = b; + bool x = bits[i]; + bool y = static_cast const&>(bits)[i]; + std::vector moved(static_cast&&>(fresh)); +} +}}. + + (** Definition sketch: own the vector and _Bvector_base/_Bvector_impl + subobjects, the allocator, the start/finish bit iterators and the + end-of-storage pointer. Existentially own the allocated unsigned-long + array beginning at [data], its capacity and allocation token. The + finish iterator encodes [length bits]; bit i of that word array equals + bits[i]. Padding bits are existential, not forced to zero. Empty and + moved-from vectors may use nullptr without owning an array there. + + [q] fractions cover both the descriptor and the actual packed words. + Full ownership is required to update a bit or destroy/move the vector. + There is intentionally no lemma giving independent writable ownership + of two bits: different bits may share one word. A proxy owns only its + descriptor; reading/writing through it also requires this live storage + with the matching [data] and an in-range index. *) +Parameter VectorBoolR : forall `{Sigma : cpp_logic} {CU : genv}, + cQp.t -> ptr -> list bool -> Rep. + +Section with_cpp. + Context `{Sigma : cpp_logic} {CU : genv}. + + #[global] Instance VectorBoolR_type_ptr q data bits : + Observe (type_ptrR "std::vector>") + (VectorBoolR q data bits). + Admitted. + Definition VectorBoolR_type_ptr_F := + ltac:(mk_at_obs_fwd VectorBoolR_type_ptr). + #[global] Instance learn_VectorBoolR : LearnEq3 VectorBoolR := + ltac:(solve_learnable). + + (** The actual libstdc++ proxy fields. This owns no vector storage. The + supported target has 64-bit unsigned long, matching _S_word_bit. *) + Definition BitReferenceR (q : cQp.t) (data : ptr) (index : N) : Rep := + structR "std::_Bit_reference" q ** + _field "std::_Bit_reference::_M_p" |-> + primR (Tptr Tulong) q + (Vptr (data .[Tulong ! Z.of_N (index / 64)])) ** + _field "std::_Bit_reference::_M_mask" |-> + ulongR q (2 ^ Z.of_N (index mod 64)). + + #[global] Instance BitReferenceR_type_ptr q data index : + Observe (type_ptrR "std::_Bit_reference") (BitReferenceR q data index). + Proof. unfold BitReferenceR. apply _. Qed. + Definition BitReferenceR_type_ptr_F := + ltac:(mk_at_obs_fwd BitReferenceR_type_ptr). + #[global] Instance learn_BitReferenceR : LearnEq3 BitReferenceR := + ltac:(solve_learnable). + + #[local] Hint Opaque VectorBoolR BitReferenceR : sl_opacity. + + cpp.spec "std::vector>::vector(unsigned long, const bool&, const std::allocator&)" + from source as vector_bool_fill_ctor_spec with (fun (this : ptr) => + \arg{size : N} "size" (Vn size) + \arg{valuep : ptr} "value" (Vref valuep) + \arg{allocp : ptr} "allocator" (Vref allocp) + \prepost{qvalue b} valuep |-> boolR qvalue b + \prepost{qalloc} allocp |-> std.allocator.R Tbool qalloc () + (* LP64 ptrdiff_t and rounded word-count bound: 2^63 - 64. *) + \pre [| (size <= 9223372036854775744)%N |] + \post Exists data, + this |-> VectorBoolR 1$m data (replicateN size b) + ). + + cpp.spec "std::vector>::vector(std::vector>&&)" + from source as vector_bool_move_ctor_spec with (fun (this : ptr) => + \arg{other : ptr} "other" (Vref other) + \pre{data bits} other |-> VectorBoolR 1$m data bits + \post this |-> VectorBoolR 1$m data bits ** + other |-> VectorBoolR 1$m nullptr [] + ). + + cpp.spec "std::vector>::~vector()" + from source as vector_bool_dtor_spec with (fun (this : ptr) => + \pre{data bits} this |-> VectorBoolR 1$m data bits + \post emp + ). + + cpp.spec "std::vector>::operator[](unsigned long)" + from source as vector_bool_index_spec with (fun (this : ptr) => + \arg{index : N} "index" (Vn index) + \prepost{q data bits} this |-> VectorBoolR q data bits + \pre [| (index < N.of_nat (length bits))%N |] + \post{retp : ptr} [Vptr retp] retp |-> BitReferenceR 1$m data index + ). + + cpp.spec "std::vector>::operator[](unsigned long) const" + from source as vector_bool_index_const_spec with (fun (this : ptr) => + \arg{index : N} "index" (Vn index) + \prepost{q data bits} this |-> VectorBoolR q data bits + \pre [| (index < N.of_nat (length bits))%N |] + \post[Vbool (nth (N.to_nat index) bits false)] emp + ). + + cpp.spec "std::_Bit_reference::operator=(bool)" + from source as bit_reference_assign_spec with (fun (this : ptr) => + \arg{b : bool} "value" (Vbool b) + \prepost{data index} this |-> BitReferenceR 1$m data index + \pre{(vectorp : ptr) bits} vectorp |-> VectorBoolR 1$m data bits + \pre [| (index < N.of_nat (length bits))%N |] + \post[Vref this] + vectorp |-> VectorBoolR 1$m data (<[N.to_nat index := b]> bits) + ). + + cpp.spec "std::_Bit_reference::operator bool() const" + from source as bit_reference_read_spec with (fun (this : ptr) => + \prepost{qref data index} this |-> BitReferenceR qref data index + \prepost{(vectorp : ptr) q bits} vectorp |-> VectorBoolR q data bits + \pre [| (index < N.of_nat (length bits))%N |] + \post[Vbool (nth (N.to_nat index) bits false)] emp + ). + + cpp.spec "std::_Bit_reference::~_Bit_reference()" + from source as bit_reference_dtor_spec with (fun (this : ptr) => + \pre{data index} this |-> BitReferenceR 1$m data index + \post emp + ). +End with_cpp. + +#[global] Hint Opaque VectorBoolR BitReferenceR : sl_opacity. +#[global] Hint Resolve VectorBoolR_type_ptr_F BitReferenceR_type_ptr_F : sl_opacity. diff --git a/rocq-brick-libstdcpp/proof/vector/bool_test.v b/rocq-brick-libstdcpp/proof/vector/bool_test.v new file mode 100644 index 00000000..6f92adef --- /dev/null +++ b/rocq-brick-libstdcpp/proof/vector/bool_test.v @@ -0,0 +1,48 @@ +(** Exercise packed-bit fill construction, proxy update/read, move, and both + moved-from and live destruction. This checks the assumed library API. *) +Require Import skylabs.auto.cpp.proof. +Require Import skylabs.lang.cpp.parser.plugin.cpp2v. +Require Import skylabs.brick.libstdcpp.allocator.spec. +Require Import skylabs.brick.libstdcpp.vector.bool_spec. + +Set Default Goal Selector "!". +Set Warnings "+sl-transparent-constants". +Import linearity. +#[local] Hint Resolve UNSAFE_read_prim_cancel : sl_opacity. +Remove Hints _at_pick_cfrac_and_split_C _at_pick_frac_and_split_C + _at_split_specific_cfrac_C _at_split_specific_frac_C + : db_skylabs_syntactic. + +#[elaborate] +cpp.prog source prog cpp:{{ +#include +bool bit_roundtrip(bool value, std::allocator const& allocator) { + std::vector bits(2, false, allocator); + bits[1] = value; + std::vector moved(static_cast&&>(bits)); + return moved[1]; +} +}}. + +Section with_cpp. + Context `{Sigma : cpp_logic, MOD : source ⊧ σ}. + + cpp.spec "bit_roundtrip(bool, const std::allocator&)" from source as bit_roundtrip_spec with ( + \arg{value : bool} "value" (Vbool value) + \arg{allocp : ptr} "allocator" (Vref allocp) + \prepost{qalloc} allocp |-> std.allocator.R Tbool qalloc () + \post[Vbool value] emp + ). + + Lemma bit_roundtrip_ok : verify[source] bit_roundtrip_spec. + Proof using MOD. + verify_spec. + go. + iExists qalloc. + go. + iExists bits_addr, [false; false]. + go. + iExists moved_addr, (cQp.mut 1), [false; value]. + go. + Qed. +End with_cpp.