From f17a48ab713cbd66a73b939f27bcb4e80f11cdfd Mon Sep 17 00:00:00 2001 From: Jasper Haag Date: Wed, 9 Sep 2026 17:39:11 -0400 Subject: [PATCH 1/4] feat: std::array specs --- .../proof/array/inc_array.cpp | 6 + rocq-brick-libstdcpp/proof/array/pred.v | 6 + rocq-brick-libstdcpp/proof/array/spec.v | 561 ++++++++++++++++++ rocq-brick-libstdcpp/proof/dune.inc | 12 + rocq-brick-libstdcpp/test/array/test.cpp | 180 ++++++ .../test/array/test_cpp_proof.v | 442 ++++++++++++++ rocq-brick-libstdcpp/test/dune.inc | 12 + 7 files changed, 1219 insertions(+) create mode 100644 rocq-brick-libstdcpp/proof/array/inc_array.cpp create mode 100644 rocq-brick-libstdcpp/proof/array/pred.v create mode 100644 rocq-brick-libstdcpp/proof/array/spec.v create mode 100644 rocq-brick-libstdcpp/test/array/test.cpp create mode 100644 rocq-brick-libstdcpp/test/array/test_cpp_proof.v diff --git a/rocq-brick-libstdcpp/proof/array/inc_array.cpp b/rocq-brick-libstdcpp/proof/array/inc_array.cpp new file mode 100644 index 00000000..02e74e9b --- /dev/null +++ b/rocq-brick-libstdcpp/proof/array/inc_array.cpp @@ -0,0 +1,6 @@ +/** + * Copyright (c) 2026 SkyLabs AI, Inc. + * This software is distributed under the terms of the BedRock Open-Source License. + * See the LICENSE-BedRock file in the repository root for details. + */ +#include diff --git a/rocq-brick-libstdcpp/proof/array/pred.v b/rocq-brick-libstdcpp/proof/array/pred.v new file mode 100644 index 00000000..9b0598d5 --- /dev/null +++ b/rocq-brick-libstdcpp/proof/array/pred.v @@ -0,0 +1,6 @@ +(* + * Copyright (c) 2026 SkyLabs AI, Inc. + * This software is distributed under the terms of the BedRock Open-Source License. + * See the LICENSE-BedRock file in the repository root for details. + *) +Require Export skylabs.brick.libstdcpp.array.spec. diff --git a/rocq-brick-libstdcpp/proof/array/spec.v b/rocq-brick-libstdcpp/proof/array/spec.v new file mode 100644 index 00000000..b5ab3757 --- /dev/null +++ b/rocq-brick-libstdcpp/proof/array/spec.v @@ -0,0 +1,561 @@ +(* + * Copyright (c) 2026 SkyLabs AI, Inc. + * This software is distributed under the terms of the BedRock Open-Source License. + * See the LICENSE-BedRock file in the repository root for details. + *) +Require Import skylabs.auto.cpp.spec. +Require Export skylabs.cpp.slice. + +Require Import skylabs.cpp.spec.concepts. +Require Import skylabs.cpp.spec.concepts.experimental. + +Require Import skylabs.brick.libstdcpp.array.inc_array_cpp. +Require Import skylabs.brick.libstdcpp.array.inc_array_cpp_templates. + +NES.Begin std. + #[local] Open Scope Z_scope. + + NES.Begin array. + (** + Module [std.array] specifies < >> for an arbitrary element + type [ty] and an arbitrary (positive) extent [n]: every definition below is a + template specification in the sense of [specify.template], so a single + specification applies to every instantiation. + + # Representation + + Unlike <>, a <> stores its elements inline, so there is + no separately allocated buffer and no capacity. The ownership of an array at [p] + therefore splits into + + - [p |-> spineR ty n q], the <> identity of the array object, and + - [p ,, elems ty n |-> array_sliceR ty 0 n Rpayload xs], the [n] element payloads, + + bundled as [p |-> R_gen ty n q Rpayload xs], with [p |-> R ty n q xs] using the + element type's [BundledRep] as the payload. Splitting the two gives the same + benefits as for <>: array automation applies to random access, + specifications keep tight footprints, and a client may vary the representation + of individual elements over time. See [std.vector] for the extended rationale. + + Because the element storage is at a fixed offset from the array object, the + "base pointer" is [p ,, elems ty n] rather than a value stored in the object; + <>, <> and <> return pointers derived from it. + + # Supported surface + + - element access: <>, <>, <>, <>, <> + - iterators: <>, <>, <>, <> + - capacity: <>, <>, <> + - operations: <>, <> + - special members: copy/move construction, copy/move assignment, destruction + + # Deliberate omissions + + LIMITATION: < >> is covered only in part, because only part + of it is well defined. At [n = 0]: + + - <>, <>, <>, <>, <> and the special + members are well defined and are specified. <> and <> degenerate + to no-ops ([array.members]), and the free <> is explicitly permitted + even for non-swappable <> ([array.special]). + - <>, <>, <>, <> and <> are well defined, but + [array.zero] leaves their value unspecified and requires only that they + agree. We commit to libstdc++'s null pointer; see the note on the + pointer-returning members below. + - <>, <> and <> violate a hardened precondition + ([sequence.reqmts]), hence are undefined on a non-hardened implementation + and terminate on a hardened one ([structure.specifications]). They carry + [0 < n] individually and so are unusable, rather than wrong, at [n = 0]. + - <> is well defined at [n = 0]: it throws <> + ([sequence.reqmts]). Exceptions are not modelled here so only the [0 < n] + path is modeled here. + + LIMITATION: the reverse iterators <>, <>, <> and + <> are omitted: they return <>, which this + library does not specify yet. + + LIMITATION: the default constructor and aggregate initialization are omitted. + Default-initializing a <> of trivially default constructible + elements leaves them uninitialized while value-initialization zeroes them, and + separating those two cases needs a triviality side-condition we cannot state + yet. Aggregate initialization does not call a constructor and is handled by + BRiCk's initialization automation rather than by a specification here. + + LIMITATION: exceptions are not modelled, so <> is specified only on its + in-range path even though it is defined to throw <> + otherwise. This matches the <> specification. + + LIMITATION: the non-member interface is omitted: <>, the three-way + comparison < >>, <>, <>, the + <> overload, and the tuple interface (<>, + <>). + + NOTE: because the iterators are raw pointers, a loop condition such as + <> is a builtin pointer comparison between two distinct + pointers into the same array. The current automation cannot discharge the + resulting [ptr_comparable] side condition, so client loops over a + <> should iterate by index (<>) rather than by iterator. + See the smoke tests in <> for a verified index loop. + + Reference: + - https://eel.is/c++draft/array + - https://en.cppreference.com/w/cpp/container/array + *) + + #[global] Abbreviation N ty n := + (Ninst "std::array" [Atype ty; Avalue (Eint n "unsigned long")]) (only parsing). + #[global] Abbreviation T ty n := (Tnamed (N ty n)) (only parsing). + + (** <::size_type>>, i.e. <>. *) + #[global] Abbreviation size_type := ("unsigned long"%cpp_type) (only parsing). + (** <::difference_type>>, i.e. <>. + + NOTE: this must be spelled with a builtin type name. The <> notation + has no <> (or <>) keyword, so <<"ptrdiff_t">> parses as the + named type [Tnamed (Nglobal (Nid "ptrdiff_t"))] rather than as an integer type, + which matches nothing in the AST. Both spellings here are LP64-specific, as is + the rest of this file. *) + #[global] Abbreviation difference_type := ("long"%cpp_type) (only parsing). + + (** The offset from a < >> object to its element storage. + + NOTE: this is libstdc++-specific: <<_M_elems>> is the (only) data member of + <> in libstdc++, and it has type <> whenever [n] is positive. + + At [n = 0] the member still exists, at offset 0, but its type is the empty + <> <<__array_traits::_Type>> rather than an array, so this offset + does not denote element storage. Nothing below reads elements at [n = 0]: + [R_gen]'s slice is empty there, and the pointer-returning members do not derive + their result from this offset. *) + #[global] Abbreviation elems ty n := (_field (N ty n .:: Nid "_M_elems")) (only parsing). + (** [spineR ty n q] owns the shape of a < >> object: the + <> identity that ties the inline element storage to the array object, + but none of the element payloads. + + Because <> stores its elements inline, the spine carries no data: + for [0 < n] the address of the storage is [p ,, elems ty n] for an array at [p], + and the number of elements is fixed by [n] (hence by the type). + + The [0 ≤ n] conjunct records that [n] models a <> template + argument. It is deliberately not [0 < n]: the zero-length case is partly well + defined, so the members that have a meaning at [n = 0] are specified here, and + the ones that do not carry [0 < n] themselves. See the LIMITATION on + < >> above. *) + sl.lock + Definition spineR `{Σ : cpp_logic} {σ : genv} (ty : type) (n : Z) (q : cQp.t) : Rep := + structR (N ty n) q ** [| 0 ≤ n |]. + #[only(lazy_unfold,type_ptr,cfractional,ascfractional,cfracvalid)] derive spineR. + + (** [R_gen ty n q Rpayload xs] owns a whole < >>: its spine + together with its [n] elements [xs], each described by [Rpayload]. + + Splitting the spine from the payload lets clients keep tight footprints and + vary the representation of individual elements over time, exactly as for + <>; see [std.vector] for the rationale. *) + #[global] Abbreviation R_gen ty n q Rpayload xs := + (spineR ty n q ** elems ty n |-> array_sliceR ty 0 n Rpayload xs)%I + (ty in scope cpp_type_scope, n in scope Z_scope, q in scope cQp_scope). + + (** [R ty n q xs] is the default ownership of a < >> holding [xs], + using the [BundledRep] of [ty] for the elements. *) + #[global] Abbreviation R ty n q xs := (R_gen ty n q (objR ty q) xs) + (ty in scope cpp_type_scope, n in scope Z_scope, q in scope cQp_scope). + + (** A < >> is modelled by the list of its elements, so it can be + used as the element type of another container (including another + <>). *) + #[global] Instance array_BundledRep `{Σ : cpp_logic} {σ : genv} ty n `{!BundledRep ty V} : + BundledRep (T ty n) (list V) := {| objR := fun q xs => R ty n q xs |}. + + (** Value-initializing a < >> value-initializes each element + ([array.overview]); this is the model of <{} >>, and it is + what containers of arrays use when they need a default element. *) + #[global] Instance array_DefaultValue ty n `{!DefaultValue ty V} : + DefaultValue (T ty n) (list V) := + {| default_val := replicateZ n (default_val ty) |}. + + (** Moving a < >> moves each element, so the moved-from array + has the same length and its elements are element-wise moved-from. *) + #[global] Instance array_MovedValue ty n `{!MovedValue ty V} : + MovedValue (T ty n) (list V) := + {| moved := Forall2 (moved ty) |}. + + Section with_RepFor. + Import rep.RepFor. + Import RepScheme. + + #[global] Instance repfor `{Σ : cpp_logic} {σ : genv} ty n `(_ : BundledRep ty M) : + rep.RepFor.C (T ty n) + [ArgType.CFrac; ArgType.Model _] + (λ q xs, R ty n q xs) := {}. + End with_RepFor. + + Section with_cpp. + Context `{Σ : cpp_logic, σ : genv}. + Context (ty : type) (n : Z). + + #[local] Abbreviation array := (N ty n) (only parsing). (** < >> *) + #[local] Abbreviation arrayT := (Tnamed array) (only parsing). + #[local] Abbreviation spineR q := (spineR ty n q). + #[local] Abbreviation R q xs := (R ty n q xs). + + (** [basep this] is the address of the element storage of the array at [this]. It + denotes element storage only when [0 < n]; see [elems]. *) + #[local] Abbreviation basep this := (this ,, elems ty n). + + (** [beginp this] is the value of <data()>>, <begin()>> and + <cbegin()>>; [endp this] is the value of <end()>> and + <cend()>>. + + For [0 < n] these are the address of the first element and the corresponding + past-the-end pointer. For [n = 0] the standard requires only + <> and leaves the value of <> + unspecified ([array.zero]); libstdc++ returns a null pointer, because the + conversion operator on its empty <<_M_elems>> stand-in is + <>. We + commit to that value, as this library does elsewhere for libstdc++ + representation choices. + + NOTE: both reduce to <> at [n = 0] without any pointer arithmetic, + which is what lets a client conclude <> there. *) + #[local] Abbreviation beginp this := + (if bool_decide (n = 0) then nullptr else (basep this) .[ ty ! 0 ]). + #[local] Abbreviation endp this := + (if bool_decide (n = 0) then nullptr else (basep this) .[ ty ! n ]). + + (** At [n = 0] the two agree, for every [ty], which is exactly the property + [array.zero] guarantees. This holds by construction rather than by any + reasoning about pointers; it is stated so that a change to one of + [beginp]/[endp] and not the other fails here rather than downstream. + + NOTE: the converse — that they differ when [0 < n] — is not provable from + these definitions alone. It needs [same_address_o_sub_eq], i.e. that distinct + indices into an array whose element type has positive size have distinct + addresses. That is the same missing ingredient as the [ptr_comparable] + cancellation hint for <>, so the two are worth doing + together. *) + Lemma beginp_endp_agree_at_zero (this : ptr) : n = 0 -> beginp this = endp this. + Proof. by move=>->. Qed. + + (** <> and <> are [constexpr] and always return [n]. *) + Definition size := + let qf := function_qualifiers.Nc in + specify.template.method array "size" qf size_type [] $ + \this this + \prepost{q} this |-> spineR q + \post[Vint n] emp. + #[global] Hint Opaque size : sl_opacity. + #[global] Arguments size : simpl never. + Definition SpecFor_size := RegisterSpec size. + #[global] Existing Instance SpecFor_size. + + Definition max_size := + let qf := function_qualifiers.Nc in + specify.template.method array "max_size" qf size_type [] $ + \this this + \prepost{q} this |-> spineR q + \post[Vint n] emp. + #[global] Hint Opaque max_size : sl_opacity. + #[global] Arguments max_size : simpl never. + Definition SpecFor_max_size := RegisterSpec max_size. + #[global] Existing Instance SpecFor_max_size. + + (** <> is [constexpr]: it is [true] exactly for < >>. *) + Definition empty := + let qf := function_qualifiers.Nc in + specify.template.method array "empty" qf Tbool [] $ + \this this + \prepost{q} this |-> spineR q + \post[Vbool (bool_decide (n = 0))] emp. + #[global] Hint Opaque empty : sl_opacity. + #[global] Arguments empty : simpl never. + Definition SpecFor_empty := RegisterSpec empty. + #[global] Existing Instance SpecFor_empty. + + (** <> requires [0 ≤ i < n]: out-of-range indices are undefined + behaviour ([array.overview]). *) + Definition subscript c := + let qf := function_qualifiers.mk c false Prvalue in + specify.template.op array OOSubscript qf (Tref (Tconst_if c ty)) [size_type] $ + \this this + \arg{i} "i" (Vint i) + \prepost{q} this |-> spineR q + \require 0 ≤ i < n + \let elemp := (basep this) .[ ty ! i ] + \post[Vref elemp] emp. + #[global] Hint Opaque subscript : sl_opacity. + #[global] Arguments subscript : simpl never. + Definition SpecFor_subscript := RegisterSpec subscript. + #[global] Existing Instance SpecFor_subscript. + + (** LIMITATION: this specification does not discuss exceptions, so <> is + specified only on its in-range path. Out of range, <> throws + <> ([array.members]) rather than being undefined. *) + Definition at_ c := + let qf := function_qualifiers.mk c false Prvalue in + specify.template.method array "at" qf (Tref (Tconst_if c ty)) [size_type] $ + \this this + \arg{i} "i" (Vint i) + \prepost{q} this |-> spineR q + \require 0 ≤ i < n + \let elemp := (basep this) .[ ty ! i ] + \post[Vref elemp] emp. + #[global] Hint Opaque at_ : sl_opacity. + #[global] Arguments at_ : simpl never. + Definition SpecFor_at_ := RegisterSpec at_. + #[global] Existing Instance SpecFor_at_. + + (** <> and <> carry the hardened precondition <> + ([sequence.reqmts]), so on an empty array they are undefined on a + non-hardened implementation and terminate on a hardened one + ([structure.specifications]). Either way there is nothing to specify, hence + the [0 < n] below. + + NOTE: C++17 said this directly in [array.zero]; that sentence is gone and the + requirement now reaches <> through the sequence container tables + ([array.overview]). In libstdc++ both members are <<_M_elems[…]>>, and + indexing the empty <<_M_elems>> stand-in is <<__builtin_trap()>>. *) + Definition front c := + let qf := function_qualifiers.mk c false Prvalue in + specify.template.method array "front" qf (Tref (Tconst_if c ty)) [] $ + \this this + \prepost{q} this |-> spineR q + \require 0 < n + \let elemp := (basep this) .[ ty ! 0 ] + \post[Vref elemp] emp. + #[global] Hint Opaque front : sl_opacity. + #[global] Arguments front : simpl never. + Definition SpecFor_front := RegisterSpec front. + #[global] Existing Instance SpecFor_front. + + Definition back c := + let qf := function_qualifiers.mk c false Prvalue in + specify.template.method array "back" qf (Tref (Tconst_if c ty)) [] $ + \this this + \prepost{q} this |-> spineR q + \require 0 < n + \let elemp := (basep this) .[ ty ! n - 1 ] + \post[Vref elemp] emp. + #[global] Hint Opaque back : sl_opacity. + #[global] Arguments back : simpl never. + Definition SpecFor_back := RegisterSpec back. + #[global] Existing Instance SpecFor_back. + + (** In libstdc++ <>'s <> and <> are the raw + pointer types <> and <>, so <>, <> and + <> all return plain pointers into the element storage and need no + separate iterator representation predicate. *) + Definition data c := + let qf := function_qualifiers.mk c false Prvalue in + specify.template.method array "data" qf (Tptr (Tconst_if c ty)) [] $ + \this this + \prepost{q} this |-> spineR q + \post[Vptr (beginp this)] emp. + #[global] Hint Opaque data : sl_opacity. + #[global] Arguments data : simpl never. + Definition SpecFor_data := RegisterSpec data. + #[global] Existing Instance SpecFor_data. + + Definition begin_spec c := + let qf := function_qualifiers.mk c false Prvalue in + specify.template.method array "begin" qf (Tptr (Tconst_if c ty)) [] $ + \this this + \prepost{q} this |-> spineR q + \post[Vptr (beginp this)] emp. + #[global] Hint Opaque begin_spec : sl_opacity. + #[global] Arguments begin_spec : simpl never. + Definition SpecFor_begin_spec := RegisterSpec begin_spec. + #[global] Existing Instance SpecFor_begin_spec. + + Definition end_spec c := + let qf := function_qualifiers.mk c false Prvalue in + specify.template.method array "end" qf (Tptr (Tconst_if c ty)) [] $ + \this this + \prepost{q} this |-> spineR q + \post[Vptr (endp this)] emp. + #[global] Hint Opaque end_spec : sl_opacity. + #[global] Arguments end_spec : simpl never. + Definition SpecFor_end_spec := RegisterSpec end_spec. + #[global] Existing Instance SpecFor_end_spec. + + Definition cbegin_spec := + let qf := function_qualifiers.Nc in + specify.template.method array "cbegin" qf (Tptr (Tconst ty)) [] $ + \this this + \prepost{q} this |-> spineR q + \post[Vptr (beginp this)] emp. + #[global] Hint Opaque cbegin_spec : sl_opacity. + #[global] Arguments cbegin_spec : simpl never. + Definition SpecFor_cbegin_spec := RegisterSpec cbegin_spec. + #[global] Existing Instance SpecFor_cbegin_spec. + + Definition cend_spec := + let qf := function_qualifiers.Nc in + specify.template.method array "cend" qf (Tptr (Tconst ty)) [] $ + \this this + \prepost{q} this |-> spineR q + \post[Vptr (endp this)] emp. + #[global] Hint Opaque cend_spec : sl_opacity. + #[global] Arguments cend_spec : simpl never. + Definition SpecFor_cend_spec := RegisterSpec cend_spec. + #[global] Existing Instance SpecFor_cend_spec. + + Section with_element_rep. + Context `{!BundledRep ty V}. + + (** <> assigns [u] to every element ([array.fill]). *) + Definition fill := + let qf := function_qualifiers.N in + specify.template.method array "fill" qf Tvoid [Tref (Tconst ty)] $ + \this this + \arg{vp} "u" (Vref vp) + \prepost{q v} vp |-> objR ty q v + \pre{xs} this |-> R (cQp.m 1) xs + \post this |-> R (cQp.m 1) (replicateZ n v). + #[global] Hint Opaque fill : sl_opacity. + #[global] Arguments fill : simpl never. + Definition SpecFor_fill := RegisterSpec fill. + #[global] Existing Instance SpecFor_fill. + + (** <> exchanges the elements of the two arrays ([array.swap]). + Unlike <>, it is linear in [n] and does not exchange + storage, so element addresses are unchanged on both sides. *) + Definition swap := + let qf := function_qualifiers.N in + specify.template.method array "swap" qf Tvoid [Tref arrayT] $ + \this this + \arg{otherp} "other" (Vref otherp) + \with xs ys + \pre this |-> R (cQp.m 1) xs ** otherp |-> R (cQp.m 1) ys + \post this |-> R (cQp.m 1) ys ** otherp |-> R (cQp.m 1) xs. + #[global] Hint Opaque swap : sl_opacity. + #[global] Arguments swap : simpl never. + Definition SpecFor_swap := RegisterSpec swap. + #[global] Existing Instance SpecFor_swap. + End with_element_rep. + + (** ** Special member functions + + <> is an aggregate, so all of its special member functions are + implicitly defined and act element-wise ([array.overview]). *) + Section special_members. + Context `{!BundledRep ty V}. + + Definition copy_ctor := + specify.template.ctor array [Tref (Tconst arrayT)] $ + \this this + \arg{otherp} "other" (Vref otherp) + \prepost{q__other xs} otherp |-> R q__other xs + \post this |-> R (cQp.m 1) xs. + #[global] Hint Opaque copy_ctor : sl_opacity. + #[global] Arguments copy_ctor : simpl never. + Definition SpecFor_copy_ctor := RegisterSpec copy_ctor. + #[global] Existing Instance SpecFor_copy_ctor. + + Definition copy_assign := + let qf := function_qualifiers.N in + specify.template.op array OOEqual qf (Tref arrayT) [Tref (Tconst arrayT)] $ + \this this + \arg{otherp} "other" (Vref otherp) + \prepost{q__other ys} otherp |-> R q__other ys + \pre{xs} this |-> R (cQp.m 1) xs + \post[Vref this] this |-> R (cQp.m 1) ys. + #[global] Hint Opaque copy_assign : sl_opacity. + #[global] Arguments copy_assign : simpl never. + Definition SpecFor_copy_assign := RegisterSpec copy_assign. + #[global] Existing Instance SpecFor_copy_assign. + + Definition dtor := + specify.template.dtor array $ + \this this + \pre{xs} this |-> R (cQp.m 1) xs + \post emp. + #[global] Hint Opaque dtor : sl_opacity. + #[global] Arguments dtor : simpl never. + Definition SpecFor_dtor := RegisterSpec dtor. + #[global] Existing Instance SpecFor_dtor. + End special_members. + + Section move_members. + Context `{!BundledRep ty V, !MovedValue ty V}. + + (** [R_moved q xs] owns an array whose elements are each in the moved-from + state corresponding to the matching element of [xs]. Moving a + <> moves the elements: it does not steal storage, so [other] + keeps its size and its element addresses ([array.overview]). *) + #[local] Abbreviation R_moved q xs := + (R_gen ty n q (fun x => moved_objR ty q x) xs) + (q in scope cQp_scope). + + Definition move_ctor := + specify.template.ctor array [Trv_ref arrayT] $ + \this this + \arg{otherp} "other" (Vref otherp) + \pre{xs} otherp |-> R (cQp.m 1) xs + \post* otherp |-> R_moved (cQp.m 1) xs + \post this |-> R (cQp.m 1) xs. + #[global] Hint Opaque move_ctor : sl_opacity. + #[global] Arguments move_ctor : simpl never. + Definition SpecFor_move_ctor := RegisterSpec move_ctor. + #[global] Existing Instance SpecFor_move_ctor. + + Definition move_assign := + let qf := function_qualifiers.N in + specify.template.op array OOEqual qf (Tref arrayT) [Trv_ref arrayT] $ + \this this + \arg{otherp} "other" (Vref otherp) + \with xs ys + \pre otherp |-> R (cQp.m 1) ys + \post* otherp |-> R_moved (cQp.m 1) ys + \pre this |-> R (cQp.m 1) xs + \post[Vref this] this |-> R (cQp.m 1) ys. + #[global] Hint Opaque move_assign : sl_opacity. + #[global] Arguments move_assign : simpl never. + Definition SpecFor_move_assign := RegisterSpec move_assign. + #[global] Existing Instance SpecFor_move_assign. + End move_members. + + Section specs. + Context `{!BundledRep ty V}. + Context `{!MovedValue ty V}. + + #[local] Abbreviation MaybeConst spec := (spec true ** spec false). + + Definition specs := + size ** + max_size ** + empty ** + MaybeConst subscript ** + MaybeConst at_ ** + MaybeConst front ** + MaybeConst back ** + MaybeConst data ** + MaybeConst begin_spec ** + MaybeConst end_spec ** + cbegin_spec ** + cend_spec ** + fill ** + swap ** + copy_ctor ** + copy_assign ** + dtor ** + move_ctor ** + move_assign. + #[global] Hint Opaque specs : typeclass_instances sl_opacity. + #[only(knowledge)] derive specs. + End specs. + + End with_cpp. + + Section instances_hints. + Context `{Σ : cpp_logic} {σ : genv} (ty : type) (n : Z). + + (** Owning any part of an array's spine witnesses that [n] is a well-formed + extent; see the note on [spineR]. *) + #[global] Instance spineR_nonneg q : Observe [| 0 ≤ n |] (spineR ty n q). + Proof. rewrite spineR.unlock. refine _. Qed. + End instances_hints. + + NES.End array. + +NES.End std. diff --git a/rocq-brick-libstdcpp/proof/dune.inc b/rocq-brick-libstdcpp/proof/dune.inc index 14a82e4b..05306fc7 100644 --- a/rocq-brick-libstdcpp/proof/dune.inc +++ b/rocq-brick-libstdcpp/proof/dune.inc @@ -11,6 +11,18 @@ (with-stderr-to inc_algorithms_cpp.v.stderr (run cpp2v -v %{input} -o inc_algorithms_cpp.v --no-elaborate --templates=inc_algorithms_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps inc_algorithms.cpp)) ) +(subdir array + (rule + (targets inc_array_cpp.v.stderr inc_array_cpp.v inc_array_cpp_templates.v) + (alias test_ast) + (deps + (:input inc_array.cpp) + (env_var CPP2V_DOCKER_ENABLED) + (glob_files_rec ../*.hpp)) + (action + (with-stderr-to inc_array_cpp.v.stderr (run cpp2v -v %{input} -o inc_array_cpp.v --no-elaborate --templates=inc_array_cpp_templates.v -- -std=c++20 -stdlib=libstdc++ )))) + (alias (name srcs) (deps inc_array.cpp)) +) (subdir cassert (rule (targets inc_cassert_cpp.v.stderr inc_cassert_cpp.v inc_cassert_cpp_templates.v) diff --git a/rocq-brick-libstdcpp/test/array/test.cpp b/rocq-brick-libstdcpp/test/array/test.cpp new file mode 100644 index 00000000..588e6289 --- /dev/null +++ b/rocq-brick-libstdcpp/test/array/test.cpp @@ -0,0 +1,180 @@ +/** + * Copyright (c) 2026 SkyLabs AI, Inc. + * This software is distributed under the terms of the BedRock Open-Source License. + * See the LICENSE-BedRock file in the repository root for details. + */ +#include +#include +#include + +using namespace std; + +void +test(bool b) { + assert(b); +} + +/* --- element access -------------------------------------------------------- */ + +int +Get(const array& a, unsigned long i) { + return a[i]; +} + +void +Set(array& a, unsigned long i, int v) { + a[i] = v; +} + +int +GetAt(const array& a, unsigned long i) { + return a.at(i); +} + +int +Front(const array& a) { + return a.front(); +} + +int +Back(const array& a) { + return a.back(); +} + +const int* +Data(const array& a) { + return a.data(); +} + +/* --- capacity, fixed by the type ------------------------------------------- */ + +unsigned long +Size(const array& a) { + return a.size(); +} + +unsigned long +MaxSize(const array& a) { + return a.max_size(); +} + +bool +Empty(const array& a) { + return a.empty(); +} + +/* --- operations ------------------------------------------------------------ */ + +void +Fill(array& a, int v) { + a.fill(v); +} + +void +Swap(array& a, array& b) { + a.swap(b); +} + +void +AssignTo(array& dst, const array& src) { + dst = src; +} + +void +MoveTo(array& dst, array& src) { + dst = std::move(src); +} + +/* --- iterators are raw pointers for std::array ----------------------------- */ + +int +FirstViaBegin(const array& a) { + return *a.begin(); +} + +int +LastViaEnd(const array& a) { + return *(a.end() - 1); +} + +int +FirstViaCBegin(const array& a) { + return *a.cbegin(); +} + +const int* +CEnd(const array& a) { + return a.cend(); +} + +// Iterating by index. Comparing two raw iterators (<>) is a +// builtin pointer comparison, which the current automation cannot discharge for +// two distinct pointers into the same object; indexing avoids that. +unsigned +SumIndexed(const array& a) { + unsigned r = 0; + for (unsigned long i = 0; i < a.size(); ++i) { + r += a[i]; + } + return r; +} + +/* --- a second instantiation: the same specifications apply ----------------- */ + +unsigned +GetU(const array& a, unsigned long i) { + return a[i]; +} + +unsigned long +SizeU(const array& a) { + return a.size(); +} + +/* --- a nested instantiation ------------------------------------------------ */ + +int +GetNested(const array, 4>& a, unsigned long i, unsigned long j) { + return a[i][j]; +} + +/* --- the zero-length instantiation ------------------------------------------ */ +// < >> is only partly well defined; see the LIMITATION in +// [std.array]. These wrappers cover the members that do have a meaning at zero. +// <>, <> and <> are omitted on purpose: they violate a +// hardened precondition, and in libstdc++ they compile to <<__builtin_trap()>>. + +unsigned long +Size0(const array& a) { + return a.size(); +} + +bool +Empty0(const array& a) { + return a.empty(); +} + +const int* +Data0(const array& a) { + return a.data(); +} + +bool +BeginIsEnd0(const array& a) { + return a.begin() == a.end(); +} + +void +Fill0(array& a, int v) { + a.fill(v); +} + +void +Swap0(array& a, array& b) { + a.swap(b); +} + +int +main() { + return 0; +} diff --git a/rocq-brick-libstdcpp/test/array/test_cpp_proof.v b/rocq-brick-libstdcpp/test/array/test_cpp_proof.v new file mode 100644 index 00000000..132fb6a9 --- /dev/null +++ b/rocq-brick-libstdcpp/test/array/test_cpp_proof.v @@ -0,0 +1,442 @@ +(* + * Copyright (c) 2026 SkyLabs AI, Inc. + * This software is distributed under the terms of the BedRock Open-Source License. + * See the LICENSE-BedRock file in the repository root for details. + *) +Require Import skylabs.auto.cpp.prelude.test. + +Require Import skylabs.brick.libstdcpp.array.spec. +Require Import skylabs.brick.libstdcpp.cassert.spec. +Require Import skylabs.brick.libstdcpp.test.array.test_cpp. +(** + Smoke tests for [std.array]. Every wrapper below is verified against the same + set of template specifications, instantiated at < >>, + < >>, the nested <, 4> >> + and the zero-length < >>. + *) + +Section with_cpp. + Context `{Σ : cpp_logic} `{MOD : source ⊧ σ}. + + #[local] Open Scope Z_scope. + + (** Pointer arithmetic on the raw-pointer iterators of <> produces + nested offsets such as <<.[int ! 3].[int ! -1]>>; [normalize_ptr] folds them. *) + Import normalize.normalize_ptr. + + Definition sum (xs : list Z) : Z := foldr Z.add 0 xs. + #[global] Arguments sum !_ / : simpl nomatch. + + (** [go] reduces an element read to a successful [!!] lookup; the specifications + below state the result with the total lookup [!!!]. *) + #[local] Ltac lookup_total := + repeat match goal with + | H : _ !! _ = Some _ |- _ => rewrite (lookup_total_correct _ _ _ H) + end. + + (** ** Capacity + + <>, <> and <> are fixed by the type. *) + + cpp.spec "Size(const std::array&)" as size_spec with + (\arg{ap} "a" (Vref ap) + \prepost{q xs} ap |-> std.array.R "int" 3 q xs + \post[Vint 3] emp). + + Lemma size_ok : verify[ source ] size_spec. + Proof using MOD. verify_spec; go. Qed. + + cpp.spec "MaxSize(const std::array&)" as max_size_spec with + (\arg{ap} "a" (Vref ap) + \prepost{q xs} ap |-> std.array.R "int" 3 q xs + \post[Vint 3] emp). + + Lemma max_size_ok : verify[ source ] max_size_spec. + Proof using MOD. verify_spec; go. Qed. + + cpp.spec "Empty(const std::array&)" as empty_spec with + (\arg{ap} "a" (Vref ap) + \prepost{q xs} ap |-> std.array.R "int" 3 q xs + \post[Vbool false] emp). + + Lemma empty_ok : verify[ source ] empty_spec. + Proof using MOD. verify_spec; go. Qed. + + (** ** Element access *) + + cpp.spec "Get(const std::array&, unsigned long)" as get_spec with + (\arg{ap} "a" (Vref ap) + \arg{i} "i" (Vint i) + \require 0 ≤ i < 3 + \prepost{q xs} ap |-> std.array.R "int" 3 q xs + \post[Vint (xs !!! i)] emp). + + Lemma get_ok : verify[ source ] get_spec. + Proof using MOD. verify_spec; go. by lookup_total. Qed. + + (** Writing through <> is stated with the tight footprint the + specification is designed for: the spine plus the single element being + written, rather than the whole array. *) + cpp.spec "Set(std::array&, unsigned long, int)" as set_spec with + (\arg{ap} "a" (Vref ap) + \arg{i} "i" (Vint i) + \arg{v} "v" (Vint v) + \require 0 ≤ i < 3 + \prepost{q} ap |-> std.array.spineR "int" 3 q + \let basep := ap ,, std.array.elems "int" 3 + \pre{x} basep .[ "int" ! i ] |-> intR 1$m x + \post basep .[ "int" ! i ] |-> intR 1$m v). + + Lemma set_ok : verify[ source ] set_spec. + Proof using MOD. verify_spec; go. Qed. + + (** Only the in-range path of <> is specified; see [std.array]. *) + cpp.spec "GetAt(const std::array&, unsigned long)" as get_at_spec with + (\arg{ap} "a" (Vref ap) + \arg{i} "i" (Vint i) + \require 0 ≤ i < 3 + \prepost{q xs} ap |-> std.array.R "int" 3 q xs + \post[Vint (xs !!! i)] emp). + + Lemma get_at_ok : verify[ source ] get_at_spec. + Proof using MOD. verify_spec; go. by lookup_total. Qed. + + cpp.spec "Front(const std::array&)" as front_spec with + (\arg{ap} "a" (Vref ap) + \prepost{q xs} ap |-> std.array.R "int" 3 q xs + \post[Vint (xs !!! 0)] emp). + + Lemma front_ok : verify[ source ] front_spec. + Proof using MOD. verify_spec; go. Qed. + + cpp.spec "Back(const std::array&)" as back_spec with + (\arg{ap} "a" (Vref ap) + \with q xs x + \prepost ap |-> std.array.R "int" 3 q (xs ++ [x]) + \post[Vint x] emp). + + Lemma back_ok : verify[ source ] back_spec. + Proof using MOD. verify_spec; go. Qed. + + cpp.spec "Data(const std::array&)" as data_spec with + (\arg{ap} "a" (Vref ap) + \prepost{q xs} ap |-> std.array.R "int" 3 q xs + \post[Vptr ((ap ,, std.array.elems "int" 3) .[ "int" ! 0 ])] emp). + + Lemma data_ok : verify[ source ] data_spec. + Proof using MOD. verify_spec; go. Qed. + + (** ** Operations *) + + cpp.spec "Fill(std::array&, int)" as fill_spec with + (\arg{ap} "a" (Vref ap) + \arg{v} "v" (Vint v) + \pre{xs} ap |-> std.array.R "int" 3 1$m xs + \post ap |-> std.array.R "int" 3 1$m (replicateZ 3 v)). + + Lemma fill_ok : verify[ source ] fill_spec. + Proof using MOD. verify_spec; go. Qed. + + cpp.spec "Swap(std::array&, std::array&)" as swap_spec with + (\arg{ap} "a" (Vref ap) + \arg{bp} "b" (Vref bp) + \with xs ys + \pre ap |-> std.array.R "int" 3 1$m xs ** bp |-> std.array.R "int" 3 1$m ys + \post ap |-> std.array.R "int" 3 1$m ys ** bp |-> std.array.R "int" 3 1$m xs). + + Lemma swap_ok : verify[ source ] swap_spec. + Proof using MOD. verify_spec; go. Qed. + + cpp.spec "AssignTo(std::array&, const std::array&)" as assign_to_spec with + (\arg{dstp} "dst" (Vref dstp) + \arg{srcp} "src" (Vref srcp) + \prepost{q ys} srcp |-> std.array.R "int" 3 q ys + \pre{xs} dstp |-> std.array.R "int" 3 1$m xs + \post dstp |-> std.array.R "int" 3 1$m ys). + + Lemma assign_to_ok : verify[ source ] assign_to_spec. + Proof using MOD. verify_spec; go. Qed. + + (** <> is only a cast; inline it so the move assignment is reached. *) + cpp.spec "std::move&>(std::array&)" from source inline. + + (** [moved "int"] is equality, so a moved-from < >> keeps its + element values and only ownership moves. The rewrite below discharges that: + [go] leaves the moved-from payload [∃ x', [| x = x' |] ** intR q x'], which + does not collapse to [intR q x] automatically. *) + cpp.spec "MoveTo(std::array&, std::array&)" as move_to_spec with + (\arg{dstp} "dst" (Vref dstp) + \arg{srcp} "src" (Vref srcp) + \with xs ys + \pre dstp |-> std.array.R "int" 3 1$m xs ** srcp |-> std.array.R "int" 3 1$m ys + \post dstp |-> std.array.R "int" 3 1$m ys ** srcp |-> std.array.R "int" 3 1$m ys). + + Lemma move_to_ok : verify[ source ] move_to_spec. + Proof using MOD. + verify_spec; go. + have Hm : forall (q0 : cQp.t) (y : Z), + (Exists y2 : Z, [| y = y2 |] ** intR q0 y2) -|- intR q0 y. + { intros q0 y; iSplit. + - by iIntros "(%y2 & -> & $)". + - iIntros "H"; iExists y; iSplitR; [ by iIntros "!%" | iFrame ]. } + setoid_rewrite Hm. go. + Qed. + + (** ** Iterators + + <>'s iterators are raw pointers in libstdc++, so they need no + representation predicate of their own. *) + + cpp.spec "FirstViaBegin(const std::array&)" as first_via_begin_spec with + (\arg{ap} "a" (Vref ap) + \prepost{q xs} ap |-> std.array.R "int" 3 q xs + \post[Vint (xs !!! 0)] emp). + + Lemma first_via_begin_ok : verify[ source ] first_via_begin_spec. + Proof using MOD. verify_spec; go. Qed. + + cpp.spec "FirstViaCBegin(const std::array&)" as first_via_cbegin_spec with + (\arg{ap} "a" (Vref ap) + \prepost{q xs} ap |-> std.array.R "int" 3 q xs + \post[Vint (xs !!! 0)] emp). + + Lemma first_via_cbegin_ok : verify[ source ] first_via_cbegin_spec. + Proof using MOD. verify_spec; go. Qed. + + cpp.spec "CEnd(const std::array&)" as cend_spec with + (\arg{ap} "a" (Vref ap) + \prepost{q xs} ap |-> std.array.R "int" 3 q xs + \post[Vptr ((ap ,, std.array.elems "int" 3) .[ "int" ! 3 ])] emp). + + Lemma cend_ok : verify[ source ] cend_spec. + Proof using MOD. verify_spec; go. Qed. + + cpp.spec "LastViaEnd(const std::array&)" as last_via_end_spec with + (\arg{ap} "a" (Vref ap) + \with q xs x + \prepost ap |-> std.array.R "int" 3 q (xs ++ [x]) + \post[Vint x] emp). + + Lemma last_via_end_ok : verify[ source ] last_via_end_spec. + Proof using MOD. + verify_spec; go. + rewrite !o_sub_sub /=. go. + Qed. + + (** ** Iterating over an array + + The loop invariant keeps the yet-to-be-summed suffix [k, 5) of the array, in + the style of the <> smoke tests. *) + + cpp.spec "SumIndexed(const std::array&)" as sum_indexed_spec with + (\arg{ap} "a" (Vref ap) + \prepost{q xs} ap |-> std.array.R "unsigned" 5 q xs + \post[Vint (trim 32 (sum xs))] emp). + + Lemma sum_indexed_ok : verify[ source ] sum_indexed_spec. + Proof using MOD. + verify_spec; go. + wp_for (fun _ => + \with k + \require 0 ≤ k ≤ 5 + \prepost ap |-> std.array.spineR "unsigned int" 5 q + \prepost a_addr |-> refR<"std::array"> 1$m ap + \prepost{ys} (ap ,, std.array.elems "unsigned int" 5) + |-> array_sliceR "unsigned int" k 5 (fun v => uintR q v) ys + \pre i_addr |-> ulongR 1$m k + \pre{r} r_addr |-> uintR 1$m r + \post + r_addr |-> uintR 1$m (trim 32 (r + sum ys)) ** + i_addr |-> ulongR 1$m 5). + iExists 0, xs, 0. go. + wp_if. + all: go. + Qed. + + (** ** Other instantiations + + The same template specifications cover a different element type and extent, + and <> nested inside itself. *) + + cpp.spec "GetU(const std::array&, unsigned long)" as get_u_spec with + (\arg{ap} "a" (Vref ap) + \arg{i} "i" (Vint i) + \require 0 ≤ i < 5 + \prepost{q xs} ap |-> std.array.R "unsigned" 5 q xs + \post[Vint (xs !!! i)] emp). + + Lemma get_u_ok : verify[ source ] get_u_spec. + Proof using MOD. verify_spec; go. by lookup_total. Qed. + + cpp.spec "SizeU(const std::array&)" as size_u_spec with + (\arg{ap} "a" (Vref ap) + \prepost{q xs} ap |-> std.array.R "unsigned" 5 q xs + \post[Vint 5] emp). + + Lemma size_u_ok : verify[ source ] size_u_spec. + Proof using MOD. verify_spec; go. Qed. + + cpp.spec "GetNested(const std::array, 4ul>&, unsigned long, unsigned long)" + as get_nested_spec with + (\arg{ap} "a" (Vref ap) + \arg{i} "i" (Vint i) + \arg{j} "j" (Vint j) + \require 0 ≤ i < 4 + \require 0 ≤ j < 2 + \prepost{q xss} ap |-> std.array.R (std.array.T "int" 2) 4 q xss + \post[Vint ((xss !!! i) !!! j)] emp). + + Lemma get_nested_ok : verify[ source ] get_nested_spec. + Proof using MOD. verify_spec; go. by lookup_total. Qed. + + (** ** Remaining entry points *) + + cpp.spec "test(bool)" as test_spec with + (\arg "b" (Vbool true) + \post emp). + + Lemma test_ok : verify[ source ] test_spec. + Proof using MOD. verify_spec; go. Qed. + + cpp.spec "main()" as main_spec with (\post[Vint 0] emp). + + Lemma main_ok : verify[ source ] main_spec. + Proof using MOD. verify_spec; go. Qed. + + + (** ** The zero-length instantiation + + < >> is only partly well defined; see the LIMITATION in + [std.array]. These clients cover the members that do have a meaning at zero. + <>, <> and <> are absent by design: they violate a + hardened precondition ([sequence.reqmts]) and carry [0 < n], so no client can + use them. *) + + cpp.spec "Size0(const std::array&)" as size0_spec with + (\arg{ap} "a" (Vref ap) + \prepost{q} ap |-> std.array.spineR "int" 0 q + \post[Vint 0] emp). + + Lemma size0_ok : verify[ source ] size0_spec. + Proof using MOD. verify_spec; go. Qed. + + cpp.spec "Empty0(const std::array&)" as empty0_spec with + (\arg{ap} "a" (Vref ap) + \prepost{q} ap |-> std.array.spineR "int" 0 q + \post[Vbool true] emp). + + Lemma empty0_ok : verify[ source ] empty0_spec. + Proof using MOD. verify_spec; go. Qed. + + (** [array.zero] leaves the value of <> unspecified; libstdc++ returns a + null pointer and [std.array] commits to that. *) + cpp.spec "Data0(const std::array&)" as data0_spec with + (\arg{ap} "a" (Vref ap) + \prepost{q} ap |-> std.array.spineR "int" 0 q + \post[Vptr nullptr] emp). + + Lemma data0_ok : verify[ source ] data0_spec. + Proof using MOD. verify_spec; go. Qed. + + (** <> is what [array.zero] does guarantee, and it is the reason + to pin the value at all. *) + cpp.spec "BeginIsEnd0(const std::array&)" as begin_is_end0_spec with + (\arg{ap} "a" (Vref ap) + \prepost{q} ap |-> std.array.spineR "int" 0 q + \post[Vbool true] emp). + + Lemma begin_is_end0_ok : verify[ source ] begin_is_end0_spec. + Proof using MOD. verify_spec; go. Qed. + + (** <> and <> degenerate to no-ops at zero ([array.members]). *) + cpp.spec "Fill0(std::array&, int)" as fill0_spec with + (\arg{ap} "a" (Vref ap) + \arg{v} "v" (Vint v) + \pre ap |-> std.array.R "int" 0 1$m [] + \post ap |-> std.array.R "int" 0 1$m []). + + Lemma fill0_ok : verify[ source ] fill0_spec. + Proof using MOD. verify_spec; go. Qed. + + cpp.spec "Swap0(std::array&, std::array&)" as swap0_spec with + (\arg{ap} "a" (Vref ap) + \arg{bp} "b" (Vref bp) + \pre ap |-> std.array.R "int" 0 1$m [] ** bp |-> std.array.R "int" 0 1$m [] + \post ap |-> std.array.R "int" 0 1$m [] ** bp |-> std.array.R "int" 0 1$m []). + + Lemma swap0_ok : verify[ source ] swap0_spec. + Proof using MOD. verify_spec; go. Qed. + + (** ** Linking + + The clients above are proved against the specifications registered by + [std.array]; the bundles [std.array.specs] provide exactly those. *) + + Definition size_B := [LINK] size_ok. + Definition max_size_B := [LINK] max_size_ok. + Definition empty_B := [LINK] empty_ok. + Definition get_B := [LINK] get_ok. + Definition set_B := [LINK] set_ok. + Definition get_at_B := [LINK] get_at_ok. + Definition front_B := [LINK] front_ok. + Definition back_B := [LINK] back_ok. + Definition data_B := [LINK] data_ok. + Definition fill_B := [LINK] fill_ok. + Definition swap_B := [LINK] swap_ok. + Definition assign_to_B := [LINK] assign_to_ok. + Definition move_to_B := [LINK] move_to_ok. + Definition first_via_begin_B := [LINK] first_via_begin_ok. + Definition first_via_cbegin_B := [LINK] first_via_cbegin_ok. + Definition cend_B := [LINK] cend_ok. + Definition last_via_end_B := [LINK] last_via_end_ok. + Definition sum_indexed_B := [LINK] sum_indexed_ok. + Definition get_u_B := [LINK] get_u_ok. + Definition size_u_B := [LINK] size_u_ok. + Definition get_nested_B := [LINK] get_nested_ok. + Definition size0_B := [LINK] size0_ok. + Definition empty0_B := [LINK] empty0_ok. + Definition data0_B := [LINK] data0_ok. + Definition begin_is_end0_B := [LINK] begin_is_end0_ok. + Definition fill0_B := [LINK] fill0_ok. + Definition swap0_B := [LINK] swap0_ok. + Definition test_B := [LINK] test_ok. + Definition main_B := [LINK] main_ok. + + #[local] Hint Resolve + size_B max_size_B empty_B get_B set_B get_at_B front_B back_B data_B + fill_B swap_B assign_to_B move_to_B first_via_begin_B first_via_cbegin_B + cend_B last_via_end_B sum_indexed_B get_u_B size_u_B get_nested_B + size0_B empty0_B data0_B begin_is_end0_B fill0_B swap0_B + test_B main_B : sl_opacity. + + Definition specs := + size_spec ** max_size_spec ** empty_spec ** + get_spec ** set_spec ** get_at_spec ** front_spec ** back_spec ** data_spec ** + fill_spec ** swap_spec ** assign_to_spec ** move_to_spec ** + first_via_begin_spec ** first_via_cbegin_spec ** cend_spec ** last_via_end_spec ** + sum_indexed_spec ** + get_u_spec ** size_u_spec ** get_nested_spec ** + size0_spec ** empty0_spec ** data0_spec ** begin_is_end0_spec ** + fill0_spec ** swap0_spec ** + test_spec ** main_spec. + + (** Every client above is discharged by instantiations of the library bundle + [std.array.specs] plus <>: nothing else about <> is + needed, and nothing in the bundle is missing. *) + + Lemma specs_ok : + denoteModule source ** + □ ▷ ( std.array.specs "int" 0 ** + std.array.specs "int" 2 ** + std.array.specs "int" 3 ** + std.array.specs "unsigned" 5 ** + std.array.specs (std.array.T "int" 2) 4 ** + std.cassert.specs ) + |-- specs. + Proof using MOD. + rewrite /specs /std.array.specs /std.cassert.specs. + work. + Qed. + + +End with_cpp. diff --git a/rocq-brick-libstdcpp/test/dune.inc b/rocq-brick-libstdcpp/test/dune.inc index 57dae3f1..24a0d533 100644 --- a/rocq-brick-libstdcpp/test/dune.inc +++ b/rocq-brick-libstdcpp/test/dune.inc @@ -1,4 +1,16 @@ ; DO NOT EDIT: Generated by "./dune-gen.sh" +(subdir array + (rule + (targets test_cpp.v.stderr test_cpp.v) + (alias test_ast) + (deps + (:input test.cpp) + (env_var CPP2V_DOCKER_ENABLED) + (glob_files_rec ../*.hpp)) + (action + (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (alias (name srcs) (deps test.cpp)) +) (subdir cctype (rule (targets test_cpp.v.stderr test_cpp.v) From f033b74a096f81f0293c8b3a72de6c4f7e04f987 Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Wed, 9 Sep 2026 21:41:27 -0400 Subject: [PATCH 2/4] use `Normalize` to rewrite `!!!` into `!!` --- rocq-brick-libstdcpp/test/array/test_cpp_proof.v | 15 ++++----------- 1 file changed, 4 insertions(+), 11 deletions(-) diff --git a/rocq-brick-libstdcpp/test/array/test_cpp_proof.v b/rocq-brick-libstdcpp/test/array/test_cpp_proof.v index 132fb6a9..9114a492 100644 --- a/rocq-brick-libstdcpp/test/array/test_cpp_proof.v +++ b/rocq-brick-libstdcpp/test/array/test_cpp_proof.v @@ -27,13 +27,6 @@ Section with_cpp. Definition sum (xs : list Z) : Z := foldr Z.add 0 xs. #[global] Arguments sum !_ / : simpl nomatch. - (** [go] reduces an element read to a successful [!!] lookup; the specifications - below state the result with the total lookup [!!!]. *) - #[local] Ltac lookup_total := - repeat match goal with - | H : _ !! _ = Some _ |- _ => rewrite (lookup_total_correct _ _ _ H) - end. - (** ** Capacity <>, <> and <> are fixed by the type. *) @@ -72,7 +65,7 @@ Section with_cpp. \post[Vint (xs !!! i)] emp). Lemma get_ok : verify[ source ] get_spec. - Proof using MOD. verify_spec; go. by lookup_total. Qed. + Proof using MOD. verify_spec; go. Qed. (** Writing through <> is stated with the tight footprint the specification is designed for: the spine plus the single element being @@ -99,7 +92,7 @@ Section with_cpp. \post[Vint (xs !!! i)] emp). Lemma get_at_ok : verify[ source ] get_at_spec. - Proof using MOD. verify_spec; go. by lookup_total. Qed. + Proof using MOD. verify_spec; go. Qed. cpp.spec "Front(const std::array&)" as front_spec with (\arg{ap} "a" (Vref ap) @@ -266,7 +259,7 @@ Section with_cpp. \post[Vint (xs !!! i)] emp). Lemma get_u_ok : verify[ source ] get_u_spec. - Proof using MOD. verify_spec; go. by lookup_total. Qed. + Proof using MOD. verify_spec; go. Qed. cpp.spec "SizeU(const std::array&)" as size_u_spec with (\arg{ap} "a" (Vref ap) @@ -287,7 +280,7 @@ Section with_cpp. \post[Vint ((xss !!! i) !!! j)] emp). Lemma get_nested_ok : verify[ source ] get_nested_spec. - Proof using MOD. verify_spec; go. by lookup_total. Qed. + Proof using MOD. verify_spec; go. Qed. (** ** Remaining entry points *) From 4f8546401b470f77818337a9986140ce105d0cf4 Mon Sep 17 00:00:00 2001 From: Jasper Haag Date: Fri, 11 Sep 2026 14:02:18 -0400 Subject: [PATCH 3/4] test(array): cover std::array construction cases and use Fail Qed for automation gaps --- rocq-brick-libstdcpp/proof/array/spec.v | 15 +- rocq-brick-libstdcpp/test/array/test.cpp | 84 +++++++- .../test/array/test_cpp_proof.v | 199 ++++++++++++++++-- 3 files changed, 275 insertions(+), 23 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/array/spec.v b/rocq-brick-libstdcpp/proof/array/spec.v index b5ab3757..5ee39de3 100644 --- a/rocq-brick-libstdcpp/proof/array/spec.v +++ b/rocq-brick-libstdcpp/proof/array/spec.v @@ -92,10 +92,10 @@ NES.Begin std. NOTE: because the iterators are raw pointers, a loop condition such as <> is a builtin pointer comparison between two distinct - pointers into the same array. The current automation cannot discharge the - resulting [ptr_comparable] side condition, so client loops over a - <> should iterate by index (<>) rather than by iterator. - See the smoke tests in <> for a verified index loop. + pointers into the same array. Which of the resulting side conditions can + be discharged is recorded by [begin_is_not_end_ok] in <> + rather than here, so that it cannot go stale; that file also carries a + verified loop that iterates by index (<>) instead. Reference: - https://eel.is/c++draft/array @@ -231,9 +231,10 @@ NES.Begin std. NOTE: the converse — that they differ when [0 < n] — is not provable from these definitions alone. It needs [same_address_o_sub_eq], i.e. that distinct indices into an array whose element type has positive size have distinct - addresses. That is the same missing ingredient as the [ptr_comparable] - cancellation hint for <>, so the two are worth doing - together. *) + addresses. It is the obligation still left open by + [begin_is_not_end_ok] in <>; the [ptr_comparable] + cancellation that used to accompany it is now discharged by + [ptr_comparable_valid_CX]. *) Lemma beginp_endp_agree_at_zero (this : ptr) : n = 0 -> beginp this = endp this. Proof. by move=>->. Qed. diff --git a/rocq-brick-libstdcpp/test/array/test.cpp b/rocq-brick-libstdcpp/test/array/test.cpp index 588e6289..ea2e572f 100644 --- a/rocq-brick-libstdcpp/test/array/test.cpp +++ b/rocq-brick-libstdcpp/test/array/test.cpp @@ -107,9 +107,16 @@ CEnd(const array& a) { return a.cend(); } -// Iterating by index. Comparing two raw iterators (<>) is a -// builtin pointer comparison, which the current automation cannot discharge for -// two distinct pointers into the same object; indexing avoids that. +// Comparing two raw iterators is a builtin pointer comparison between two +// distinct pointers into the same object. Which of the resulting side conditions +// can be discharged is recorded by the <> test [begin_is_not_end_ok] +// in <>. +bool +BeginIsNotEnd(const array& a) { + return a.begin() != a.end(); +} + +// Iterating by index, which avoids that comparison. unsigned SumIndexed(const array& a) { unsigned r = 0; @@ -131,6 +138,77 @@ SizeU(const array& a) { return a.size(); } +/* --- constructing arrays --------------------------------------------------- */ +// Every client above receives its array as a reference, so nothing there forces +// the representation predicate to be inhabited. These construct one, through the +// copy and the move constructor, at two instantiations. + +int +CopyThenGet(const array& a, unsigned long i) { + array b(a); + return b[i]; +} + +int +MoveThenGet(array& a, unsigned long i) { + array b(std::move(a)); + return b[i]; +} + +unsigned +CopyThenGetU(const array& a, unsigned long i) { + array b(a); + return b[i]; +} + +unsigned +MoveThenGetU(array& a, unsigned long i) { + array b(std::move(a)); + return b[i]; +} + +// Brace initialization of an aggregate calls no constructor: it is handled by +// BRiCk's initialization automation rather than by a specification in +// [std.array]. A full initializer list and an empty one verify; a short list and +// a nested one are pinned by <> tests in <>, because +// the initialization automation does not cover those two forms yet. + +int +BraceInitThenGet(unsigned long i) { + array a{1, 2, 3}; + return a[i]; +} + +int +BraceInitAssignmentThenGet(unsigned long i) { + array a = {1, 2, 3}; + return a[i]; +} + +unsigned +BraceInitThenGetU(unsigned long i) { + array a{1, 2, 3, 4, 5}; + return a[i]; +} + +int +BraceInitPartialThenGet(unsigned long i) { + array a{1}; + return a[i]; +} + +int +BraceInitValueThenGet() { + array a{}; + return a[1]; +} + +int +BraceInitNestedThenGet(unsigned long i, unsigned long j) { + array, 2> a{{{1, 2}, {3, 4}}}; + return a[i][j]; +} + /* --- a nested instantiation ------------------------------------------------ */ int diff --git a/rocq-brick-libstdcpp/test/array/test_cpp_proof.v b/rocq-brick-libstdcpp/test/array/test_cpp_proof.v index 9114a492..f2286f0a 100644 --- a/rocq-brick-libstdcpp/test/array/test_cpp_proof.v +++ b/rocq-brick-libstdcpp/test/array/test_cpp_proof.v @@ -5,6 +5,8 @@ *) Require Import skylabs.auto.cpp.prelude.test. +Require Import skylabs.cpp.string. + Require Import skylabs.brick.libstdcpp.array.spec. Require Import skylabs.brick.libstdcpp.cassert.spec. Require Import skylabs.brick.libstdcpp.test.array.test_cpp. @@ -153,10 +155,18 @@ Section with_cpp. (** <> is only a cast; inline it so the move assignment is reached. *) cpp.spec "std::move&>(std::array&)" from source inline. - (** [moved "int"] is equality, so a moved-from < >> keeps its - element values and only ownership moves. The rewrite below discharges that: - [go] leaves the moved-from payload [∃ x', [| x = x' |] ** intR q x'], which - does not collapse to [intR q x] automatically. *) + (** [moved ty] is equality for the element types used here, so a moved-from + <> keeps its element values and only ownership moves. [go] leaves + that as a payload [∃ x', [| x = x' |] ** Rp x'], which does not collapse to + [Rp x] on its own; this is the rewrite that does it. *) + #[local] Lemma moved_prim_elim (Rp : Z -> Rep) (x : Z) : + (Exists x' : Z, [| x = x' |] ** Rp x') -|- Rp x. + Proof. + iSplit. + - by iIntros "(%x' & -> & $)". + - iIntros "H"; iExists x; iSplitR; [ by iIntros "!%" | iFrame ]. + Qed. + cpp.spec "MoveTo(std::array&, std::array&)" as move_to_spec with (\arg{dstp} "dst" (Vref dstp) \arg{srcp} "src" (Vref srcp) @@ -165,15 +175,7 @@ Section with_cpp. \post dstp |-> std.array.R "int" 3 1$m ys ** srcp |-> std.array.R "int" 3 1$m ys). Lemma move_to_ok : verify[ source ] move_to_spec. - Proof using MOD. - verify_spec; go. - have Hm : forall (q0 : cQp.t) (y : Z), - (Exists y2 : Z, [| y = y2 |] ** intR q0 y2) -|- intR q0 y. - { intros q0 y; iSplit. - - by iIntros "(%y2 & -> & $)". - - iIntros "H"; iExists y; iSplitR; [ by iIntros "!%" | iFrame ]. } - setoid_rewrite Hm. go. - Qed. + Proof using MOD. verify_spec; go. setoid_rewrite moved_prim_elim. go. Qed. (** ** Iterators @@ -216,6 +218,34 @@ Section with_cpp. rewrite !o_sub_sub /=. go. Qed. + (** <>'s iterators are raw pointers, so a condition such as + <> is a builtin pointer comparison between the first and + last element addresses, [p .[ "int" ! 0 ]] and [p .[ "int" ! 3 ]]. + [wp_eval_ptr_neq] splits that into two obligations, and only one of them can + be discharged today: + + - [ptr_comparable] between the two pointers. [ptr_comparable_valid_CX] + (SkyLabsAI/auto#452) proves it. It is passed explicitly because, unlike + [ptr_comparable_cstringR], it is not registered in a hint database. + - the value of the comparison, which [wp_eval_ptr_neq] states as + [bool_decide (p1 <> p2)]. Deciding it means going from pointer equality + back to index equality, which holds only where the pointers have addresses + -- and [valid_ptr] does not give that. [auto]'s [refine1_offset] records + exactly this gap: it is a [Refine1 false true], i.e. complete but not + sound, and is registered only for <>. + + So closing SkyLabsAI/auto#451 needs more than the merged hint, and the loop + below still iterates by index. The <> pins the one remaining + obligation and starts failing once it is closed. *) + + cpp.spec "BeginIsNotEnd(const std::array&)" as begin_is_not_end_spec with + (\arg{ap} "a" (Vref ap) + \prepost{q xs} ap |-> std.array.R "int" 3 q xs + \post[Vbool true] emp). + + Lemma begin_is_not_end_ok : verify[ source ] begin_is_not_end_spec. + Proof using MOD. verify_spec; go using ptr_comparable_valid_CX. Fail Qed. Abort. + (** ** Iterating over an array The loop invariant keeps the yet-to-be-summed suffix [k, 5) of the array, in @@ -282,6 +312,134 @@ Section with_cpp. Lemma get_nested_ok : verify[ source ] get_nested_spec. Proof using MOD. verify_spec; go. Qed. + (** ** Constructing an array + + Every client above receives its array by reference, so none of them forces + [std.array.R] to be inhabited. These do: each builds a fresh array from an + existing one and then reads it back, through the copy and the move + constructor, at two instantiations. *) + + cpp.spec "CopyThenGet(const std::array&, unsigned long)" + as copy_then_get_spec with + (\arg{ap} "a" (Vref ap) + \arg{i} "i" (Vint i) + \require 0 ≤ i < 3 + \prepost{q xs} ap |-> std.array.R "int" 3 q xs + \post[Vint (xs !!! i)] emp). + + Lemma copy_then_get_ok : verify[ source ] copy_then_get_spec. + Proof using MOD. verify_spec; go. Qed. + + cpp.spec "CopyThenGetU(const std::array&, unsigned long)" + as copy_then_get_u_spec with + (\arg{ap} "a" (Vref ap) + \arg{i} "i" (Vint i) + \require 0 ≤ i < 5 + \prepost{q xs} ap |-> std.array.R "unsigned" 5 q xs + \post[Vint (xs !!! i)] emp). + + Lemma copy_then_get_u_ok : verify[ source ] copy_then_get_u_spec. + Proof using MOD. verify_spec; go. Qed. + + cpp.spec "std::move&>(std::array&)" + from source inline. + + (** As in [move_to_ok], the moved-from array keeps its element values; + [moved_prim_elim] collapses the leftover existential. *) + cpp.spec "MoveThenGet(std::array&, unsigned long)" + as move_then_get_spec with + (\arg{ap} "a" (Vref ap) + \arg{i} "i" (Vint i) + \require 0 ≤ i < 3 + \prepost{xs} ap |-> std.array.R "int" 3 1$m xs + \post[Vint (xs !!! i)] emp). + + Lemma move_then_get_ok : verify[ source ] move_then_get_spec. + Proof using MOD. verify_spec; go. setoid_rewrite moved_prim_elim. go. Qed. + + cpp.spec "MoveThenGetU(std::array&, unsigned long)" + as move_then_get_u_spec with + (\arg{ap} "a" (Vref ap) + \arg{i} "i" (Vint i) + \require 0 ≤ i < 5 + \prepost{xs} ap |-> std.array.R "unsigned" 5 1$m xs + \post[Vint (xs !!! i)] emp). + + Lemma move_then_get_u_ok : verify[ source ] move_then_get_u_spec. + Proof using MOD. verify_spec; go. setoid_rewrite moved_prim_elim. go. Qed. + + (** ** Brace initialization + + Aggregate initialization calls no constructor ([array.overview]): the AST + carries an [Einitlist] rather than an [Econstructor], so these clients never + reach [std.array]'s constructor specifications. The representation predicate + has to come out of BRiCk's initialization automation instead, which checks + [std.array.R] against libstdc++'s layout rather than against an assumed + specification. *) + + cpp.spec "BraceInitThenGet(unsigned long)" as brace_init_then_get_spec with + (\arg{i} "i" (Vint i) + \require 0 ≤ i < 3 + \post[Vint ([1; 2; 3] !!! i)] emp). + + Lemma brace_init_then_get_ok : verify[ source ] brace_init_then_get_spec. + Proof using MOD. verify_spec; go. Qed. + + cpp.spec "BraceInitAssignmentThenGet(unsigned long)" as brace_init_assignment_then_get_spec with + (\arg{i} "i" (Vint i) + \require 0 ≤ i < 3 + \post[Vint ([1; 2; 3] !!! i)] emp). + + Lemma brace_init_assignment_then_get_ok : verify[ source ] brace_init_assignment_then_get_spec. + Proof using MOD. verify_spec; go. Qed. + + cpp.spec "BraceInitThenGetU(unsigned long)" as brace_init_then_get_u_spec with + (\arg{i} "i" (Vint i) + \require 0 ≤ i < 5 + \post[Vint ([1; 2; 3; 4; 5] !!! i)] emp). + + Lemma brace_init_then_get_u_ok : verify[ source ] brace_init_then_get_u_spec. + Proof using MOD. verify_spec; go. Qed. + + (** LIMITATION: a short initializer list value-initializes the remaining + elements, which the AST records as an [Einitlist] carrying a filler + ([Eimplicit_init]). The initialization automation does not handle that form + yet, so this is pinned rather than proved. *) + cpp.spec "BraceInitPartialThenGet(unsigned long)" as brace_init_partial_then_get_spec with + (\arg{i} "i" (Vint i) + \require 0 ≤ i < 3 + \post[Vint ([1; 0; 0] !!! i)] emp). + + Lemma brace_init_partial_then_get_ok : verify[ source ] brace_init_partial_then_get_spec. + Proof using MOD. verify_spec; go. Fail Qed. Abort. + + (** < a{}>> value-initializes every element, unlike the omitted + default constructor; see the LIMITATION in [std.array]. *) + cpp.spec "BraceInitValueThenGet()" as brace_init_value_then_get_spec with + (\post[Vint 0] emp). + + (** Value initialization goes through [primR] rather than through the element + type's [BundledRep], hence the explicit hint. The index is a literal here: + with a symbolic one the leftover total lookup ends up in the premise of a + wand, where the [Normalize] hint that handles it elsewhere cannot reach it. *) + Lemma brace_init_value_then_get_ok : verify[ source ] brace_init_value_then_get_spec. + Proof using MOD. verify_spec; go using prim.primR_aggressiveC. Qed. + + cpp.spec "BraceInitNestedThenGet(unsigned long, unsigned long)" + as brace_init_nested_then_get_spec with + (\arg{i} "i" (Vint i) + \arg{j} "j" (Vint j) + \require 0 ≤ i < 2 + \require 0 ≤ j < 2 + \post[Vint (([[1; 2]; [3; 4]] !!! i) !!! j)] emp). + + (** LIMITATION: the nested aggregate initializer is an [Einitlist] of + [Einitlist]s, which the initialization automation does not handle yet. Note + that [get_nested_ok] above does verify reads of a nested array, so it is the + initialization rather than [std.array.R] that is missing here. *) + Lemma brace_init_nested_then_get_ok : verify[ source ] brace_init_nested_then_get_spec. + Proof using MOD. verify_spec; go. Fail Qed. Abort. + (** ** Remaining entry points *) cpp.spec "test(bool)" as test_spec with @@ -386,6 +544,14 @@ Section with_cpp. Definition get_u_B := [LINK] get_u_ok. Definition size_u_B := [LINK] size_u_ok. Definition get_nested_B := [LINK] get_nested_ok. + Definition copy_then_get_B := [LINK] copy_then_get_ok. + Definition copy_then_get_u_B := [LINK] copy_then_get_u_ok. + Definition move_then_get_B := [LINK] move_then_get_ok. + Definition move_then_get_u_B := [LINK] move_then_get_u_ok. + Definition brace_init_then_get_B := [LINK] brace_init_then_get_ok. + Definition brace_init_assignment_then_get_B := [LINK] brace_init_assignment_then_get_ok. + Definition brace_init_then_get_u_B := [LINK] brace_init_then_get_u_ok. + Definition brace_init_value_then_get_B := [LINK] brace_init_value_then_get_ok. Definition size0_B := [LINK] size0_ok. Definition empty0_B := [LINK] empty0_ok. Definition data0_B := [LINK] data0_ok. @@ -399,6 +565,9 @@ Section with_cpp. size_B max_size_B empty_B get_B set_B get_at_B front_B back_B data_B fill_B swap_B assign_to_B move_to_B first_via_begin_B first_via_cbegin_B cend_B last_via_end_B sum_indexed_B get_u_B size_u_B get_nested_B + copy_then_get_B copy_then_get_u_B move_then_get_B move_then_get_u_B + brace_init_then_get_B brace_init_assignment_then_get_B + brace_init_then_get_u_B brace_init_value_then_get_B size0_B empty0_B data0_B begin_is_end0_B fill0_B swap0_B test_B main_B : sl_opacity. @@ -409,6 +578,10 @@ Section with_cpp. first_via_begin_spec ** first_via_cbegin_spec ** cend_spec ** last_via_end_spec ** sum_indexed_spec ** get_u_spec ** size_u_spec ** get_nested_spec ** + copy_then_get_spec ** copy_then_get_u_spec ** + move_then_get_spec ** move_then_get_u_spec ** + brace_init_then_get_spec ** brace_init_assignment_then_get_spec ** + brace_init_then_get_u_spec ** brace_init_value_then_get_spec ** size0_spec ** empty0_spec ** data0_spec ** begin_is_end0_spec ** fill0_spec ** swap0_spec ** test_spec ** main_spec. From 600cbabca21a074cf4d80d285cf02337f1e8188b Mon Sep 17 00:00:00 2001 From: Jasper Haag Date: Mon, 14 Sep 2026 15:00:42 -0400 Subject: [PATCH 4/4] test(array): remove redundant iExists from proof --- rocq-brick-libstdcpp/test/array/test_cpp_proof.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/rocq-brick-libstdcpp/test/array/test_cpp_proof.v b/rocq-brick-libstdcpp/test/array/test_cpp_proof.v index f2286f0a..3389f8e7 100644 --- a/rocq-brick-libstdcpp/test/array/test_cpp_proof.v +++ b/rocq-brick-libstdcpp/test/array/test_cpp_proof.v @@ -271,9 +271,8 @@ Section with_cpp. \post r_addr |-> uintR 1$m (trim 32 (r + sum ys)) ** i_addr |-> ulongR 1$m 5). - iExists 0, xs, 0. go. - wp_if. - all: go. + go. + wp_if; go. Qed. (** ** Other instantiations