Add stdlib examples from geeks_for_geeks

rocq-brick-libstdcpp/Makefile

@@ -3,6 +3,8 @@
 proof: proof/dune.inc
 	dune b
 
-proof/dune.inc: proof/dune-gen.sh proof/cpp2v-dune-gen.sh
-	(cd proof; ./dune-gen.sh)
+proof/dune.inc:
+	dune b @dune_inc --auto-promote || true
+# The --auto-promote option will automatically update the .inc file with the new
+# build rule _and fail if any change is needed_, so we ignore the failure.
 

rocq-brick-libstdcpp/proof/cpp2v-dune-gen.sh

@@ -44,7 +44,7 @@ outRule() {
 	if [ "$system" = 1 ]; then
 		universe=" (universe)"
 	fi
-	local cpp2v="cpp2v -v %{input} -o ${module}"
+	local cpp2v="cpp2v -v %{input} -o ${module} --no-elaborate"
 
 	if [ "$gen_names" = 1 ]; then
 		local names="${name}_${ext}_names.v"

rocq-brick-libstdcpp/proof/dune.inc

@@ -5,7 +5,7 @@
   (alias test_ast)
   (deps (:input inc_cassert.cpp) (glob_files_rec ../*.hpp) (universe))
   (action
-  	 (with-stderr-to inc_cassert_cpp.v.stderr (run cpp2v -v %{input} -o inc_cassert_cpp.v  -- -std=c++20 -stdlib=libstdc++ ))))
+  	 (with-stderr-to inc_cassert_cpp.v.stderr (run cpp2v -v %{input} -o inc_cassert_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps inc_cassert.cpp))
 )
 (subdir cctype
@@ -14,7 +14,7 @@
   (alias test_ast)
   (deps (:input inc_cctype.cpp) (glob_files_rec ../*.hpp) (universe))
   (action
-  	 (with-stderr-to inc_cctype_cpp.v.stderr (run cpp2v -v %{input} -o inc_cctype_cpp.v  -- -std=c++20 -stdlib=libstdc++ ))))
+  	 (with-stderr-to inc_cctype_cpp.v.stderr (run cpp2v -v %{input} -o inc_cctype_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps inc_cctype.cpp))
 )
 (subdir cstdlib
@@ -23,16 +23,25 @@
   (alias test_ast)
   (deps (:input inc_cstdlib.cpp) (glob_files_rec ../*.hpp) (universe))
   (action
-  	 (with-stderr-to inc_cstdlib_cpp.v.stderr (run cpp2v -v %{input} -o inc_cstdlib_cpp.v  -- -std=c++20 -stdlib=libstdc++ ))))
+  	 (with-stderr-to inc_cstdlib_cpp.v.stderr (run cpp2v -v %{input} -o inc_cstdlib_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps inc_cstdlib.cpp))
 )
+(subdir iostream
+ (rule
+  (targets inc_iostream_cpp.v.stderr inc_iostream_cpp.v)
+  (alias test_ast)
+  (deps (:input inc_iostream.cpp) (glob_files_rec ../*.hpp) (universe))
+  (action
+  	 (with-stderr-to inc_iostream_cpp.v.stderr (run cpp2v -v %{input} -o inc_iostream_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps inc_iostream.cpp))
+)
 (subdir mutex
  (rule
   (targets demo_cpp.v.stderr demo_cpp.v)
   (alias test_ast)
   (deps (:input demo.cpp) (glob_files_rec ../*.hpp) (universe))
   (action
-  	 (with-stderr-to demo_cpp.v.stderr (run cpp2v -v %{input} -o demo_cpp.v  -- -std=c++20 -stdlib=libstdc++ ))))
+  	 (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 mutex
@@ -41,7 +50,7 @@
   (alias test_ast)
   (deps (:input inc.hpp) (glob_files_rec ../*.hpp) (universe))
   (action
-  	 (with-stderr-to inc_hpp.v.stderr (run cpp2v -v %{input} -o inc_hpp.v  -- -std=c++20 -stdlib=libstdc++ ))))
+  	 (with-stderr-to inc_hpp.v.stderr (run cpp2v -v %{input} -o inc_hpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps inc.hpp))
 )
 (subdir mutex
@@ -50,7 +59,7 @@
   (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  -- -std=c++20 -stdlib=libstdc++ ))))
+  	 (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 new
@@ -59,7 +68,7 @@
   (alias test_ast)
   (deps (:input inc_new.cpp) (glob_files_rec ../*.hpp) (universe))
   (action
-  	 (with-stderr-to inc_new_cpp.v.stderr (run cpp2v -v %{input} -o inc_new_cpp.v  -- -std=c++20 -stdlib=libstdc++ ))))
+  	 (with-stderr-to inc_new_cpp.v.stderr (run cpp2v -v %{input} -o inc_new_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps inc_new.cpp))
 )
 (subdir semaphore
@@ -68,7 +77,7 @@
   (alias test_ast)
   (deps (:input inc.hpp) (glob_files_rec ../*.hpp) (universe))
   (action
-  	 (with-stderr-to inc_hpp.v.stderr (run cpp2v -v %{input} -o inc_hpp.v  -- -std=c++20 -stdlib=libstdc++ ))))
+  	 (with-stderr-to inc_hpp.v.stderr (run cpp2v -v %{input} -o inc_hpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
  (alias (name srcs) (deps inc.hpp))
 )
 (subdir semaphore
@@ -77,6 +86,15 @@
   (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  -- -std=c++20 -stdlib=libstdc++ ))))
+  	 (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 string
+ (rule
+  (targets inc_string_cpp.v.stderr inc_string_cpp.v)
+  (alias test_ast)
+  (deps (:input inc_string.cpp) (glob_files_rec ../*.hpp) (universe))
+  (action
+  	 (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))
+)

rocq-brick-libstdcpp/proof/iostream/inc_iostream.cpp

@@ -0,0 +1 @@
+#include <iostream>

rocq-brick-libstdcpp/proof/iostream/pred.v

@@ -0,0 +1,48 @@
+(**
+Tentative iostreams specs.
+
+These are trace-based specifications, and there is a _wish_ to move to a
+different style of specifications.
+
+*)
+Require Import skylabs.auto.cpp.prelude.proof.
+Require Export skylabs.cpp.string.
+
+Require Import skylabs.brick.libstdcpp.iostream.inc_iostream_cpp.
+
+(** TODO upstream START *)
+#[only(cfracsplittable)] derive cstring.R.
+
+(** TODO upstream *)
+#[global] Bind Scope bs_scope with cstring.t.
+(* We only have `Bind Scope bs_scope with t.` inside `Module cstring.` *)
+(** TODO upstream END *)
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv}.
+
+  Parameter ostreamT : Type.
+  Parameter ostreamR : cQp.t -> ostreamT -> Rep.
+  Parameter ostream_contentR : cQp.t -> cstring.t -> Rep.
+  (* TODO: type_ptr *)
+  #[only(cfracsplittable)] derive ostreamR.
+  #[only(cfracsplittable)] derive ostream_contentR.
+
+  #[global] Instance: LearnEqF1 ostreamR := ltac:(solve_learnable).
+  #[global] Instance: LearnEqF1 ostream_contentR := ltac:(solve_learnable).
+
+  Parameter istreamT : Type.
+  Parameter istreamR : cQp.t -> istreamT -> Rep.
+  #[only(cfracsplittable)] derive istreamR.
+  #[global] Instance: LearnEqF1 istreamR := ltac:(solve_learnable).
+
+  Lemma ostream_contentR_aggressive (os_p : ptr) q str str':
+    os_p |-> ostream_contentR q str ⊢
+    [| str = str' |] -∗
+    os_p |-> ostream_contentR q str'.
+  Proof. work. Qed.
+  Definition ostream_contentR_aggressiveC := [CANCEL] ostream_contentR_aggressive.
+
+End with_cpp.
+
+#[export] Hint Resolve ostream_contentR_aggressiveC : br_hints.

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

@@ -0,0 +1,95 @@
+(**
+Tentative iostreams specs.
+
+These are trace-based specifications, and there is a _wish_ to move to a
+different style of specifications.
+
+*)
+Require Import skylabs.auto.cpp.prelude.proof.
+Require Export skylabs.cpp.string.
+Require Export skylabs.brick.libstdcpp.iostream.pred.
+
+Require Import skylabs.brick.libstdcpp.iostream.inc_iostream_cpp.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv}.
+
+  cpp.spec "std::operator<<<std::char_traits<char>>(std::basic_ostream<char, std::char_traits<char>>&, const char*)" from source as ostream_insert_spec with (
+    \arg{osP} "" (Vptr osP)
+    \prepost{osM} osP |-> ostreamR 1$m osM
+    \pre{str} osP |-> ostream_contentR 1$m str
+    \arg{strP} "" (Vptr strP)
+    \prepost{q__s strM} strP |-> cstring.R q__s strM
+    \post[Vptr osP]
+      osP |-> ostream_contentR 1$m (str ++ strM)).
+
+  Parameter Z_to_string : Z -> cstring.t.
+  #[global] Declare Instance Z_to_string_inj : Inj eq eq Z_to_string.
+  (** TODO: find an implementation!*)
+
+  cpp.spec "std::basic_ostream<char, std::char_traits<char>>::operator<<(int)" from source as ostream_print_int_spec with (
+    \this this
+    \prepost{osM} this |-> ostreamR 1$m osM
+    \pre{str} this |-> ostream_contentR 1$m str
+    \arg{n} "" (Vint n)
+    \post[Vptr this]
+        this |-> ostream_contentR 1$m (str ++ Z_to_string n)
+  ).
+
+  cpp.spec "std::basic_ostream<char, std::char_traits<char>>::operator<<(unsigned long)" from source as ostream_print_ulong_spec with (
+    \this this
+    \prepost{osM} this |-> ostreamR 1$m osM
+    \pre{str} this |-> ostream_contentR 1$m str
+    \arg{n} "" (Vint n)
+    \post[Vptr this]
+        this |-> ostream_contentR 1$m (str ++ Z_to_string n)
+  ).
+
+  Definition iostream_manip_spec state_f contents_f : WpSpec_cpp_val := (
+    \arg{osP : ptr} "" (Vptr osP)
+    (* XXX: manipulators can modify [osM]! *)
+    \pre{osM} osP |-> ostreamR 1$m osM
+    \post* osP |-> ostreamR 1$m (state_f osM)
+    \pre{str} osP |-> ostream_contentR 1$m str
+    \post[Vptr osP] osP |-> ostream_contentR 1$m (contents_f str)).
+
+  Definition ostream_cpp_type : type :=
+    "std::basic_ostream<char, std::char_traits<char>>&".
+  Definition iostream_manip_kind : okind :=
+    tFunction ostream_cpp_type [ostream_cpp_type].
+
+  cpp.spec "std::endl<char, std::char_traits<char>>(std::basic_ostream<char, std::char_traits<char>>&)" from source as endl_spec with (
+    \exact Reduce iostream_manip_spec (fun osM => osM) (fun str => str ++ "\n")%bs
+  ).
+
+  (* This is the overload taking the endl manipulator. *)
+  (* https://eel.is/c++draft/output.streams#ostream.inserters *)
+  cpp.spec "std::basic_ostream<char, std::char_traits<char>>::operator<<(std::basic_ostream<char, std::char_traits<char>>&(*)(std::basic_ostream<char, std::char_traits<char>>&))"
+    from source as ostream_insert_string_spec with (
+    \this this
+    \arg{os_f} "" (Vptr os_f)
+    \pre{state_f stream_f}
+      os_f |-> unmaterialized_specR
+        iostream_manip_kind
+        (iostream_manip_spec state_f stream_f)
+    \pre{osM} this |-> ostreamR 1$m osM
+    \post* this |-> ostreamR 1$m (state_f osM)
+    \pre{str} this |-> ostream_contentR 1$m str
+    \post[Vptr this]
+      this |-> ostream_contentR 1$m (stream_f str)
+  ).
+
+  (** NOTE: this specification is weak because it does not connect to the
+      actual stream "contents". *)
+  cpp.spec "std::basic_istream<char, std::char_traits<char>>::operator>>(int&)"
+    from source as istream_take_int_spec with (
+    \this this
+    \pre{isM} this |-> istreamR 1$m isM
+    \arg{nP} "" (Vptr nP)
+    \pre nP |-> anyR "int" 1$m
+    \post[Vptr this] Exists isM' n,
+        this |-> istreamR 1$m isM' **
+          nP |-> intR 1$m n
+  ).
+
+End with_cpp.

rocq-brick-libstdcpp/proof/string/inc_string.cpp

@@ -0,0 +1 @@
+#include <string>

rocq-brick-libstdcpp/proof/string/pred.v

@@ -0,0 +1,29 @@
+(**
+Tentative Specifications for <string>
+*)
+Require Import skylabs.auto.cpp.prelude.spec.
+Require Import skylabs.auto.cpp.elpi.derive.
+Require Export skylabs.cpp.string.
+
+Require Import skylabs.brick.libstdcpp.string.inc_string_cpp.
+
+(**
+Model of basic_string<char>/basic_string<char8>.
+
+NOTE: the type `bs` is only suitable for the `char` and `char8` specializations.
+
+To support wider character types, we need to generalize this to something like `list N` or
+`list PrimInt63`.
+*)
+#[global] Notation string_type := bs (only parsing).
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv}.
+
+  Parameter basic_stringR :
+    forall value_type : type, cQp.t -> string_type -> Rep.
+  #[only(type_ptr="std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>",cfracsplittable)] derive basic_stringR.
+
+  #[global] Instance: Cbn (Learn (learn_eq ==> any ==> learn_eq ==> learn_hints.fin) basic_stringR) := ltac:(solve_learnable).
+
+End with_cpp.

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

@@ -0,0 +1,45 @@
+(**
+Tentative Specifications for <string>
+*)
+Require Import skylabs.auto.cpp.prelude.spec.
+Require Export skylabs.cpp.string.
+Require Export skylabs.brick.libstdcpp.string.pred.
+
+Require Import skylabs.brick.libstdcpp.string.inc_string_cpp.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv}.
+
+  Definition N_to_byte (n : N) : Byte.byte :=
+    match Byte.of_N n with
+    | None => Byte.x00 (* TODO: default *)
+    | Some b => b
+    end.
+
+  (* default constructor *)
+  cpp.spec "std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>::basic_string()" from source as string_default_ctor_spec with (
+    \this this
+    \post this |-> basic_stringR "char" 1$m "").
+
+  (* default destructor *)
+  cpp.spec "std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>::~basic_string()" from source as string_dtor_spec with (
+     \this this
+     \pre{s} this |-> basic_stringR "char" 1$m s
+     \post emp).
+
+  cpp.spec "std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>::operator=(char)" from source as string_op_eq_char_spec with (
+    \this this
+    \arg{c} "" (Vchar c)
+    \pre{s} this |-> basic_stringR "char" 1$m s
+    \post[Vptr this]
+      this |-> basic_stringR "char" 1$m (BS.String (N_to_byte c) BS.EmptyString)).
+
+  cpp.spec "std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>::operator=(const std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>&)" from source as string_op_eq_string_spec with (
+    \this this
+    \arg{other} "" (Vref other)
+    \pre{s} this |-> basic_stringR "char" 1$m s
+    \prepost{otherS} other |-> basic_stringR "char" 1$m otherS
+    \post[Vptr this]
+      this |-> basic_stringR "char" 1$m otherS).
+
+End with_cpp.