Merge pull request #101 from SkyLabsAI/gmalecha/vector-repfor

[RepFor] instance for [vector<T>] & misc types

Author: pgiarrusso-sl

rocq-brick-libstdcpp/proof/mutex/spec/defer_lock_t.v

@@ -8,6 +8,14 @@ Section with_cpp.
   Parameter R : forall {σ : genv}, cQp.t -> Rep.
   #[only(cfracsplittable, type_ptr="std::defer_lock_t")] derive R.
 
+  Section with_RepFor.
+    Import rep.RepFor.
+    Import RepScheme.
+
+    #[global] Instance repfor `{Σ : cpp_logic} {σ : genv} :
+      rep.RepFor.C "std::defer_lock_t" [ArgType.CFrac] R := {}.
+  End with_RepFor.
+
   cpp.spec "std::defer_lock_t::defer_lock_t(const std::defer_lock_t&)" as defer_lock_copy_ctor_spec from source with (
     \this this
     \arg{other} "other" (Vptr other)

rocq-brick-libstdcpp/proof/mutex/spec/lock_guard.v

@@ -26,6 +26,16 @@ Module lock_guard.
   #[only(type_ptr)] derive R.
   #[only(lazy_unfold)] derive R.
 
+  Section with_RepFor.
+    Import rep.RepFor.
+    Import RepScheme.
+
+    #[global] Instance repfor `{Σ : cpp_logic, !HasStdThreads Σ} {σ : genv} :
+      rep.RepFor.C "std::lock_guard<std::mutex>"
+      [ArgType.Constant _; ArgType.CFrac; ArgType.Constant _]
+      R := {}.
+  End with_RepFor.
+
   (**
   These automated proofs fail, so we prove it by hand.
   [R_cfrac] does not seem too useful (why ever split a lock guard?), but let's

rocq-brick-libstdcpp/proof/mutex/spec/mutex.v

@@ -35,6 +35,16 @@ Section with_cpp.
   Parameter token : forall {HAS_THREADS : HasStdThreads Σ} {σ : genv}, gname -> Qp -> mpred.
   #[only(fractional,fracvalid,asfractional,timeless)] derive token.
 
+  Section with_RepFor.
+    Import rep.RepFor.
+    Import RepScheme.
+
+    #[global] Instance repfor `{!HasStdThreads Σ} {σ : genv} :
+      rep.RepFor.C "std::mutex" [ArgType.Constant _; ArgType.CFrac; ArgType.Constant _]
+        (funI γ q P => R γ q P ∗ pureR (token γ q)) := {}.
+  End with_RepFor.
+
+
   (** A resource enforcing that the thread calling unlock must be the same thread
       that owns the lock
 

rocq-brick-libstdcpp/proof/mutex/spec/unique_lock.v

@@ -48,6 +48,15 @@ NES.Begin unique_lock.
       pureR (m.(mutex_ptr) |-> mutexR (cQp.scale m.(mutex_q) q) m.(mutex_m))
     end.
 
+  Section with_RepFor.
+    Import rep.RepFor.
+    Import RepScheme.
+
+    #[global] Instance repfor `{Σ : cpp_logic} {σ : genv} ty {T} mutexR `{!BasicLockable ty (T:=T) mutexR} :
+      rep.RepFor.C (Tnamed $ "std::unique_lock" .<< Atype ty >>) [ArgType.CFrac; ArgType.Constant _]
+        (R ty mutexR) := {}.
+  End with_RepFor.
+
   Module R_unfold.
     #[only(lazy_unfold(export))] derive R.
   End R_unfold.

rocq-brick-libstdcpp/proof/vector/spec.v

@@ -148,7 +148,7 @@ NES.Begin std.
     (** 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 [array_sliceR] separately. *)
-    #[global] Notation R_alloc_cap ty alloc_ty q size st xs :=
+    #[global] Abbreviation R_alloc_cap ty alloc_ty q size st xs :=
       ( spineR ty alloc_ty q size st **
         pureR (base_pointer st |-> array_sliceR ty 0 size (objR ty q) xs) )%I
       (q in scope cQp_scope, basep in scope bi_scope, size, cap in scope Z_scope ).
@@ -163,6 +163,16 @@ NES.Begin std.
     #[global] Abbreviation R ty q xs :=
       (R_alloc ty (std.allocator.T ty) q xs).
 
+    Section with_RepFor.
+      Import rep.RepFor.
+      Import RepScheme.
+
+      #[global] Instance repfor `{Σ : cpp_logic} {σ : genv} ty aty `(_ : BundledRep ty M) :
+        rep.RepFor.C (T ty aty)
+          [ArgType.CFrac; ArgType.Model _]
+          (λ q xs, R ty q xs) := {}.
+    End with_RepFor.
+
     (** [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.