specifications for std::vector and std::find

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<ty> 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.

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.

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))
+)