diff --git a/rocq-brick-libstdcpp/proof/algorithms/spec.v b/rocq-brick-libstdcpp/proof/algorithms/spec.v new file mode 100644 index 0000000..71e7b1e --- /dev/null +++ b/rocq-brick-libstdcpp/proof/algorithms/spec.v @@ -0,0 +1,97 @@ +(** + * Copyright (C) 2025 SkyLabs AI, Inc. + * All rights reserved. + * + * SPDX-License-Identifier: LGPL-2.1 WITH BlueRock Exception for use over network, see repository root for details. + *) +Require Import skylabs.auto.cpp.spec. +Require Import skylabs.auto.cpp.proof. +Require Import skylabs.cpp.spec.concepts. + +Require Import skylabs.prelude.under_rel_proper. + +Require Import skylabs.cpp.spec.concepts. + +Require Export skylabs.brick.libstdcpp.iterator.spec. + +(* Require Import skylabs.ltac2.extra.internal.constr. *) +(* Require Import skylabs.ltac2.extra.extra. *) + +Section lists. + + Fixpoint list_findZ_from {A} (P : A → Prop) `{!∀ x : A, Decision (P x)} (base : Z) (xs : list A) : option (Z * A) := + match xs with + | [] => None + | x :: xs => + if bool_decide (P x) then + Some (base, x) + else + list_findZ_from P (base + 1) xs + end. + #[global] Arguments list_findZ_from _ _ _ _ !xs /. + + Lemma list_findZ_to_nat {A} (P : A → Prop) `{!∀ x : A, Decision (P x)} base xs : + list_findZ_from P base xs = prod_map (fun i => base + Z.of_nat i)%Z id <$> list_find P xs. + Proof. + elim: xs base => [|x xs IH] base //=. + rewrite bool_decide_decide. + case: decide => [HP|HnP] /=. + - do 2 f_equal; lia. + - rewrite -option_fmap_compose /compose IH. + case: list_find => [[i a]/=|//]. + do 2 f_equal; lia. + Qed. + +End lists. + +#[global] Notation list_findZ P := (list_findZ_from P 0). + +NES.Begin std. + +Section with_cpp. + Context `{Σ : cpp_logic, σ : genv}. + Context (it_ty ty : type). + Implicit Types p : ptr. + Import specify_notation. + + Notation ok := (tFunction "$it_ty" ["$it_ty";"$it_ty";"const $ty &"]%cpp_type). + + Definition find := + specify_notation.specify ok "std::__1::find<$it_ty,$ty>($it_ty,$it_ty,const $ty &)" + ( \\requires{C Iter} BundledRep it_ty (C * Iter)%type + \\requires HasRanges it_ty C Iter + \\requires{V} BundledRep ty V + \\requires EqDecision V + \\with + \with c + \arg{beginp : ptr} "begin" beginp + \prepost{itb} beginp |-> objR it_ty 1$m (c, itb) + + \arg{endp : ptr} "end" endp + \prepost{ite} endp |-> objR it_ty 1$m (c, ite) + + \arg{vpp : ptr} "v" vpp + \prepost{vp : ptr} vpp |-> refR 1$m vp + \prepost{vq v} vp |-> objR ty vq v + + (* spine and payload of the range between `begin` and `end` *) + \prepost{q ps} range it_ty c q itb ps ite + \prepost{objq xs} payload it_ty c (fun x => objR ty objq x) ps xs + \post{retp : ptr}[retp] + ∃ itr, + retp |-> objR it_ty 1$m (c, itr) ** + match list_findZ (eq v) xs with + | Some (i, _) => + lookup_result (ps !! i) itr + | None => [| itr = ite |] + end ). + + Definition find_spec := Hnf (fst find). + Definition find_inst := Hnf (snd find find_spec). + #[global] Hint Opaque find_spec : sl_opacity. + #[global] Arguments find_spec : simpl never. + #[global] Existing Instance find_inst. + +End with_cpp. + +NES.End std. diff --git a/rocq-brick-libstdcpp/proof/allocator/spec.v b/rocq-brick-libstdcpp/proof/allocator/spec.v new file mode 100644 index 0000000..bbaac7b --- /dev/null +++ b/rocq-brick-libstdcpp/proof/allocator/spec.v @@ -0,0 +1,41 @@ +(** + * Copyright (C) 2025 SkyLabs AI, Inc. + * All rights reserved. + * + * SPDX-License-Identifier: LGPL-2.1 WITH BlueRock Exception for use over network, see repository root for details. + *) +Require Import skylabs.auto.cpp.spec. + +Require Import skylabs.cpp.spec.concepts. + +NES.Begin std.allocator_traits. + + Class IsAllocator `{Σ : cpp_logic,σ : genv} (ty : type) := + { size_type : type ; + alloc_state : Set ; + #[global] size_type_is_prim_int :: PrimVal size_type Z ; + #[global] is_RepFor :: BundledRep ty alloc_state ; + }. + Arguments size_type {_ _ _ _} ty {_}. + +NES.End std.allocator_traits. + +NES.Begin std.allocator. + NES.Open allocator_traits. + + #[global] Notation N ty := (Ninst "std::__1::allocator" [Atype ty]). + #[global] Notation T ty := (Tnamed (Ninst "std::__1::allocator" [Atype ty])). + sl.lock Definition R `{Σ : cpp_logic,σ : genv} (ty : type) (q : cQp.t) (_ : ()) : Rep := + structR (N ty) q. + #[only(ascfractional,cfractional,cfracvalid,type_ptr)] derive R. + + #[global] Instance R_agree `{Σ : cpp_logic,σ : genv} ty q1 q2 a1 a2 : Observe2 [| a1 = a2 |] (R ty q1 a1) (R ty q2 a2). + Proof. by destruct a1,a2; apply observe_2_intro_only_provable; iIntros "? ? !%". Qed. + + #[global] Instance R_HasRep `{Σ : cpp_logic,σ : genv} ty : BundledRep (T ty) () := {| objR := R ty |}. + + #[global] Instance is_allocator `{Σ : cpp_logic,σ : genv} (ty : type) : IsAllocator (T ty) := + {| size_type := "unsigned long" ; + alloc_state := () |}. + +NES.End std.allocator. diff --git a/rocq-brick-libstdcpp/proof/dune.inc b/rocq-brick-libstdcpp/proof/dune.inc index 8f61fc1..70c68d9 100644 --- a/rocq-brick-libstdcpp/proof/dune.inc +++ b/rocq-brick-libstdcpp/proof/dune.inc @@ -107,3 +107,12 @@ (with-stderr-to inc_string_cpp.v.stderr (run cpp2v -v %{input} -o inc_string_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps inc_string.cpp)) ) +(subdir vector + (rule + (targets inc_vector_cpp.v.stderr inc_vector_cpp.v) + (alias test_ast) + (deps (:input inc_vector.cpp) (glob_files_rec ../*.hpp) (universe)) + (action + (with-stderr-to inc_vector_cpp.v.stderr (run cpp2v -v %{input} -o inc_vector_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (alias (name srcs) (deps inc_vector.cpp)) +) diff --git a/rocq-brick-libstdcpp/proof/iterator/spec.v b/rocq-brick-libstdcpp/proof/iterator/spec.v new file mode 100644 index 0000000..df9a88f --- /dev/null +++ b/rocq-brick-libstdcpp/proof/iterator/spec.v @@ -0,0 +1,724 @@ +(** + * Copyright (C) 2025 SkyLabs AI, Inc. + * All rights reserved. + * + * SPDX-License-Identifier: LGPL-2.1 WITH BlueRock Exception for use over network, see repository root for details. + *) +Require Import skylabs.auto.cpp.spec. +Require Import skylabs.auto.lazy.big_sep.lemmas. +Require Import skylabs.cpp.spec.concepts. + +Require Import skylabs.prelude.under_rel_proper. + +Require Import skylabs.cpp.slice. +Require Import skylabs.cpp.spec.concepts. + +NES.Begin std. + (** An interface for collection ownership predicates. *) + + Class HasRanges `{Σ : cpp_logic} (ty : type) (C : Set) (V : Type) := + { collection_idT := C ; + dereference : C -> V -> ptr ; + range (c : collection_idT) (q : cQp.t) (begp : V) (ps : list V) (endp : V) : mpred ; + (** + [range iter_ty c q begp ps endp] owns fraction [q] of a collection segment from [begp] (included) to [endp] (excluded). + [ps] is a list of pointers to the collection elements, and [c] is a collection ID. + [range] only owns the collection "spine", not the actual payloads. + *) + range_frac c : CFractional3 (range c) ; + (* TODO: + We omit [CFracValid3 (range c)]: [range] only owns the collection + spine, and for vectors, this corresponds to no physical ownership. + Since we typically own [range c q begp ps endp ** ... ], we can typically derive [q] is valid anyway. *) + obs_range_nil c q s0 s1 : Observe [| s0 = s1 |] (range c q s0 [] s1) ; + obs_range_is_nil c q s ps : Observe [| ps = [] |] (range c q s ps s) ; + obs_range_cons c q s0 s ss s1 : Observe [| s0 = s |] (range c q s0 (s :: ss) s1) ; + range_app c q s0 s2 xs ys : + range c q s0 (xs ++ ys) s2 -|- ∃ s1, range c q s0 xs s1 ∗ range c q s1 ys s2 ; + obs_range_agree_l c st_end xs : AgreeCF1 (fun q s => range c q s xs st_end) ; + obs_range_agree_r c st_start xs : AgreeCF1 (fun q s => range c q st_start xs s) + }. + #[global] Arguments HasRanges {_ _ _} ty C V : assert. + #[global] Hint Mode HasRanges - - - + - - : typeclass_instances. + #[global] Arguments range {_ _ _} ty {C V _} c q begp ps endp : assert. + #[global] Arguments dereference {_ _ _} ty {C V _} c v : assert. + #[global] Arguments collection_idT {_ _ _} ty {C V _} : assert. + + #[global] Hint Opaque range : sl_opacity. + + (** * [payload iter_ty coll R ps vs] + Encapsulates a series objects with [R x] as their [Rep] predicate. + + Provided an instance [HasRanges iter_ty C Iter]m + - iter_ty : type -- type of an iterator; + - coll : C -- identity of source collection; + - R : A -> Rep -- specification of individual objects; + - ps : list Iter -- list of iterator states that can be dereferenced to access individual + objects; + - vs : list A -- list of values zipped with [ps] to specify each object. + *) + sl.lock + Definition payload `{Σ : cpp_logic,σ : genv} {A} + (iter_ty : type) `{!HasRanges iter_ty C Iter} + (coll : C) (R : A -> Rep) (ps : list Iter) (vs : list A) : mpred := + [∗ list] p ; v ∈ ps ; vs, dereference iter_ty coll p |-> R v. + +(** + Iterators and ranges + This file provides abstract predicates to used to specify C++ iterators and ranges. Iterators + and ranges are central ideas in the design of the algorithms in the C++ standard library. + Functions on collections can be made generic by using iterator types or range types. + + + # [HasRanges] + + [HasRanges] uses [range] to specify a list of pointers to consecutive elements of a collection + without specifying what the underlying collection is. A range is delimited by a pair of + pointers. These endpoints can be taken as the state of a begin / end pair of iterators or as the + state of a single C++ range object. + + For example, a function that abstractly reverses the values in a range specified by two iterators + can be specified as follows: + << + Definition reverse_spec {A} (ty iter_ty : type) + `{!RepFor ty A, (* [objR] for the objects contained by the range *) + !RepFor iter_ty (C * It), (* [objR] for the iterators *) + !HasRanges iter_ty C It} := (* [range] where the endpoints are iterators of type [iter_ty] *) + \arg{it_begp} "begin" (Vptr it_begp) + \arg{it_endp} "end" (Vptr it_endp) + (* Ownership of `begin` / `end` iterator objects. *) + \prepost{begp} it_begp |-> objR iter_ty 1$m begp + \prepost{endp} it_endp |-> objR iter_ty 1$m endp + (* Below, [c] is a collection ID, which is shared between a collection and all ranges taken + from it. [ps] is a list of pointers to the objects contained between `[begin,end[`; if + [ps] is non-empty, the first element is [begp] while [endp] is always excluded. + IMPORTANT NOTE: [range] does not own any of the elements of the underlying collection. A + separate term is provided for that purpose. *) + \prepost{c qr ps} range it_ty c qr begp ps endp + \pre{vs} payload iter_ty c (objR ty 1$m) ps vs (* ownership of the elements *) + \post payload iter_ty c (objR ty 1$m) ps (reverse vs) + (* The values of the objects in the range are returned in reversed order. The list of + pointers itself is unchanged which guarantees that the reversal is performed in-place. *) + >> + + In a proof, dereferencing an iterator [itp |-> objR iter_ty q elemp] in the following state: + << + _ : it_begp |-> objR iter_ty 1$m (c, begp) + _ : it_endp |-> objR iter_ty 1$m (c, endp) + _ : itp |-> objR iter_ty 1$m (c, elemp) <---- dereferencing reads this term + _ : range iter_ty c qr begp ps0 elemp + _ : range iter_ty c qr elemp (elemp :: ps1) endp + _ : [∗ list] p; v ∈ elemp :: ps1; vs, + dereference iter_ty c p |-> objR ty q v <---- and gets an object from this term + >> + will yield the pointer [dereference iter_ty c elemp] and big sep automation can be used to gain + access to the corresponding [objR ty] term. + + From that state, incrementing iterator [itp] gets us into the following state: + << + _ : it_begp |-> objR iter_ty 1$m (c, begp) + _ : it_endp |-> objR iter_ty 1$m (c, endp) + _ : itp |-> objR iter_ty 1$m (c, nextp) <---- these terms changed + _ : range iter_ty c qr begp (ps0 ++ [elemp]) nextp <---- + _ : range iter_ty c qr nextp ps1 endp <---- + _ : [∗ list] p; v ∈ elemp :: ps1; vs, + dereference iter_ty c p |-> objR ty q v + >> + + + # [array_spine] + + [array_spine] is the main definition underlying a generic [HasRanges] instance to specify + iterators and ranges for any array-backed collection. + + It is designed to satisfy the equation: + << + basep |-> arrayLR ty i j R vs + -|- + ∃ ps, + array_spine ty basep 1$m i ps j ** + [∗ list] idx; v ∈ ps; vs, basep .[ ty ! idx ] |-> R v + >> + and thus separate a [arrayLR] term into a term that specifies a list of pointers and a different + term to specify the objects that are stored at those pointers. + + NOTE: the listings in this comment are type checked in module [code_snippets]. + + # [lookup_result] + + [lookup_result] is a predicate, provided as an automation gadget for specifications that return a + term of the form [ [| m !! k = Some x |] ]. It helps keep the proposition in the spatial context + long enough for a hint to turn it into something useful. It is possible that the same can be + accomplished without [lookup_result]. + More experimentation needed. + *) + (** + [HasRanges] + Class [HasRanges iter_ty C Iter] defines predicate [range] and related properties for an + iterator type [iter_ty] or a range type. + + [range iter_ty c q begp ps endp] + ▲ ▲ ▲ ▲ ▲ ▲ + | | | | | └--- [ptr], end position of the range (not included); + | | | | | + | | | | └------- [list ptr], list of the address of every element of the range; + | | | | + | | | └----------- [ptr], begin position of the range (included); + | | | + | | └-------------- [cQp.t], fractional ownership; + | | + | └---------------- [C], contextual information shared by every range taken from + | the same collection; + | + └---------------------- [type], iterator type or range type of the object implementing a + range. + + [range] specifies pointers to a series of object without specifying the objects themselves. It + defines the order of the objects abstractly to allow any collection type to specify its own. It + is meant to be easy to split, recombine and move elements between consecutive ranges. Two ranges + are said to be consecutive iff the end position of one coincides with the beginning position of + the other. + *) + Open Scope Z_scope. + + Section UPSTREAM. + + Lemma lookup_rangeZ i j (k : nat) x : + rangeZ i j !! k = Some x <-> i ≤ x < j ∧ x = i + k. + Proof. + rewrite -lookupZ_rangeZ lookupZ_Some_to_nat Nat2Z.id. + intuition; lia. + Qed. + + #[global] Instance obs_Forall2_big_sepL2 {PROP A B} (R : A -> B -> Prop) (xs : list A) (ys : list B) P : + (forall k x y, Observe [| R x y |] (P k x y)) -> + Observe (PROP := PROP) [| Forall2 R xs ys |] (big_sepL2 P xs ys). + Proof. + move => HRxy. + elim/rev_ind: xs ys => [|x xs IH] ys; + rewrite (big_sepL2_nil_l_inv,big_sepL2_snoc_l_inv). + - iIntros "-> !> !%"; constructor. + - iIntros "(%y & %ys' & -> & P & Ps)". + iDestruct (HRxy with "P") as %?. + iDestruct (IH with "Ps") as %?. + iIntros "!> !%". + apply Forall2_app; repeat first [assumption | constructor]. + Qed. + + Lemma rangeZ_snoc_inv i j x xs : rangeZ i j = xs ++ [x] <-> i < j ∧ j - 1 = x ∧ rangeZ i (j-1) = xs. + Proof. + split. + - case: (Z.lt_ge_cases i j) => Hij. + + by rewrite rangeZ_snoc // => /app_inj_2 [//|-> [= <-]]. + + by rewrite rangeZ_oob // symmetry_iff app_nil => - []. + - move => - [Hij [] Hxi Hrng]. + by rewrite rangeZ_snoc // -Hxi Hrng. + Qed. + + End UPSTREAM. + + Section array. + Open Scope Z_scope. + Context `{Σ : cpp_logic, σ : genv}. + #[local] Notation IterState := Z (only parsing). + + (** + [array_spine ty basep q pi xs pj] + + [array_spine] provides a notion of [range] (from [HasRanges]) for any array based + collection. It allows a conversion between an array-specific definition of a collection to one + compatible with the notion of iterator specified by [HasRanges]. + + In particular, we ensure that the following equivalence holds (lemma + [arrayLR_eqv_array_spine_big_sepL2]): + << + basep |-> arrayLR ty i j R vs + -|- + ∃ ps, + array_spine ty basep 1$m (basep .[ ty ! i]) ps (basep .[ ty ! j]) ** + [∗ list] p; v ∈ ps; vs, p |-> R v + >> + + so that we can use [basep .[ ty ! i]] and [basep .[ ty ! j]] can be used as the state of an iterator + in code parameterized by the kind of collection or iterators. + + Limitations: + 1. proving agreement: can't deduce [i = j] from [basep .[ ty ! i] = basep .[ ty ! j]] (lemma is admitted) + 2. CFracValid: [array_spine] has no underlying PCM. + 3. When [array_spine] is given to a function which takes a [range ... begp ps endp] + precondition and which returns an iterator at index [i] in that range, the state of that + iterator can be specified abstractly as: + << + ∃ elemp, [| ps !! i = Some elemp |] ** itp |-> objR iter_ty elemp + >> + Once returned to the caller and interpretted in that context, the pure term boils down to: + << + [| (fun i => basep .[ ty ! i ] ) <$> rangeZ m n !! i = Some elemp |] + >> + Ideally, we should want the automation to see that this entails + [∃ k, m ≤ k < n ∧ elemp = basep .[ ty ! k ] ] and let us continue our proof from + there. However, if [ps] is not a fresh variable, substituting it for the [_ <$> rangeZ _ _] + formulation may not be straightforward. + 4. By using [ptr] as the type for positions, [array_spine] and [HasRanges] cannot specify + iterations over `vector`. + + Idea 1: + include the ownership of the base pointer. It solves 2. + Issue 1: this does not allow `std::vector` to preserve the validity of iterators after move. + Issue 2: breaks lemma [arrayLR_eqv_array_spine_big_sepL2]. + + Idea 2: + To solve 3, [HasRanges] could be reformulated as follows: + << + position : Set ; + dereference : position -> ptr ; + range : cQp.t -> position -> list position -> position -> mpred + (* everything else more or less the same *) + >> + and we can instantiate it for [array_spine] as: + << + position := ptr * Z ; + dereference '(basep, i) := basep .[ ty ! i ] ; + (* everything else adjusted accordingly *) + >> + with this definition, [ps] has all the information we need to find the array subscript + designated by the resulting iterator. + + Reference from the cppreference page on `std::vector`: + - after move constructor / assignment, the iterators of `other` remain valid but now reference + elements of `*this` + *) + Definition array_spine (ty : type) (basep : ptr) (q : cQp.t) (i : IterState) (xs : list IterState) (j : IterState) : mpred := + [| (i ≤ j)%Z |] ∗ + [| is_Some (size_of σ ty) |] ** + [| rangeZ i j = xs |] ** + valid_ptr (basep .[ ty ! j ]) ** + [∗ list] idx ∈ xs, type_ptr ty (basep .[ ty ! idx ]). + #[global] Arguments array_spine _ _ _ _ !xs _ / : assert. + #[global] Arguments array_spine : simpl never. + #[global] Hint Opaque array_spine : sl_opacity. + + Section local_stuff. + Context {ty : type}. + Context {basep : ptr}. + + #[local] Notation deref s := ( (basep : ptr) .[ ty ! s ] ). + #[local] Notation array_spine := (array_spine ty basep). + + #[global] Instance array_spine_CFractional3 : CFractional3 array_spine. + Proof. + rewrite /CFractional/array_spine => *. + by rewrite -bi.persistent_sep_dup. + Qed. + + + + #[global] Instance array_spine_obs_valid_r q s0 ps s1 : + Observe (valid_ptr (deref s1)) (array_spine q s0 ps s1). + Proof. + rewrite /array_spine. + by iIntros "(%Hij & ? & ? & #A & B) !>". + Qed. + + #[global] Instance array_spine_obs_valid_l q s0 ps s1 : + Observe (valid_ptr (deref s0)) (array_spine q s0 ps s1). + Proof. + rewrite /array_spine. + case: ps. + - + iIntros "(%Hij & ? & %Hnil & #A & B)". + move: Hnil => /rangeZ_nil_inv Hji; iIntros "!>". + by have -> : s0 = s1 by lia. + - iIntros (p ps) "(%Hij & ? & %Heq & A & #B) !>". + move: Heq => /rangeZ_cons_inv [? [<- ?]] /=. + iDestruct "B" as "[B _]". + iApply (type_ptr_valid with "B"). + Qed. + + #[global] Instance array_spine_obs_has_size q s0 ps s1 : + Observe [| is_Some (size_of σ ty) |] (array_spine q s0 ps s1). + Proof. rewrite /array_spine; apply _. Qed. + + Lemma array_spine_unfold q ps i j : + array_spine q i ps j + -|- + [| (i ≤ j)%Z |] ∗ + [| is_Some (size_of σ ty) |] ** + valid_ptr (basep .[ ty ! j ]) ** + [∗ list] idx; p ∈ rangeZ i j ; ps, [| p = idx |] ∗ type_ptr ty (basep .[ ty ! p ]). + Proof. + rewrite /array_spine. + apply observe_both with (p := is_Some (size_of σ ty)); [> apply _ .. | move => ?]. + apply observe_both with (p := rangeZ i j = ps); [apply _ | | move => Hrng]. + { rewrite big_sepL2_sep. + iIntros "(%Hij & _ & _ & A & _)". + rewrite list_eq_Forall2. + iApply (observe with "A"). + auto using observe_only_provable_impl, obs_Forall2_big_sepL2. } + f_equiv; rewrite !only_provable_True // !left_id; f_equiv. + rewrite big_sepL2_rangeZ_l -Hrng; apply big_sepL_proper => k y. + rewrite lookup_rangeZ => - [_ ->]. + by rewrite only_provable_True // left_id. + Qed. + + #[global] Instance array_spine_obs_valid q i j k ps (Hbounds : SolveArith (i ≤ j ≤ k)) : + Observe (valid_ptr (basep .[ ty ! j ])) (array_spine q i ps k). + Proof. + case: Hbounds => [] [Hij Hjk]. + have /Zle_lt_or_eq [Hlt|->] : j ≤ k by lia. + - rewrite array_spine_unfold. + do 3 apply observe_sep_r. + have -> : rangeZ i k = rangeZ i j ++ j :: rangeZ (j + 1) k. + { rewrite -rangeZ_cons // rangeZ_app //. } + iIntros "A". + iDestruct (big_sepL2_app_l_inv with "A") as (?? ->) "[_ B]". + iDestruct (big_sepL2_cons_l_inv with "B") as (?? ->) "[[-> B] _]". + iApply (observe with "B"). + - apply array_spine_obs_valid_r. + Qed. + + (* NOTE: it might be simpler to have this equality verbatim in [array_spine] *) + Lemma array_spine_obs_fmap_rangeZ q ps i j : + Observe [| ps = rangeZ i j |] + (array_spine q i ps j). + Proof. + rewrite array_spine_unfold. + rewrite /Observe persistently_only_provable big_sepL2_sep_sepL_r. + iIntros "(%Hij & _ & _ & A & _)"; iStopProof. + elim: ps i Hij => [| p ps IH] i Hij; iIntros "A". + - iDestruct (big_sepL2_nil_r_inv with "A") as %Hji%rangeZ_nil_inv. + have {Hji Hij} <- : i = j by lia. + by rewrite rangeZ_nil. + - iDestruct (big_sepL2_cons_r_inv with "A") as "(%i' & %is' & %Hrng & -> & A)". + move: Hrng => /rangeZ_cons_inv [{} Hij] [<- {i'}] <- {is'}. + iDestruct (IH with "A") as "->"; [lia | iPureIntro => {IH}]. + by rewrite [rangeZ i j]rangeZ_cons. + Qed. + + Lemma array_spine_obs_len q ps i j : + Observe [| lengthZ ps = j - i |] (array_spine q i ps j). + Proof. + rewrite array_spine_unfold. + iIntros "(%Hij & _ & _ & B)". + iDestruct (big_sepL2_lengthZ with "B") as %Hlen. + move: Hlen; rewrite lengthN_rangeZ => <-. + iIntros "!> !%"; lia. + Qed. + + #[global] Instance array_spine_obs_nil q s0 s1 : + Observe [| s0 = s1 |] (array_spine q s0 [] s1). + Proof. + iIntros "A". + iDestruct (array_spine_obs_len with "A") as %Hlen. + have {Hlen} <- : s0 = s1 by move: Hlen; rewrite lengthN_nil; lia. + by iIntros "!> !%". + Qed. + + #[global] Instance array_spine_obs_is_nil q ps s : + Observe [| ps = [] |] (array_spine q s ps s). + Proof. + iIntros "A". + iDestruct (array_spine_obs_len with "A") as %Hlen. + iIntros "!> !%". + apply base.lengthN_nil_inv, (inj Z.of_N). + by move: Hlen ; rewrite Z.sub_diag. + Qed. + + #[global] Instance array_spine_obs_cons q s0 s ss s1 : + Observe [| s0 = s |] (array_spine q s0 (s :: ss) s1). + Proof. + rewrite /array_spine => *. + iIntros "(%Hij & #? & %Hrng & A & B) !> !%". + by move: Hrng => /rangeZ_cons_inv [?] [<- ?]. + Qed. + + #[global] Instance array_spine_obs_snoc q s0 s ss s1 : + Observe [| s = s1 - 1 |] (array_spine q s0 (ss ++ [s]) s1). + Proof. + rewrite /array_spine => *. + iIntros "(%Hij & #? & %Hrng & A & B) !> !%". + by move: Hrng => /rangeZ_snoc_inv [?] [<- ?]. + Qed. + + #[global] Instance array_spine_obs_agree_l st_end xs : + AgreeCF1 (fun q s => array_spine q s xs st_end). + Proof. + iIntros (q1 q2 i i') "A B"; rename st_end into j. + iDestruct (array_spine_obs_len with "A") as %Hlen0. + iDestruct (array_spine_obs_len with "B") as %Hlen1. + have <- : i = i' by lia. + by iIntros "!> !%". + Qed. + + #[global] Instance array_spine_obs_agree_r st_start xs : + AgreeCF1 (fun q s => array_spine q st_start xs s). + Proof. + iIntros (q1 q2 j j') "A B"; rename st_start into i. + iDestruct (array_spine_obs_len with "A") as %Hlen0. + iDestruct (array_spine_obs_len with "B") as %Hlen1. + have <- : j = j' by lia. + by iIntros "!> !%". + Qed. + + Lemma array_spine_app (q : cQp.t) (s0 s2 : IterState) (xs0 xs1 : list IterState) : + array_spine q s0 (xs0 ++ xs1) s2 ⊣⊢ ∃ s1 : IterState, array_spine q s0 xs0 s1 ∗ array_spine q s1 xs1 s2. + Proof. + rename s0 into i, s2 into k. + split'. + - iIntros "A". + iDestruct (array_spine_obs_len with "A") as %Hlen. + move: Hlen; rewrite lengthN_app N2Z.inj_add => Hlen. + iDestruct (observe_elim (valid_ptr (basep .[ ty ! i + lengthZ xs0 ])) with "A") as "[A #?]". + rewrite array_spine_unfold big_sepL2_app_r_inv. + iDestruct "A" as (?) "(#Hsize & #Hvalid & %ys0 & %ys1 & %Hys & A & B)". + iDestruct (big_sepL2_lengthZ with "A") as %Hlen0. + move: Hys Hlen0 => /rangeZ_app_inv [[]|]; first by lia. + move => [j] [Hij] [<-] [Hjk <-]. + rewrite lengthN_rangeZ => Hlen0. + have -> : i + lengthZ xs0 = j by rewrite -Hlen0; lia. + iExists j. + by rewrite !array_spine_unfold; iFrame "# ∗". + - iIntros "(%j & A & B)". + rewrite !array_spine_unfold big_sepL2_app_r_inv. + iDestruct "A" as (?) "(Hj & #? & $)". + iDestruct "B" as (?) "($ & $ & $)". + iPureIntro; rewrite rangeZ_app //; split; [lia|done]. + Qed. + + Lemma array_spine_rangeZ_split {q i} j {k} (Hij : i ≤ j) (Hjk : j ≤ k) : + array_spine q i (rangeZ i k) k + -|- + array_spine q i (rangeZ i j) j ∗ + array_spine q j (rangeZ j k) k. + Proof. + have <- : rangeZ i j ++ rangeZ j k = rangeZ i k + by rewrite !rangeZ_app //; lia. + rewrite array_spine_app. + split'; last iIntros "$". + iIntros "(%s & A & B)". + move: (Zle_lt_or_eq _ _ Hij) (Zle_lt_or_eq _ _ Hjk) => {Hij Hjk} + => - [Hij _|<- [Hjk|<-]]. + - iDestruct (observe_elim [| j - 1 = s - 1 |] with "A") as "[A %Hjs]"; + first by rewrite rangeZ_snoc //; apply _. + move: Hjs => /Z.sub_cancel_r <-; iFrame. + - iDestruct (observe_elim [| s = i |] with "B") as "[B ->]"; + first by rewrite rangeZ_cons //; apply _. + iFrame. + - rewrite rangeZ_nil. + iDestruct (observe_elim [| i = s |] with "A") as "[A <-]". + iFrame. + Qed. + + Lemma arrayLR_eqv_array_spine_big_sepL2_rangeZ {A} q i j (R : A -> Rep) (vs : list A) : + basep |-> arrayLR ty i j R vs + -|- + array_spine q i (rangeZ i j) j ** + [∗ list] p; v ∈ rangeZ i j; vs, deref p |-> R v. + Proof. + rewrite arrayLR.unlock arrayR_eq/arrayR_def arrR_eq/arrR_def. + rewrite !(_at_sep,_at_only_provable,_at_offsetR,_at_big_sepL,_at_validR). + split'. + - iIntros "A". + rewrite array_spine_unfold. + iDestruct "A" as "(% & #? & #Hsize & SEP)". + have ? : i ≤ j by lia. + have Hi_len : i + length (R <$> vs) = j + by rewrite length_fmap -lengthZ_correct; lia. + rewrite o_sub_sub Hi_len. + iFrame "#". + rewrite [ [| i ≤ j |] ] only_provable_True // left_id. + rewrite 2!big_sepL2_rangeZ_l 1!big_opL_fmap. + rewrite (big_opL_rangeZ vs) //. + rewrite -big_opL_op. + iApply (big_sepL_mono with "SEP") => k x Hx. + rewrite only_provable_True // left_id. + by rewrite _at_offsetR _at_sep _at_type_ptrR o_sub_sub. + - iIntros "[A B]". + iDestruct (array_spine_obs_len with "A") as %Hlen. + iDestruct (array_spine_obs_has_size with "A") as %Hsize'. + iDestruct (array_spine_obs_valid_r with "A") as "#valid". + iDestruct (big_sepL2_lengthZ with "B") as %?. + have ? : lengthZ vs = j - i by etrans. + rewrite array_spine_unfold. + iDestruct "A" as "(%Hij & %Hsize & _ & SEP)". + rewrite !only_provable_True // !left_id. + rewrite length_fmap -lengthZ_correct o_sub_sub. + have -> : i + lengthZ vs = j by lia. + iFrame "valid". + rewrite !big_sepL2_rangeZ_l !big_opL_fmap. + rewrite (big_opL_rangeZ vs) //. + iCombine "SEP B" as "A". + rewrite -big_opL_op. + iApply (big_sepL_mono with "A") => k x Hx. + rewrite only_provable_True // left_id. + by rewrite _at_offsetR _at_sep _at_type_ptrR o_sub_sub. + Qed. + + Lemma arrayLR_eqv_array_spine_big_sepL2 {A} q i j (R : A -> Rep) (vs : list A) : + basep |-> arrayLR ty i j R vs + -|- + ∃ ps, + array_spine q i ps j ** + [∗ list] p; v ∈ ps; vs, deref p |-> R v. + Proof. + rewrite (arrayLR_eqv_array_spine_big_sepL2_rangeZ q). + split'; first by iIntros "$". + iIntros "(%ps & A & B)". + iDestruct (array_spine_obs_fmap_rangeZ with "A") as %->. + iFrame. + Qed. + + Lemma array_spine_frac {q} q' begp ps endp : + array_spine q begp ps endp -|- array_spine q' begp ps endp. + Proof. by rewrite /array_spine. Qed. + + (* NOTE: This hint loses all [type_ptr] of the [ptr]s in [ps] but they are typically available + through the array *) + Lemma array_spine_collect q begp ps endp : + array_spine q begp ps endp |-- valid_ptr (deref endp). + Proof. + iIntros "A". + iDestruct (array_spine_obs_valid_r with "A") as "#$". + Qed. + + #[global] Instance learn_array_spine_rangeZ q i ps j : + Learnable + emp + (array_spine q i ps j) + [ ps = rangeZ i j ]. + Proof. solve_learnable. Qed. + + Definition array_spine_collect_F := [FWD] array_spine_collect. + + Definition congr_array_spine q := normalize.NormCongr4 (fun basep => array_spine basep q). + + End local_stuff. + + #[program] + Definition array_ranges ty it_ty : + HasRanges it_ty ptr Z := + {| dereference := fun (basep : ptr) st => basep .[ ty ! st ] ; + range := array_spine ty ; + range_app basep := array_spine_app ; + |}. + + Lemma arrayLR_eqv_spine_payload_rangeZ ty it_ty q (H := array_ranges ty it_ty) + {A} (basep : ptr) i j (R : A -> Rep) (vs : list A) : + basep |-> arrayLR ty i j R vs + -|- + array_spine ty basep q i (rangeZ i j) j ** + payload it_ty basep R (rangeZ i j) vs. + Proof. by rewrite arrayLR_eqv_array_spine_big_sepL2_rangeZ payload.unlock. Qed. + End array. + + #[global] Hint Resolve array_spine_collect_F : sl_opacity. + #[global] Hint Resolve congr_array_spine : normalize_db. + + Section lookup_result. + + (* gadget meant to facilitate the manipulation of iterators returned from functions. *) + Definition lookup_result {PROP : bi} {A} (x : option A) (r : A) : PROP := + [| x = Some r |]. + + #[global] Hint Opaque lookup_result : sl_opacity typeclass_instances. + #[global] Arguments lookup_result : simpl nomatch. + + Lemma lookup_result_fmap {PROP A B} (f : A -> B) (i : Z) (xs : list A) y : + lookup_result (PROP := PROP) ((f <$> xs) !! i) y + |-- + ∃ x (_ : y = f x), + lookup_result (PROP := PROP) (xs !! i) x. + Proof. + rewrite /lookup_result list_lookupZ_fmap. + iPureIntro => /fmap_Some [x] [-> ->]. + by exists _, eq_refl. + Qed. + + Definition lookup_result_fmap_F := [FWD] @lookup_result_fmap. + + Lemma lookup_result_rangeZ {PROP} (m n i : Z) x `{Hnorm : !normalize.Normalize eq (i + m)%Z x'} : + lookup_result (PROP := PROP) (rangeZ m n !! i) x + |-- + ∃ (_ : x = x'), emp. + Proof. + rewrite /lookup_result -{}Hnorm. + iPureIntro => /lookupZ_rangeZ [? ->]. + by rewrite Z.add_comm; exists eq_refl. + Qed. + + Definition lookup_result_rangeZ_F := [FWD] @lookup_result_rangeZ. + + End lookup_result. + + #[global] Hint Resolve lookup_result_rangeZ_F : sl_opacity. + #[global] Hint Resolve lookup_result_fmap_F : sl_opacity. + +NES.End std. + +(** TODO: update comment to reflect changes to this *) +Module Type CODE_SNIPPETS (U : common.UNIT). +Section code_snippets. + Context `{Σ : cpp_logic,σ : genv}. + #[local] Notation WpSpec := (WpSpec mpred val val). + NES.Open std. + + Definition reverse_spec {A} (ty iter_ty : type) + `{!BundledRep ty A, (* [objR] for the objects contained by the range *) + !BundledRep iter_ty It, (* [objR] for the iterators *) + !HasRanges iter_ty C It} : WpSpec := (* [range] where the endpoints are iterators of type [iter_ty] *) + \arg{it_begp} "begin" (Vptr it_begp) + \arg{it_endp} "end" (Vptr it_endp) + (* Ownership of `begin` / `end` iterator objects. *) + \prepost{begp} it_begp |-> objR iter_ty 1$m begp + \prepost{endp} it_endp |-> objR iter_ty 1$m endp + (* Below, [c] is a collection ID, which is shared between a collection and all ranges taken + from it. [ps] is a list of pointers to the objects contained between `[begin,end[`; if + [ps] is non-empty, the first element is [begp] while [endp] is always excluded. + IMPORTANT NOTE: [range] does not own any of the elements of the underlying collection. A + separate term is provided for that purpose. *) + \prepost{c qr ps} range iter_ty c qr begp ps endp + \pre{vs} payload iter_ty c (objR ty 1$m) ps vs (* ownership of the elements *) + \post payload iter_ty c (objR ty 1$m) ps (reverse vs). + (* The values of the objects in the range are returned in reversed order. The list of + pointers itself is unchanged which guarantees that the reversal is performed in-place. *) + + Context {ty iter_ty : type}. + Context `{!HasRanges iter_ty C Iter}. + Context `{!BundledRep iter_ty (C * Iter)}. + Context {it_begp it_endp : ptr}. + Context {begp endp : Iter}. + Context {itp : ptr} {elemp : Iter}. + Context {ps0 ps1 : list Iter}. + Context {qr q : cQp.t}. + Context (c : collection_idT iter_ty). + Context {A} `{!BundledRep ty A} (vs : list A). + + Definition example2 : list mpred := + [ it_begp |-> objR iter_ty 1$m (c, begp) + ; it_endp |-> objR iter_ty 1$m (c, endp) + ; itp |-> objR iter_ty 1$m (c, elemp) + ; range iter_ty c qr begp ps0 elemp + ; range iter_ty c qr elemp (elemp :: ps1) endp + ; [∗ list] p; v ∈ elemp :: ps1; vs, dereference iter_ty c p |-> objR ty q v ]%I. + + Context {nextp : Iter}. + + Definition example3 : list mpred := + [ it_begp |-> objR iter_ty 1$m (c, begp) + ; it_endp |-> objR iter_ty 1$m (c, endp) + ; itp |-> objR iter_ty 1$m (c, nextp) + ; range iter_ty c qr begp (ps0 ++ [elemp]) nextp + ; range iter_ty c qr nextp ps1 endp + ; [∗ list] p; v ∈ elemp :: ps1; vs, dereference iter_ty c p |-> objR ty q v ]%I. + + Context {basep : ptr} (i j : Z) (R : A -> Rep). + + Definition example4 := + basep |-> arrayLR ty i j R vs + -|- + ∃ ps, + array_spine ty basep 1$m i ps j ** + [∗ list] idx; v ∈ ps; vs, basep .[ ty ! idx ] |-> R v. +End code_snippets. +End CODE_SNIPPETS. diff --git a/rocq-brick-libstdcpp/proof/vector/inc_vector.cpp b/rocq-brick-libstdcpp/proof/vector/inc_vector.cpp new file mode 100644 index 0000000..c8339cc --- /dev/null +++ b/rocq-brick-libstdcpp/proof/vector/inc_vector.cpp @@ -0,0 +1,7 @@ +/** + * Copyright (C) 2025 BlueRock Security, Inc. + * All rights reserved. + * + * SPDX-License-Identifier: LGPL-2.1 WITH BlueRock Exception for use over network, see repository root for details. + */ +#include diff --git a/rocq-brick-libstdcpp/proof/vector/pred.v b/rocq-brick-libstdcpp/proof/vector/pred.v new file mode 100644 index 0000000..696d782 --- /dev/null +++ b/rocq-brick-libstdcpp/proof/vector/pred.v @@ -0,0 +1,7 @@ +(** + * Copyright (C) 2025 SkyLabs AI, Inc. + * All rights reserved. + * + * SPDX-License-Identifier: LGPL-2.1 WITH BlueRock Exception for use over network, see repository root for details. + *) +Require Export skylabs.brick.libstdcpp.vector.spec. diff --git a/rocq-brick-libstdcpp/proof/vector/spec.v b/rocq-brick-libstdcpp/proof/vector/spec.v new file mode 100644 index 0000000..8dcc73d --- /dev/null +++ b/rocq-brick-libstdcpp/proof/vector/spec.v @@ -0,0 +1,860 @@ +(** + * Copyright (C) 2025 SkyLabs AI, Inc. + * All rights reserved. + * + * SPDX-License-Identifier: LGPL-2.1 WITH BlueRock Exception for use over network, see 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.vector.inc_vector_cpp. + +Require Export skylabs.brick.libstdcpp.allocator.spec. +Require Export skylabs.brick.libstdcpp.iterator.spec. + +NES.Begin std. + #[local] Open Scope Z_scope. + + Module Type VECTOR_PREDS. + #[global] Notation N ty alloc_ty := (Ninst "std::__1::vector" [Atype ty;Atype alloc_ty]) (only parsing). + #[global] Notation T ty alloc_ty := (Tnamed (N ty alloc_ty)) (only parsing). + + (** + * NOTE(Simon): + * This state type does not make reference to the state of the allocator or the [max_size] it can + * accommodate. + * + * TODO: support [max_size] and the allocator state (vector::get_allocator gives direct access to + * it). + *) + Record InternalState := + { capacity : Z ; + base_pointer : ptr }. + + (** + * Module [std.vector] + * provides a [Rep] predicate for vectors of [ty] using type [alloc_ty] as the allocator. The + * C++ standard library provides < >> as a default choice of allocator and we + * can base a specification on that default using the notations: [std.vector.R], + * [std.vector.R_cap], and [std.vector.R_resized]. [std.vector] provides the [Rep] predicate + * [spineR ty alloc_ty q size st] which specifies the ownership of only the shape of the + * vector, not the payload itself. [size] is the number of elements of the vector whereas + * [st : InternalState] is a record that keeps track of the capacity of the vector and a + * pointer to the memory holding the payloads. + * + * A vector together with its payload can be specified as: + * << + * p |-> std.vector.spineR ty alloc_ty q size st ** + * base_pointer st |-> arrayLR ty 0 size Rpayload xs + * >> + * + * [p |-> std.vector.R ty q xs]. + * We can also use the shorthand [p |-> std.vector.R ty q xs] that allows us to omit the type of + * the allocator, the internal state of the vector, its size and the Rep predicate for each + * payload -- using the [RepFor] type class and its projection [objR] as a default for the + * latter. + * + * The specifications of <> rarely use [std.vector.R] in particular to make it easy to + * prove that memory addresses of the payloads remain constant in certain circumstances. + * + * Various notations other than [std.vector.R] are provided so that the ownership of a vector can + * be expressed at various levels of abstractions. Because all those shorthands are defined as + * notations, whatever the level of abstraction chosen will result in the use of + * [std.vector.spineR] for the shape of the vector and [arrayLR] for the payload. Any automation + * that manipulates either will be usable with any use of vectors. + * + * # Rationale + * The value of leaning heavily on [spineR] and [arrayLR] the specify the shape of vectors is + * threefold: + * + * 1. We can use basic array automation to reason about random access to elements of a vector as + * well as convenient features such as specifying slices and varying the representation of + * vector elements over time. + * + * 2. We can write specifications for the <> functions with very tight footprints. As + * an example, let us consider a loop, say [for (i = 0; i < v.size(); ++i)], where we iterate + * over the elements of a vector to change their representation from [p .[ ty ! i] |-> RA q x] + * to [p .[ ty ! i] |-> RB q x]. We can specify the loop invariant as + * << + * basep |-> arrayLR ty 0 i (RA 1$m) xs0 ** + * basep |-> arrayLR ty i size (RB 1$m) xs1 + * >> + * whenever we call [v.size()], only [spineR] is required and there is no need to repackage + * the [arrayLR] terms into a more homogeneous shape, such as [arrayLR ty 0 size objR (xs0 ++ xs1)], + * which would be needed by a wider footprint characterization of <>. + * + * 2. The standard makes strong guarantees about the validity of references and iterators within + * a vector and about when storage gets realocated. By focusing our definitions around + * [spineR] and [arrayLR], we can write strong specifications for the <> functions + * and use the same strong specifications whether the specifications of the client code + * references the internal state of <> or uses more abstract terms to specify + * <> objects. + * + * To make the comparison more concrete, here are three formulations of the same vector (in + * different states) that can be mixed and matched without complications: + * + * A) The most abstract, no reference to the internal state: + * << + * vp |-> std.vector.R ty q (xs0 ++ xs1 ++ xs2) + * >> + * + * B) Bundled and low-level, concise and allows us to assert that inner references remain valid: + * << + * vp |-> std.vector.R_cap ty q size st (xs0 ++ xs1 ++ xs2) + * >> + * + * C) Low-level and detailed, allows us to use our favorite features of [arrayLR]: + * << + * vp |-> std.vector.spineR ty alloc_ty q size st ** (* NOTE: should this be called [R_spine] instead? Or + * [std.vector.internals.R_spine]? *) + * base_pointer st |-> arrayLR ty 0 i (RA q) xs0 ** + * [| xs1 = x :: xs1' |] ** + * base_pointer st .[ ty ! i ] |-> RB q x ** + * base_pointer st |-> arrayLR ty (i + 1) j (RC q) xs1' ** + * base_pointer st |-> arrayLR ty j size (RD q) xs2 + * >> + * + * When verifying a piece of code, assertions can alternate between B) and C) when we need + * references to remain valid and we can use A) at points of discontinuity where we no longer use + * the internal references of our vector. + * + * LIMITATION: this specification applies to the libc++ vectors and does not support + * < >>. To support < >>, we need a different + * construction from [arrayLR] so that we can track invidividual bits separately. + * + * LIMITATION: the specification does not discuss exceptions. If allocation fails in + * <> and callers (i.e. <>, + * <>, <>, etc), an exception is thrown. + * + * NOTE: When printing [spineR] in a goal, because it is a primitive projection, it will be + * printed as [spineR _ _ q x] instead of [spineR ty alloc_ty q x]. Turning on [Printing + * Primitive Projection Parameters] can make this nicer. + *) + Parameter spineR : + forall `{Σ : cpp_logic} {σ : genv} (ty alloc_ty : type) + (q : cQp.t) (size : Z) (intl : InternalState), Rep. + + sl.lock + Definition resizedR `{Σ : cpp_logic} (size : Z) (st st' : InternalState) : Rep := + if bool_decide (size ≤ capacity st) + then [| st' = st |] + else emp. + #[global] Arguments resizedR {_ _ Σ} size st st' : assert. + + (** Question(Simon): Should we take a predicate as a parameter instead of using [objR]? That would allow varying the + representation of the contents of the vector of the course of a single proof. That's also enabled by manipulating + [spineR] and [arrayLR] separately. *) + #[global] Notation R_alloc_cap ty alloc_ty q size st xs := + ( spineR ty alloc_ty q size st ** + pureR (base_pointer st |-> arrayLR ty 0 size (objR ty q) xs) )%I + (q in scope cQp_scope, basep in scope bi_scope, size, cap in scope Z_scope ). + + #[global] Notation R_alloc ty alloc_ty q xs := + (∃ size st, R_alloc_cap ty alloc_ty q size st xs )%I + (q in scope cQp_scope). + + #[global] Notation R_cap ty q size st xs := + (R_alloc_cap ty (std.allocator.T ty) q size st xs). + + #[global] Notation R ty q xs := + (R_alloc ty (std.allocator.T ty) q xs). + + (** [R_alloc_resized ty alloc_ty q size st xs] is a vector whose payloads can be proven (on + demand) to be stored in memory specified by [st] if that memory can accommodate [size] elements. + Otherwise, the memory location of the payloads is unspecified. + + Reference: + - https://en.cppreference.com/w/cpp/container/vector, section Iterator invalidation + *) + #[global] Notation R_alloc_resized ty alloc_ty q size st xs := + (∃ st', + resizedR size st st' ** + R_alloc_cap ty alloc_ty q size st' xs)%I + (size in scope Z_scope). + + (** See [R_alloc_resized] above *) + #[global] Notation R_resized ty q size st xs := + (R_alloc_resized ty (std.allocator.T ty) q size st xs). + + #[global] Notation null_state := ({| base_pointer := nullptr; capacity := 0 |}). + (** [R_null q] allows us to specify an empty vector without using a [Rep] predicate for [ty]. + + NOTE: Making [nullptr] the unique representation of an empty vector may prevent us from + proving that iterator [v.begin()] remains valid after we popped the last element of the + vector *) + #[global] Notation R_null ty alloc_ty q := (spineR ty alloc_ty q 0 null_state). + + Section spineR_props. + Context `{Σ : cpp_logic} {σ : genv}. + Context (ty alloc_ty : type). + #[local] Notation spineR := (spineR ty alloc_ty). + + #[global] Declare Instance spineR_cfrac : CFractional2 spineR. + #[global] Declare Instance spineR_ascfrac : AsCFractional2 spineR. + #[global] Declare Instance spineR_typed q st size : + Observe (type_ptrR (T ty alloc_ty)) (spineR q size st). + #[global] Declare Instance spineR_agree q size q' st size' st' : + Observe2 [| st = st' ∧ size = size' |] + (spineR q size st) + (spineR q' size' st'). + #[global] Declare Instance spineR_valid_size q size st : + Observe [| 0 ≤ size ≤ capacity st |] (spineR q size st). + #[global] Declare Instance nullptr_valid q size cap : + Observe [| cap = 0 |] (spineR q size {| base_pointer := nullptr ; capacity := cap |} ). + #[global] Declare Instance obs_splineR_array_spine q size st : + Observe (pureR (array_spine ty (base_pointer st) q 0 (rangeZ 0 size) size)) (spineR q size st). + End spineR_props. + + End VECTOR_PREDS. + + Module VECTOR_SPECS (Import vector : VECTOR_PREDS). + + Module iterator. + Import skylabs.brick.libstdcpp.iterator.spec. + + #[global] Notation NS := "std::__1"%cpp_name. + #[global] Notation N_base const ty := + (NS .:: Nid "__wrap_iter" .<< Atype (Tptr (Tconst_if const ty)) >> ). + #[global] Notation T_base const ty := (Tnamed (N_base const ty)). + sl.lock + Definition R_base `{Σ : cpp_logic, σ : genv} (const : bool) (ty : type) (q : cQp.t) (basep : ptr) (i : Z) : Rep := + _field (N_base const ty .:: Nid "__i_") |-> ptrR q (basep .[ ty ! i]) ** + structR (N_base const ty) q. + #[only(type_ptr,ascfractional)] derive R_base. + + #[global] Notation N ty := (N_base false ty). + #[global] Notation N_const ty := (N_base true ty). + #[global] Notation T ty := (T_base false ty). + #[global] Notation T_const ty := (T_base true ty). + #[global] Notation R ty := (R_base false ty). + #[global] Notation R_const ty := (R_base true ty). + + Section iter. + Context `{Σ : cpp_logic, σ : genv}. + + (* TODO: why do we need this instance locally instead of the one we make global? *) + #[local] Instance iterator_has_rep' is_const ty : concepts.BundledRep (T_base is_const ty) (ptr * Z) := + {| objR := fun q st => R_base is_const ty q st.1 st.2 |}. + + (* This has a type similar to [iterator_has_rep'] with some additional variables to + facilitate unification. *) + Definition iterator_has_rep is_const ty := + make_abstracted_name (T_base is_const ty, Hnf (iterator_has_rep' is_const ty)). + + Definition iter_default_ctor const ty := + concepts.default_ctor (T_base const ty) (nullptr, 0). + #[global] Hint Opaque iter_default_ctor : sl_opacity. + #[global] Arguments iter_default_ctor : simpl never. + Definition iter_default_ctor_SpecFor const := RegisterSpec (iter_default_ctor const). + #[global] Existing Instance iter_default_ctor_SpecFor. + + Definition iter_copy_ctor const ty := + concepts.copy_ctor (T_base const ty). + #[global] Hint Opaque iter_copy_ctor : sl_opacity. + #[global] Arguments iter_copy_ctor : simpl never. + Definition iter_copy_ctor_SpecFor const := + RegisterSpec (iter_copy_ctor const). + #[global] Existing Instance iter_copy_ctor_SpecFor. + + Definition iter_dtor const ty := concepts.dtor (T_base const ty). + #[global] Hint Opaque iter_dtor : sl_opacity. + #[global] Arguments iter_dtor : simpl never. + Definition iter_dtor_SpecFor := RegisterSpec (iter_dtor). + #[global] Existing Instance iter_dtor_SpecFor. + + Definition iter_move_assign const ty := + concepts.move_assign (T_base const ty) (fun p => p). + #[global] Hint Opaque iter_move_assign : sl_opacity. + #[global] Arguments iter_move_assign : simpl never. + Definition iter_move_assign_SpecFor := + RegisterSpec (iter_move_assign). + #[global] Existing Instance iter_move_assign_SpecFor. + + Definition iter_deref const ty := + let qf := function_qualifiers.mk true false Prvalue in + specify.template.op (N_base const ty) OOStar qf (Tref (Tconst_if const ty)) [] $ + \this this + \with basep i + \let itemp := basep .[ ty ! i ] + \prepost{q} this |-> R_base const ty q basep i + \post[Vref itemp] emp. + #[global] Hint Opaque iter_deref : sl_opacity. + #[global] Arguments iter_deref : simpl never. + Definition iter_deref_SpecFor := RegisterSpec iter_deref. + #[global] Existing Instance iter_deref_SpecFor. + + Definition iter_op_post_inc const ty := + let qf := function_qualifiers.mk false false Prvalue in + specify.template.op (N_base const ty) OOPlusPlus qf (T_base const ty) [Tint] $ + \this this + \arg{dummy} "_ignored_" (Vint dummy) + (* TODO: we need a precondition to state that we don't go out of bounds. + Maybe something like: + << + \prepost range (T_base const ty) basep (basep .[ ty ! i ]) [basep .[ ty ! i ]] (basep .[ ty ! i + 1 ]) + >> + this would have the following benefit: + - bounds can be checked even when a vector isn't around to specify the bounds + - available ranges, even if incomplete specify how far we can go with a given iterator + even when we don't dereference them + *) + \with basep i + \pre this |-> R_base const ty 1$m basep i + \post{prevp}[Vptr prevp] + prevp |-> R_base const ty 1$m basep i ** + this |-> R_base const ty 1$m basep (i + 1). + #[global] Hint Opaque iter_op_post_inc : sl_opacity. + #[global] Arguments iter_op_post_inc : simpl never. + Definition iter_op_post_inc_SpecFor := RegisterSpec iter_op_post_inc. + #[global] Existing Instance iter_op_post_inc_SpecFor. + + Definition iter_op_pre_inc const ty := + let qf := function_qualifiers.mk false false Prvalue in + specify.template.op (N_base const ty) OOPlusPlus qf (Tref (T_base const ty)) [] $ + \this this + \with basep i + (* TODO bound-checking, like above *) + \pre this |-> R_base const ty 1$m basep i + \post[Vptr this] this |-> R_base const ty 1$m basep (i + 1). + #[global] Hint Opaque iter_op_pre_inc : sl_opacity. + #[global] Arguments iter_op_pre_inc : simpl never. + Definition iter_op_pre_inc_SpecFor := RegisterSpec iter_op_pre_inc. + #[global] Existing Instance iter_op_pre_inc_SpecFor. + + Definition iter_op_eq const ty := + specify.template.static_op NS OOEqualEqual + [Atype (Tptr (Tconst_if const ty))] + Tbool [Tref (Tconst (T_base const ty)); Tref (Tconst (T_base const ty))] $ + \arg{firstp} "first" (Vptr firstp) + \arg{secondp} "second" (Vptr secondp) + \with basep i j + \prepost{q0} firstp |-> R_base const ty q0 basep i + \prepost{q1} secondp |-> R_base const ty q1 basep j + \post[Vbool (bool_decide (i = j))] emp. + #[global] Hint Opaque iter_op_eq : sl_opacity. + #[global] Arguments iter_op_eq : simpl never. + Definition iter_op_eq_SpecFor := RegisterSpec iter_op_eq. + #[global] Existing Instance iter_op_eq_SpecFor. + + Definition iter_op_ne const ty := + specify.template.static_op NS OOExclaimEqual + [Atype (Tptr (Tconst_if const ty))] + Tbool [Tref (Tconst (T_base const ty)); Tref (Tconst (T_base const ty))] $ + \arg{firstp} "first" (Vptr firstp) + \arg{secondp} "second" (Vptr secondp) + \with basep i j + \prepost{q0} firstp |-> R_base const ty q0 basep i + \prepost{q1} secondp |-> R_base const ty q1 basep j + \post[Vbool (bool_decide (i <> j))] emp. + #[global] Hint Opaque iter_op_ne : sl_opacity. + #[global] Arguments iter_op_ne : simpl never. + Definition iter_op_ne_SpecFor := RegisterSpec iter_op_ne. + #[global] Existing Instance iter_op_ne_SpecFor. + + Definition specs const ty := + iter_default_ctor const ty ** + iter_copy_ctor const ty ** + iter_dtor const ty ** + iter_move_assign const ty ** + iter_deref const ty ** + iter_op_post_inc const ty ** + iter_op_pre_inc const ty ** + iter_op_eq const ty ** + iter_op_ne const ty. + + End iter. + #[global] Existing Instance iterator_has_rep. + + Section hints. + Context `{Σ : cpp_logic, σ : genv}. + + #[global] Instance R_base_learn c ty : LearnEqF2 (R_base c ty) := ltac:(solve_learnable). + + Definition congr_iterator_R_base := normalize.NormCongr4 iterator.R_base. + End hints. + #[global] Hint Resolve congr_iterator_R_base : normalize_db. + + End iterator. + + #[global] Notation range_base const ty := (std.range (iterator.T_base const ty)). + #[global] Notation range ty := (std.range (iterator.T ty)). + #[global] Notation range_const ty := (std.range (iterator.T_const ty)). + + #[global] Notation payload_base const ty := (std.payload (iterator.T_base const ty)). + #[global] Notation payload ty := (std.payload (iterator.T ty)). + #[global] Notation payload_const ty := (std.payload (iterator.T_const ty)). + + Section with_cpp. + Context `{Σ : cpp_logic, σ : genv}. + Context (ty alloc_ty : type). + + NES.Open allocator_traits. + + #[local] Notation vector := (N ty alloc_ty) (only parsing). (** [vector] *) + #[local] Notation vectorT := (Tnamed vector) (only parsing). + + #[local] Notation R_null q := (spineR ty alloc_ty q 0 null_state). + #[local] Notation R q xs := (R_alloc ty alloc_ty q xs). + #[local] Notation R_cap q size st xs := (R_alloc_cap ty alloc_ty q size st xs). + + (** See [R_resized] and [R_alloc_resized] above *) + #[local] Notation R_resized q size s xs := (R_alloc_resized ty alloc_ty q size s xs). + + #[local] Notation spineR q size st := (spineR ty alloc_ty q size st). + #[local] Notation size_type := (allocator_traits.size_type alloc_ty). + + Definition default_ctor := + specify.template.ctor vector [] $ + \this this + \post this |-> R_null (cQp.m 1). + #[global] Hint Opaque default_ctor : sl_opacity. + #[global] Arguments default_ctor : simpl never. + Definition SpecFor_default_ctor := RegisterSpec default_ctor. + #[global] Existing Instance SpecFor_default_ctor. + + Definition ctor_with_alloc `{!BundledRep alloc_ty AllocT} := + specify.template.ctor vector [alloc_ty] $ + \this this + \arg{allocp} "alloc" (Vptr allocp) + \prepost{a} allocp |-> objR alloc_ty (cQp.m 1) a + \post this |-> R_null (cQp.m 1). + #[global] Hint Opaque ctor_with_alloc : sl_opacity. + #[global] Arguments ctor_with_alloc : simpl never. + Definition SpecFor_ctor_with_alloc := RegisterSpec default_ctor. + #[global] Existing Instance SpecFor_ctor_with_alloc. + + Section allocator. + Context `{!IsAllocator alloc_ty}. + Context `{!BundledRep ty V}. + + Section default_ctor. + Context `{!DefaultValue ty V}. + + Definition sized_ctor := + specify.template.ctor vector [size_type; alloc_ty] $ + \this this + \arg{size} "size" (Vint size) + \arg{allocp} "alloc" (Vptr allocp) + \prepost{a} allocp |-> objR alloc_ty (cQp.m 1) a + \post this |-> R (cQp.m 1) (replicateZ size (default_val ty)). + #[global] Hint Opaque sized_ctor : sl_opacity. + #[global] Arguments sized_ctor : simpl never. + Definition SpecFor_sized_ctor := RegisterSpec sized_ctor. + #[global] Existing Instance SpecFor_sized_ctor. + End default_ctor. + + Definition init_ctor := + specify.template.ctor vector [size_type; Tref (Tconst ty); alloc_ty] $ + \this this + \arg{size} "size" (Vint size) + \arg{vp} "v0" (Vref vp) + \arg{allocp} "alloc" (Vptr allocp) + \prepost{v0 vq} vp |-> objR ty vq v0 + \prepost{a} allocp |-> objR alloc_ty (cQp.m 1) a + \post this |-> R (cQp.m 1) (replicateZ size v0). + #[global] Hint Opaque init_ctor : sl_opacity. + #[global] Arguments init_ctor : simpl never. + Definition SpecFor_init_ctor := RegisterSpec init_ctor. + #[global] Existing Instance SpecFor_init_ctor. + + Definition copy_alloc_ctor := + specify.template.ctor vector [Tref (Tconst vectorT); Tref (Tconst alloc_ty)] $ + \this this + \arg{otherp} "other" (Vref otherp) + \arg{allocp} "alloc" (Vptr allocp) + \prepost{q__other size st xs} + otherp |-> R_cap q__other size st xs + \prepost{a} allocp |-> objR alloc_ty (cQp.m 1) a + \post this |-> R (cQp.m 1) xs. + #[global] Hint Opaque copy_alloc_ctor : sl_opacity. + #[global] Arguments copy_alloc_ctor : simpl never. + Definition SpecFor_copy_alloc_ctor := RegisterSpec copy_alloc_ctor. + #[global] Existing Instance SpecFor_copy_alloc_ctor. + + Definition move_alloc_ctor := + specify.template.ctor vector [Trv_ref vectorT; Tref (Tconst alloc_ty)] $ + \this this + \arg{otherp} "other" (Vref otherp) + \arg{allocp} "alloc" (Vptr allocp) + \pre{size st xs} + otherp |-> R_cap (cQp.m 1) size st xs + \post* otherp |-> R_null (cQp.m 1) + \prepost{a} allocp |-> objR alloc_ty (cQp.m 1) a + \post this |-> R_cap (cQp.m 1) size st xs. + #[global] Hint Opaque move_alloc_ctor : sl_opacity. + #[global] Arguments move_alloc_ctor : simpl never. + Definition SpecFor_move_alloc_ctor := RegisterSpec move_alloc_ctor. + #[global] Existing Instance SpecFor_move_alloc_ctor. + + End allocator. + + Section no_alloc. + Context `{!BundledRep ty V}. + + Definition copy_ctor := + specify.template.ctor vector [Tref (Tconst vectorT)] $ + \this this + \arg{otherp} "other" (Vref otherp) + \prepost{q__other size st xs} + otherp |-> R_cap q__other size st xs + \let cap := capacity st + \post + Exists new_basep, + let new_st := {| base_pointer := new_basep; capacity := cap |} in + this |-> R_cap (cQp.m 1) size new_st 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 move_ctor := + specify.template.ctor vector [Trv_ref vectorT] $ + \this this + \arg{otherp} "other" (Vref otherp) + \pre{size st xs} + otherp |-> R_cap (cQp.m 1) size st xs + \post* otherp |-> R_null (cQp.m 1) + \post this |-> R_cap (cQp.m 1) size st 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 dtor := + specify.template.dtor vector $ + \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. + + Definition subscript `{!IsAllocator alloc_ty} c := + let qf := function_qualifiers.mk c false Prvalue in + specify.template.op vector OOSubscript qf (Tref (Tconst_if c ty)) [size_type] $ + \this this + \arg{i} "i" (Vint i) + \prepost{q size st} this |-> spineR q size st + \require 0 ≤ i < size (** This is probably required in order to have `type_ptr` on the resulting reference *) + \post[Vref (base_pointer st .[ ty ! i])] emp . + #[global] Hint Opaque subscript : sl_opacity. + #[global] Arguments subscript : simpl never. + Definition SpecFor_subscript := RegisterSpec (@subscript). + #[global] Existing Instance SpecFor_subscript. + + Definition push_back_copy := + let qf := function_qualifiers.N in + specify.template.method vector "push_back" qf Tvoid [Tref (Tconst ty)] $ + \this this + \arg{p} "p" (Vref p) + \prepost{q x} p |-> objR ty q x + \pre{size st xs} + this |-> R_cap (cQp.m 1) size st xs + \post this |-> R_resized (cQp.m 1) (size + 1) st (xs ++ [x]). + #[global] Hint Opaque push_back_copy : sl_opacity. + #[global] Arguments push_back_copy : simpl never. + Definition SpecFor_push_back_copy := RegisterSpec push_back_copy. + #[global] Existing Instance SpecFor_push_back_copy. + + Definition push_back_move `{!concepts.MovedValue ty V} := + let qf := function_qualifiers.N in + specify.template.method vector "push_back" qf Tvoid [Trv_ref ty] $ + (* specify.template.ctor vector "push_back" qf [Trv_ref ty] $ *) + \this this + \arg{p} "p" (Vref p) + \pre{x} p |-> objR ty (cQp.m 1) x + \post* p |-> moved_objR ty (cQp.m 1) x + \pre{size st xs} + this |-> R_cap (cQp.m 1) size st xs + \post this |-> R_resized (cQp.m 1) (size+1) st (xs ++ [x]). + #[global] Hint Opaque push_back_move : sl_opacity. + #[global] Arguments push_back_move : simpl never. + Definition SpecFor_push_back_move := RegisterSpec (@push_back_move). + #[global] Existing Instance SpecFor_push_back_move. + + Definition pop_back := + let qf := function_qualifiers.N in + specify.template.method vector "pop_back" qf Tvoid [] $ + \this this + \with size st xs x + \pre this |-> R_cap (cQp.m 1) size st (xs ++ [x]) + \post this |-> R_resized (cQp.m 1) (size - 1) st xs. + #[global] Hint Opaque pop_back : sl_opacity. + #[global] Arguments pop_back : simpl never. + Definition SpecFor_pop_back := RegisterSpec pop_back. + #[global] Existing Instance SpecFor_pop_back. + + Definition back c := + let qf := function_qualifiers.mk c false Prvalue in + specify.template.method vector "back" qf (Tref (Tconst_if c ty)) [] $ + \this this + \with q size st + \require 0 < size + \prepost this |-> spineR q size st + \let backp := base_pointer st .[ ty ! size - 1 ] + \post[Vptr backp] emp. + #[global] Hint Opaque back : sl_opacity. + #[global] Arguments back : simpl never. + Definition SpecFor_back := RegisterSpec back. + #[global] Existing Instance SpecFor_back. + + Definition front c := + let qf := function_qualifiers.mk c false Prvalue in + specify.template.method vector "front" qf (Tref (Tconst_if c ty)) [] $ + \this this + \with q size st + \require 0 < size + \prepost this |-> spineR q size st + \let backp := base_pointer st .[ ty ! 0 ] + \post[Vptr backp] emp. + #[global] Hint Opaque front : sl_opacity. + #[global] Arguments front : simpl never. + Definition SpecFor_front := RegisterSpec front. + #[global] Existing Instance SpecFor_front. + + Definition clear := + let qf := function_qualifiers.N in + specify.template.method vector "clear" qf Tvoid [] $ + \this this + \with size st xs + \pre this |-> R_cap (cQp.m 1) size st xs + \post this |-> R_cap (cQp.m 1) 0 st []. + #[global] Hint Opaque clear : sl_opacity. + #[global] Arguments clear : simpl never. + Definition SpecFor_clear := RegisterSpec clear. + #[global] Existing Instance SpecFor_clear. + + Definition resize_default `{!concepts.DefaultValue ty V,!IsAllocator alloc_ty} := + let qf := function_qualifiers.N in + specify.template.method vector "resize" qf Tvoid [size_type] $ + \this this + \arg{new_size} "new_size" (Vint new_size) + \with size st xs + \pre this |-> R_cap (cQp.m 1) size st xs + \post + ∃ xs', + (if bool_decide (size = new_size) then + [| xs' = xs |] + else if bool_decide (new_size < size) then (* it would be better to have [new_size ≤ + size] for when neither [new_size = size] + nor [new_size ≠ size] *) + [| xs' = takeN (Z.to_N new_size) xs |] (* would [sliceZ] be better here (because of Z vs N)? *) + else (* size < new_size *) + [| xs' = xs ++ replicateZ (new_size - size) (default_val ty) |] ) ∗ + this |-> R_resized (cQp.m 1) new_size st xs'. + #[global] Hint Opaque resize_default : sl_opacity. + #[global] Arguments resize_default : simpl never. + Definition SpecFor_resize_default := RegisterSpec (@resize_default). + #[global] Existing Instance SpecFor_resize_default. + + Definition resize `{!IsAllocator alloc_ty} := + let qf := function_qualifiers.N in + specify.template.method vector "resize" qf Tvoid [size_type; Tref (Tconst ty)] $ + \this this + \arg{new_size} "new_size" (Vint new_size) + \arg{vp} "v0" (Vptr vp) + \prepost{q v0} vp |-> objR ty q v0 + \with size st xs + \pre this |-> R_cap (cQp.m 1) size st xs + \post + ∃ xs', + (if bool_decide (size = new_size) then + [| xs' = xs |] + else if bool_decide (new_size < size) then (* it would be better to have [new_size ≤ + size] for when neither [new_size = size] + nor [new_size ≠ size] *) + [| xs' = takeN (Z.to_N new_size) xs |] (* would [sliceZ] be better here (because of Z vs N)? *) + else (* size < new_size *) + [| xs' = xs ++ replicateZ (new_size - size) v0 |] ) ∗ + this |-> R_resized (cQp.m 1) new_size st xs'. + #[global] Hint Opaque resize : sl_opacity. + #[global] Arguments resize : simpl never. + Definition SpecFor_resize := RegisterSpec (@resize). + #[global] Existing Instance SpecFor_resize. + + Definition size `{!IsAllocator alloc_ty} := + let qf := function_qualifiers.Nc in + specify.template.method vector "size" qf size_type [] $ + \this this + \with q size st + \prepost this |-> spineR q size st + \post[Vint size] emp. + #[global] Hint Opaque size : sl_opacity. + #[global] Arguments size : simpl never. + Definition SpecFor_size := RegisterSpec (@size). + #[global] Existing Instance SpecFor_size. + + End no_alloc. + Section iterators. + + Definition begin_spec const := + let qf := function_qualifiers.mk const false Prvalue in + specify.template.method vector "begin" qf (iterator.T_base const ty) [] $ + \this this + \prepost{q size st} + this |-> spineR q size st + \post{itp}[Vptr itp] itp |-> iterator.R_base const ty 1$m (base_pointer st) 0. + #[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 const := + let qf := function_qualifiers.mk const false Prvalue in + specify.template.method vector "end" qf (iterator.T_base const ty) [] $ + \this this + \prepost{q size st} + this |-> spineR q size st + \post{itp}[Vptr itp] itp |-> iterator.R_base const ty 1$m (base_pointer st) size. + #[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. + + (** + [vector_has_ranges] should have type [HasRanges (iterator.T_base const ty)]. + Type class search then wouldn't find it so we use the notation [make_abstracted_name] + defined in [cpp/spec/specify.v] + + [vector_has_ranges] is defined as specialization of the generic array [HasRanges] + instance. + + TODO: this needs to be less abstruse. *) + Definition vector_has_ranges const := + make_abstracted_name (* this notation rewrites type [it_ty] to make it easier to match + modulo [const] *) + ( let it_ty := iterator.T_base const ty in + (it_ty, std.array_ranges ty it_ty)). + #[global] Existing Instance vector_has_ranges. + + End iterators. + + Section specs. + Context `{!IsAllocator alloc_ty}. + Context `{!BundledRep ty V}. + Context `{!DefaultValue ty V}. + Context `{!MovedValue ty V}. + + #[local] Notation MaybeConst spec := (spec true ** spec false). + + Definition specs := + default_ctor ** + ctor_with_alloc ** + sized_ctor ** + init_ctor ** + copy_alloc_ctor ** + move_alloc_ctor ** + copy_ctor ** + move_ctor ** + dtor ** + MaybeConst subscript ** + push_back_copy ** + push_back_move ** + pop_back ** + MaybeConst front ** + MaybeConst back ** + clear ** + resize_default ** + resize ** + size ** + MaybeConst begin_spec ** + MaybeConst end_spec. + + End specs. + + End with_cpp. + + Section instances_hints. + Context `{Σ : cpp_logic} {σ : genv} (ty alloc_ty : type). + + #[global] Instance nullptr_cap_size q size cap : + Observe ([| cap = 0 |] ** [| size = 0 |]) + (spineR ty alloc_ty q size {| base_pointer := nullptr ; capacity := cap |}). + Proof. + iIntros "H". + iDestruct (observe_elim_pure (0 ≤ size ≤ cap) with "H") as %Hsize. + { apply spineR_valid_size. } + iDestruct (nullptr_valid with "H") as %->. + move: Hsize => /= /ZMicromega.eq_le_iff <-. + by iIntros "!>". + Qed. + Definition nullptr_cap_size_F := ltac:(mk_obs_fwd nullptr_cap_size). + + #[global] Instance learn_spineR : + LearnEqF2 (spineR ty alloc_ty) := ltac:(solve_learnable). + + #[global] Instance learn_array_spine (p : ptr) q q' st ps size i j : + Learnable + (p |-> vector.spineR ty alloc_ty q size st) + (std.array_spine ty (vector.base_pointer st) q' i ps j + ) + [q = q' ]. + Proof. solve_learnable. Qed. + + #[global] Instance resizedR_affine size s s' : Affine (resizedR size s s'). + Proof. rewrite resizedR.unlock; apply _. Qed. + + Lemma trivial_resized_elim (p basep : ptr) size s' : + p |-> resizedR size {| base_pointer := basep ; capacity := 0 |} s' |-- emp. + Proof. rewrite resizedR.unlock; by iIntros. Qed. + Definition trivial_resized_elim_F := [FWD] trivial_resized_elim. + + #[program] + Definition vector_spine_intro_CB (p : ptr) q q' st size i j := + \cancelx + \preserving p |-> spineR ty alloc_ty q size st + \let basep := vector.base_pointer st + \proving std.array_spine ty basep q' i (rangeZ i j) j + \bound A (R : A -> Rep) + \proving{(vs : list A)} payload ty basep R (rangeZ i j) vs + \through basep |-> arrayLR ty i j R vs + \end. + Next Obligation. + intros. iIntros "$" (???) "A". + iDestruct (arrayLR_eqv_spine_payload_rangeZ with "A") as "[$ $]". + Qed. + + #[program] + Definition vector_spine_elim_CF (p : ptr) q st size i j (Harith : SolveArith (0 ≤ i ≤ j ≤ size)) := + \cancelx + \preserving p |-> spineR ty alloc_ty q size st + \let basep := vector.base_pointer st + \with A (R : A -> Rep) + \using{(vs : list A)} payload ty basep R (rangeZ i j) vs + \deduce basep |-> arrayLR ty i j R vs + \end. + Next Obligation. + intros; case: Harith => [[] Hi0 [] Hij Hj_size]. + iIntros "(A & B)". + iDestruct (observe_elim (array_spine _ _ _ _ _ _) with "A") as "[$ C]". + { apply observe_intuitionistically_if, _at_observe_pureR, _. } + have ? : 0 ≤ j by lia. + rewrite (array_spine_rangeZ_split j) // (array_spine_rangeZ_split i) //. + iDestruct "C" as "([_ C] & _)". + rewrite arrayLR_eqv_spine_payload_rangeZ. + iFrame "B C". + Qed. + + Definition congr_spineR q := normalize.NormCongr2 (vector.spineR ty alloc_ty q). + Definition congr_resizedR s s' := normalize.NormCongr1 (fun size => vector.resizedR size s s'). + + End instances_hints. + #[global] Hint Resolve nullptr_cap_size_F learn_spineR trivial_resized_elim_F : sl_opacity. + + #[global] Hint Resolve vector_spine_elim_CF : sl_opacity. + #[global] Hint Resolve vector_spine_intro_CB : sl_opacity. + + #[global] Hint Resolve congr_spineR : normalize_db. + #[global] Hint Resolve congr_resizedR : normalize_db. + + End VECTOR_SPECS. + + Module Type VECTOR := VECTOR_PREDS <+ VECTOR_SPECS. + + Declare Module vector : VECTOR. + +NES.End std. diff --git a/rocq-brick-libstdcpp/test/dune.inc b/rocq-brick-libstdcpp/test/dune.inc index b2bcdd3..f2704e1 100644 --- a/rocq-brick-libstdcpp/test/dune.inc +++ b/rocq-brick-libstdcpp/test/dune.inc @@ -170,3 +170,12 @@ (with-stderr-to demo_cpp.v.stderr (run cpp2v -v %{input} -o demo_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps demo.cpp)) ) +(subdir vector + (rule + (targets test_cpp.v.stderr test_cpp.v) + (alias test_ast) + (deps (:input test.cpp) (glob_files_rec ../*.hpp) (universe)) + (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)) +) diff --git a/rocq-brick-libstdcpp/test/vector/test.cpp b/rocq-brick-libstdcpp/test/vector/test.cpp new file mode 100644 index 0000000..edb34ef --- /dev/null +++ b/rocq-brick-libstdcpp/test/vector/test.cpp @@ -0,0 +1,101 @@ +/** + * Copyright (C) 2025 BlueRock Security, Inc. + * All rights reserved. + * + * SPDX-License-Identifier: LGPL-2.1 WITH BlueRock Exception for use over network, see repository root for details. + */ +#include +#include +#include + +using namespace std; + +void +test(bool b, const char* msg = nullptr) { + assert(b); +} + +void +TestBasic() { + vector v; + v.push_back(1); + v.push_back(2); + v.push_back(3); + test(v[0] == 1); + test(v[1] == 2); + test(v[2] == 3); + test(v.size() == 3); +} + +void +TestIntIter() { + vector v; + v.push_back(1); + v.push_back(2); + v.push_back(3); + auto it = std::find(v.begin(), v.end(), 2); + test(*it == 2); + it = v.begin(); + it++; + auto it2 = std::find(it, v.end(), 1); + auto it3 = v.end(); + test(it2 == it3); +} + +unsigned +sum(const vector& v) { + unsigned r = 0; + for (auto x : v) { + r += x; + } + return r; +} + +void +TestForEach() { + vector v{}; + v.push_back(1); + v.push_back(2); + v.push_back(3); + int r = sum(v); + test(r == 6); +} + +struct Aggregate { + int x, y, z; + Aggregate(const Aggregate &) = default; + Aggregate(Aggregate &&) = default; + Aggregate& operator = (const Aggregate &) = default; + Aggregate& operator = (Aggregate &&) = default; + + Aggregate(int a) : x(a), y(a), z(a) {} + bool operator==(Aggregate& other) { + return x == other.x && y == other.y && z == other.z; + } + bool operator!=(Aggregate& other) { + return !(*this == other); + } +}; + +void +TestAggregate() { + vector v; + Aggregate o1{1}, o2{2}, o3{3}; + test(o1 != o2); + v.push_back(o1); + v.push_back(o2); + v.push_back(o3); + test(v[0] == o1); + test(v[1] == o2); + test(v[2] == o3); + test(v.size() == 3); +} + +int +main() { + TestBasic(); + TestAggregate(); + TestIntIter(); + TestForEach(); + return 0; +} diff --git a/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v b/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v new file mode 100644 index 0000000..80d8a83 --- /dev/null +++ b/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v @@ -0,0 +1,346 @@ +(* + * Copyright (c) 2025 BlueRock Systems, 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.proof. +Require Import skylabs.brick.libstdcpp.allocator.spec. +Require Import skylabs.brick.libstdcpp.cassert.spec. +Require Import skylabs.brick.libstdcpp.vector.spec. +Require Import skylabs.brick.libstdcpp.algorithms.spec. +Require Import skylabs.brick.libstdcpp.test.vector.test_cpp. + +Require Import skylabs.auto.cpp.prelude.test. + +(* #[global] Hint Resolve arrayLR_split_head_bwd_C : sl_opacity. *) + +Import auto.lazy.big_sep.hints. +Import auto.cpp.lazy.big_sep.array. + +Module Aggregate. + Import concepts. + + cpp.class "Aggregate" prefix "" from module + dataclass { copyable ; movable ; destructible }. + #[only(eq_dec)] derive T. + + (* this could be generated *) + #[global] Instance BundledRep_Aggregate `{Σ : cpp_logic, σ : genv} : + BundledRep "Aggregate" T := {| objR := R |}. + + (* this could be generated *) + #[global] Instance DefaultValue_Aggregate `{Σ : cpp_logic, σ : genv} : + DefaultValue "Aggregate" T := + {| default_val := + {| x := default_val "int"; + y := default_val "int"; + z := default_val "int";|} |}. + + (* this could be generated *) + #[global] Instance MovedValue_Aggregate `{Σ : cpp_logic, σ : genv} : + MovedValue "Aggregate" T := + {| moved := + fun a a' => + moved "int" (x a) (x a') ∧ + moved "int" (y a) (y a') ∧ + moved "int" (z a) (z a') |}. + + Section with_cpp. + Context `{Σ : cpp_logic, σ : genv}. + Section specs. + Context `{MOD : test_cpp.module ⊧ σ}. + + cpp.spec "Aggregate::Aggregate(int)" as ctor_spec with + (\this this + \arg{a} "a" (Vint a) + \let r := {| Aggregate.x := a; Aggregate.y := a ; Aggregate.z := a |} + \post this |-> Aggregate.R 1$m r ). + + cpp.spec "Aggregate::operator==(Aggregate&)" as op_eq_spec with + (\this this + \arg{otherp} "otherp" (Vptr otherp) + \prepost{qa a} this |-> R qa a + \prepost{qb b} otherp |-> R qb b + \post[Vbool (bool_decide (a = b))] emp ). + + cpp.spec "Aggregate::operator!=(Aggregate&)" as op_neq_spec with + (\this this + \arg{otherp} "otherp" (Vptr otherp) + \prepost{qa a} this |-> R qa a + \prepost{qb b} otherp |-> R qb b + \post[Vbool (bool_decide (a ≠ b))] emp ). + + Definition specs := + ctor_spec ** + copy_ctor_spec ** + copy_assign_spec ** + move_ctor_spec ** + move_assign_spec ** + op_eq_spec ** + op_neq_spec ** + dtor_spec . + + End specs. + + Section proofs. + Context `{MOD : test_cpp.module ⊧ σ}. + Import linearity auto_frac. + Import wp_path.WpPrimRSep. + + Lemma copy_assign_ok : + denoteModule module |-- copy_assign_spec. + Proof using MOD. + verify_spec. go with pick_frac. + (* errors.Errors.UNSUPPORTED.body + "wp_method_shift: defaulted methods"%pstring *) + Fail Qed. + Admitted. + Definition copy_assign_B := [LINK] copy_assign_ok. + + Lemma copy_ctor_ok : + denoteModule module |-- copy_ctor_spec. + Proof using MOD. verify_spec. go with pick_frac. Qed. + Definition copy_ctor_B := [LINK] copy_ctor_ok. + + Lemma ctor_ok : + denoteModule module |-- ctor_spec. + Proof using MOD. verify_spec. go with pick_frac. Qed. + Definition ctor_B := [LINK] ctor_ok. + + Lemma dtor_ok : + denoteModule module |-- dtor_spec. + Proof using MOD. verify_spec. go with pick_frac. Qed. + Definition dtor_B := [LINK] dtor_ok. + + Lemma move_assign_ok : + denoteModule module |-- move_assign_spec. + Proof using MOD. + verify_spec. go with pick_frac. + + Fail Qed. + Admitted. + Definition move_assign_B := [LINK] move_assign_ok. + + Lemma move_ctor_ok : + denoteModule module |-- move_ctor_spec. + Proof using MOD. verify_spec. go with pick_frac. Qed. + Definition move_ctor_B := [LINK] move_ctor_ok. + + Import join.manual_expr_condition. + Import reduce_bool_decide. + + Lemma iff_eqv_both_or_neither {P Q : Prop} `{HdecP : !Decision P} : + (P <-> Q) <-> (P ∧ Q) ∨ (¬ P ∧ ¬ Q). + Proof. + split. + - by move => <-; case: HdecP; [left|right]. + - by move => [] [HP HQ]. + Qed. + + Lemma op_eq_ok : + denoteModule module |-- op_eq_spec. + Proof using MOD. + verify_spec. + case: (bool_decide_reflect (a = b)) => Hab. + - go using prim.primR_aggressiveC with smash_delayed_case. + by []. + - go with pick_frac smash_delayed_case; iIntros "!%". + + rewrite iff_eqv_both_or_neither; right; split; last by []. + move => Hzab. + apply: Hab; by destruct a, b; f_equal. + + by rewrite iff_eqv_both_or_neither; right; split => +. + + by rewrite iff_eqv_both_or_neither; right; split => +. + Qed. + Definition op_eq_B := [LINK] op_eq_ok. + + Lemma op_neq_ok : + denoteModule module |-- op_neq_spec. + Proof using MOD. + verify_spec. wapply op_eq_ok. + go using prim.primR_aggressiveC. + by []. + Qed. + Definition op_neq_B := [LINK] op_neq_ok. + + End proofs. + End with_cpp. +End Aggregate. + +#[local] Hint Resolve Aggregate.copy_assign_B : sl_opacity. +#[local] Hint Resolve Aggregate.copy_ctor_B : sl_opacity. +#[local] Hint Resolve Aggregate.ctor_B : sl_opacity. +#[local] Hint Resolve Aggregate.dtor_B : sl_opacity. +#[local] Hint Resolve Aggregate.move_assign_B : sl_opacity. +#[local] Hint Resolve Aggregate.move_ctor_B : sl_opacity. +#[local] Hint Resolve Aggregate.op_eq_B : sl_opacity. +#[local] Hint Resolve Aggregate.op_neq_B : sl_opacity. + +Section with_cpp. + Context `{Σ : cpp_logic, σ : genv}. + + Section defs. + + Definition sum (xs : list Z) : Z := + foldr Z.add 0 xs. + #[global] Arguments sum !_ / : simpl nomatch. + + End defs. + + Section specs. + Context `{MOD : test_cpp.module ⊧ σ}. + + cpp.spec "test(bool, const char*)" as test_spec with + (\arg "b" (Vbool true) + \arg{p} "" (Vptr p) + \post emp). + + cpp.spec "sum(const std::__1::vector>&)" as sum_spec with + ( \arg{vp} "v" (Vptr vp) + \with q vs st size + \prepost vp |-> std.vector.R_cap "unsigned" q size st vs + \post[Vint (trim 32 (sum vs))] emp). + + cpp.spec "TestBasic()" as test_basic with + (\post emp). + + cpp.spec "TestIntIter()" as test_int_iter with + (\post emp). + + cpp.spec "TestForEach()" as test_for_each with + (\post emp). + + cpp.spec "TestAggregate()" as test_aggregate with + (\post emp). + + cpp.spec "main()" as main with + (\post[Vint 0] emp). + + Definition specs := + test_basic ** + main. + End specs. + + Section proofs. + Context `{MOD : test_cpp.module ⊧ σ}. + #[local] Notation alloc_int := (std.allocator.T "int"). + #[local] Notation alloc_uint := (std.allocator.T "unsigned"). + #[local] Notation alloc_agg := (std.allocator.T "Aggregate"). + Implicit Type p : ptr. + + Import linearity. + Import normalize_ptr only_provable_norm. + + (* UPSTREAM. Where? *) + #[global] Instance SplitRecord_prod A B : SplitRecord (@prod A B) := {}. + + Lemma test_int_iter_ok : verify[ module ] test_int_iter. + Proof using MOD. + verify_spec. + time "test_int_iter_ok" go. + Qed. + Definition test_int_iter_B := [LINK] test_int_iter_ok. + #[local] Hint Resolve test_int_iter_B : sl_opacity. + + #[local] Hint Resolve prim.primR_aggressiveC : sl_opacity. + + (* TODO: remove this when we can have a [StepToSubobject] instance for [arrayRL] *) + Import wp_path.WpPrimRSep. + + Lemma test_for_each_ok : verify[ module ] test_for_each. + Proof using MOD. + verify_spec. + time "test_for_each_ok" go. + Qed. + Definition test_for_each_B := [LINK] test_for_each_ok. + #[local] Hint Resolve test_for_each_B : sl_opacity. + + Lemma sum_ok : verify[ module ] sum_spec. + Proof using MOD. + verify_spec. + time "test_for_each_ok" go. + + name_locals; rename + __begin1_addr into beginp, + __end1_addr into endp. + + wp_for (fun _ => + \with basep + \pre{ib} beginp |-> std.vector.iterator.R_const "unsigned" 1$m basep ib + \prepost{ie} endp |-> std.vector.iterator.R_const "unsigned" 1$m basep ie + \prepost{vs} basep |-> arrayLR "unsigned" ib ie (fun v => uintR q v) vs + \pre{r} r_addr |-> uintR 1$m r + \post + r_addr |-> uintR 1$m (trim 32 (r + sum vs)) ∗ + beginp |-> std.vector.iterator.R_const "unsigned" 1$m basep ie ). + + go; wp_if. + { go. } + go. + Qed. + Definition sum_B := [LINK] sum_ok. + #[local] Hint Resolve sum_B : sl_opacity. + + Lemma test_basic_ok : verify[ module ] test_basic. + Proof using MOD. + verify_spec. + go. + Qed. + Definition test_basic_B := [LINK] test_basic_ok. + #[local] Hint Resolve test_basic_B : sl_opacity. + + Lemma test_aggregate_ok : verify[ module ] test_aggregate. + Proof using MOD. + verify_spec. + go. + Qed. + Definition test_aggregate_B := [LINK] test_aggregate_ok. + #[local] Hint Resolve test_aggregate_B : sl_opacity. + + (* TODO: investigate. We get a warning for missing specs but the proof goes through anyway *) + Lemma test_ok : verify[ module ] test_spec. + Proof using MOD. + verify_spec. + go. + Qed. + Definition test_B := [LINK] test_ok. + #[local] Hint Resolve test_B : sl_opacity. + + Lemma main_ok : verify[ module ] main. + Proof using MOD. + verify_spec. + go. + Qed. + + Definition main_B := [LINK] main_ok. + #[local] Hint Resolve main_B : sl_opacity. + + (* NOTE(Simon): this is annoyingly verbose + + Updated: latest update to [SpecFor] instances makes it more concise but the underscore are + still superfluous. + *) + Definition find_spec := + std.find_spec + (std.vector.iterator.T "int") "int" + module + ptr Z _ _ Z _ _. + + (* glue all the proofs together *) + Lemma specs_ok : + denoteModule module ** + ▷ ( std.vector.specs "Aggregate" alloc_agg ** + std.vector.specs "int" alloc_int ** + std.vector.specs "unsigned" alloc_uint ** + std.vector.iterator.specs true "unsigned" ** + std.vector.iterator.specs false "int" ** + find_spec ** + std.cassert.specs) + |-- main. + Proof using MOD. + rewrite /std.vector.specs. + rewrite /std.vector.iterator.specs. + work. + Qed. + + End proofs. +End with_cpp.