From 26cadd5c688d8c3903689bd268abc524c4a8581f Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Fri, 6 Mar 2026 17:23:39 +0100
Subject: [PATCH 1/8] Makefile: build on @dune_inc rules

---
 rocq-brick-libstdcpp/Makefile | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/rocq-brick-libstdcpp/Makefile b/rocq-brick-libstdcpp/Makefile
index ea6ee94..36de449 100644
--- a/rocq-brick-libstdcpp/Makefile
+++ b/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.
 

From 315c150fcd247f053cb869aa513f83c257a286ce Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Fri, 6 Mar 2026 17:24:21 +0100
Subject: [PATCH 2/8] cpp2v-dune-gen.sh: deduplicate

---
 rocq-brick-libstdcpp/test/cpp2v-dune-gen.sh | 139 +-------------------
 1 file changed, 1 insertion(+), 138 deletions(-)
 mode change 100755 => 120000 rocq-brick-libstdcpp/test/cpp2v-dune-gen.sh

diff --git a/rocq-brick-libstdcpp/test/cpp2v-dune-gen.sh b/rocq-brick-libstdcpp/test/cpp2v-dune-gen.sh
deleted file mode 100755
index a228dca..0000000
--- a/rocq-brick-libstdcpp/test/cpp2v-dune-gen.sh
+++ /dev/null
@@ -1,138 +0,0 @@
-#!/bin/bash
-#
-# Copyright (C) 2020-2025 BlueRock Security, 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.
-#
-
-usage() {
-	cat >&2 <<-EOF
-		usage: $(basename "$0") [ -t ] <filename>.<ext> <cpp2v-options> -- [ <clang-options> ]
-
-		This will output (to stdout) dune rules for building <filename>.<ext>,
-		passing <options> to cpp2v. Redirect output to dune.inc and
-		load via dune's include.
-
-		The output is filesystem-independent and <filename>.<ext> need not exist.
-		Placing the output in <base>/dune.inc will transform
-		<base>/<filename>.<ext> into <base>/<filename>_<ext>.v and
-		<base>/<filename>_<ext>_names.v and (with \`-t\`)
-		<base>/<filename>_<ext>_templates.v.
-	EOF
-	exit 1
-}
-
-outRule() {
-	local indent fullName name ext
-	indent="$1"
-	fullName="$2"
-	shift 2
-
-	# The extension starts at the last dot:
-	name="${fullName%.*}"
-	if [ "$name" = "$fullName" ]; then
-		echo -e "Error: filename '$fullName' has no extension\n" >&2
-		usage
-	fi
-	ext="${fullName##*.}"
-
-	local module="${name}_${ext}.v"
-	local targ="${module}"
-	local clang_options=""
-	local universe=""
-	if [ "$system" = 1 ]; then
-		universe=" (universe)"
-	fi
-	local cpp2v="cpp2v -v %{input} -o ${module}"
-
-	if [ "$gen_names" = 1 ]; then
-		local names="${name}_${ext}_names.v"
-		targ="${targ} ${names}"
-		cpp2v="${cpp2v} -names ${names}"
-	fi
-
-	if [ "$templates" = 1 ]; then
-		local templates="${name}_${ext}_templates.v"
-		cpp2v="${cpp2v} --templates=${templates}"
-		targ="$targ ${templates}"
-	fi
-
-	action="(run ${cpp2v} ${1+ $@} ${clang_options})"
-
-	sed "s/^/${indent}/" <<-EOF
-		(rule
-		 (targets ${module}.stderr ${targ})
-		 (alias test_ast)
-		 (deps (:input ${name}.${ext}) (glob_files_rec ${prefix}*.hpp)${universe})
-		 (action
-		 	 (with-stderr-to ${module}.stderr ${action})))
-		(alias (name srcs) (deps ${name}.${ext}))
-	EOF
-	# TODO: maybe drop @srcs alias, seems leftover from !2613
-}
-
-traverse() {
-	local indent path firstDir rest
-	indent="$1"
-	path="$2"
-	shift 2
-	firstDir="${path%%/*}"
-	rest="${path#*/}"
-	if [ "$firstDir" = "$path" ]; then
-		outRule "$indent" "$path" "$@"
-	elif [ "$firstDir" = "." ]; then
-		traverse "$indent" "$rest" "$@"
-	else
-		#echo DIR $firstDir
-		#echo REST $rest
-		echo "${indent}(subdir ${firstDir}"
-		(cd "${firstDir}"; traverse " $indent" "$rest" "$@")
-		echo "${indent})"
-	fi
-}
-
-gen_names=0
-templates=0
-system=0
-prefix="../"
-while :
-do
-	case "$1" in
-	-n)
-		gen_names=1
-		shift
-		;;
-	-t)
-		templates=1
-		shift
-		;;
-	-s)
-		system=1
-		shift
-		;;
-	-p)
-		shift
-		prefix="$1"
-		shift
-		;;
-	--)
-		shift
-		break
-		;;
-	-*)
-		usage
-		;;
-	*)
-		break
-		;;
-	esac
-done
-[ $# -ge 1 ] || usage
-
-path="$1"
-shift
-
-traverse "" "$path" "$@"
-
-# vim:set noet sw=8:
diff --git a/rocq-brick-libstdcpp/test/cpp2v-dune-gen.sh b/rocq-brick-libstdcpp/test/cpp2v-dune-gen.sh
new file mode 120000
index 0000000..ce60b52
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/cpp2v-dune-gen.sh
@@ -0,0 +1 @@
+../proof/cpp2v-dune-gen.sh
\ No newline at end of file

From b95c20861ff4a397359184da515e5ad0a60caeaf Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Fri, 6 Mar 2026 17:26:26 +0100
Subject: [PATCH 3/8] cpp2v-dune-gen.sh: add --no-elaborate to avoid SIGSEGV on
 stdlib

---
 rocq-brick-libstdcpp/proof/cpp2v-dune-gen.sh |  2 +-
 rocq-brick-libstdcpp/proof/dune.inc          | 18 +++++++++---------
 rocq-brick-libstdcpp/test/dune.inc           |  6 +++---
 3 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/cpp2v-dune-gen.sh b/rocq-brick-libstdcpp/proof/cpp2v-dune-gen.sh
index a228dca..d6ef98b 100755
--- a/rocq-brick-libstdcpp/proof/cpp2v-dune-gen.sh
+++ b/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"
diff --git a/rocq-brick-libstdcpp/proof/dune.inc b/rocq-brick-libstdcpp/proof/dune.inc
index dd49356..6d6db53 100644
--- a/rocq-brick-libstdcpp/proof/dune.inc
+++ b/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,7 +23,7 @@
   (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 mutex
@@ -32,7 +32,7 @@
   (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 +41,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 +50,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 +59,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 +68,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 +77,6 @@
   (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))
 )
diff --git a/rocq-brick-libstdcpp/test/dune.inc b/rocq-brick-libstdcpp/test/dune.inc
index 37569d2..7a4d9ff 100644
--- a/rocq-brick-libstdcpp/test/dune.inc
+++ b/rocq-brick-libstdcpp/test/dune.inc
@@ -5,7 +5,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 cstdlib
@@ -14,7 +14,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
@@ -23,6 +23,6 @@
   (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))
 )

From 74fb1eee4ca7261608beaca38b20c538e13fa63f Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Fri, 6 Mar 2026 17:27:51 +0100
Subject: [PATCH 4/8] Add string and iostreams draft specs

---
 rocq-brick-libstdcpp/proof/dune.inc           | 18 ++++
 .../proof/iostream/inc_iostream.cpp           |  1 +
 rocq-brick-libstdcpp/proof/iostream/pred.v    | 54 +++++++++++
 rocq-brick-libstdcpp/proof/iostream/spec.v    | 95 +++++++++++++++++++
 .../proof/string/inc_string.cpp               |  1 +
 rocq-brick-libstdcpp/proof/string/pred.v      | 39 ++++++++
 rocq-brick-libstdcpp/proof/string/spec.v      | 45 +++++++++
 7 files changed, 253 insertions(+)
 create mode 100644 rocq-brick-libstdcpp/proof/iostream/inc_iostream.cpp
 create mode 100644 rocq-brick-libstdcpp/proof/iostream/pred.v
 create mode 100644 rocq-brick-libstdcpp/proof/iostream/spec.v
 create mode 100644 rocq-brick-libstdcpp/proof/string/inc_string.cpp
 create mode 100644 rocq-brick-libstdcpp/proof/string/pred.v
 create mode 100644 rocq-brick-libstdcpp/proof/string/spec.v

diff --git a/rocq-brick-libstdcpp/proof/dune.inc b/rocq-brick-libstdcpp/proof/dune.inc
index 6d6db53..e5f2d43 100644
--- a/rocq-brick-libstdcpp/proof/dune.inc
+++ b/rocq-brick-libstdcpp/proof/dune.inc
@@ -26,6 +26,15 @@
   	 (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)
@@ -80,3 +89,12 @@
   	 (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))
+)
diff --git a/rocq-brick-libstdcpp/proof/iostream/inc_iostream.cpp b/rocq-brick-libstdcpp/proof/iostream/inc_iostream.cpp
new file mode 100644
index 0000000..604782e
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/iostream/inc_iostream.cpp
@@ -0,0 +1 @@
+#include <iostream>
diff --git a/rocq-brick-libstdcpp/proof/iostream/pred.v b/rocq-brick-libstdcpp/proof/iostream/pred.v
new file mode 100644
index 0000000..d8cdec2
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/iostream/pred.v
@@ -0,0 +1,54 @@
+(**
+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.
+
+(** TODO upstream *)
+#[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.` *)
+
+Require Import skylabs.brick.libstdcpp.iostream.inc_iostream_cpp.
+
+(** TODO: split this into pred.v and spec.v *)
+
+(** TODO upstream to auto *)
+#[global] Instance refine_bs_app' (str a b : BS.t) :
+  Refine1 true true (str ++ a = str ++ b)%bs [a = b].
+Proof. tac_refine. exact: (inj (BS.append str)). Qed.
+
+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.
diff --git a/rocq-brick-libstdcpp/proof/iostream/spec.v b/rocq-brick-libstdcpp/proof/iostream/spec.v
new file mode 100644
index 0000000..3851fd6
--- /dev/null
+++ b/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.
diff --git a/rocq-brick-libstdcpp/proof/string/inc_string.cpp b/rocq-brick-libstdcpp/proof/string/inc_string.cpp
new file mode 100644
index 0000000..d5a7322
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/string/inc_string.cpp
@@ -0,0 +1 @@
+#include <string>
diff --git a/rocq-brick-libstdcpp/proof/string/pred.v b/rocq-brick-libstdcpp/proof/string/pred.v
new file mode 100644
index 0000000..f806a37
--- /dev/null
+++ b/rocq-brick-libstdcpp/proof/string/pred.v
@@ -0,0 +1,39 @@
+(**
+Tentative Specifications for <string>
+*)
+Require Import skylabs.auto.cpp.prelude.spec.
+Require Import skylabs.auto.cpp.elpi.derive.
+Require Export skylabs.cpp.string.
+
+(** TODO upstream *)
+#[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.` *)
+
+Require Import skylabs.brick.libstdcpp.string.inc_string_cpp.
+
+(** TODO: split this into pred.v and spec.v *)
+
+(** TODO upstream to auto *)
+#[global] Instance refine_bs_app' (str a b : BS.t) :
+  Refine1 true true (str ++ a = str ++ b)%bs [a = b].
+Proof. tac_refine. exact: (inj (BS.append str)). Qed.
+
+#[global] Notation string_type := bs (only parsing).
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv}.
+
+  (* 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`
+   *)
+  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.
diff --git a/rocq-brick-libstdcpp/proof/string/spec.v b/rocq-brick-libstdcpp/proof/string/spec.v
new file mode 100644
index 0000000..7a9bde9
--- /dev/null
+++ b/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.

From 31de00b486eaf0f024e9702e41640bcdd5cc98f6 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Fri, 6 Mar 2026 17:28:04 +0100
Subject: [PATCH 5/8] Add geeks_for_geeks examples

Co-authored-by: Gregory Malecha <gregory@skylabs-ai.com>
---
 rocq-brick-libstdcpp/test/dune.inc            | 63 +++++++++++++++++++
 .../geeks_for_geeks_examples/N12_area.cpp     | 32 ++++++++++
 .../test/geeks_for_geeks_examples/N12_area.v  | 37 +++++++++++
 .../N1_hello_world.cpp                        | 12 ++++
 .../geeks_for_geeks_examples/N1_hello_world.v | 20 ++++++
 .../test/geeks_for_geeks_examples/N4_sum.cpp  | 13 ++++
 .../test/geeks_for_geeks_examples/N4_sum.v    | 20 ++++++
 .../geeks_for_geeks_examples/N4_sum_a.cpp     | 20 ++++++
 .../test/geeks_for_geeks_examples/N4_sum_a.v  | 35 +++++++++++
 .../test/geeks_for_geeks_examples/N5_swap.cpp | 18 ++++++
 .../test/geeks_for_geeks_examples/N5_swap.v   | 34 ++++++++++
 .../geeks_for_geeks_examples/N5_swap_a.cpp    | 16 +++++
 .../test/geeks_for_geeks_examples/N5_swap_a.v | 35 +++++++++++
 .../N6_print_sizeof.cpp                       | 32 ++++++++++
 .../N6_print_sizeof.v                         | 35 +++++++++++
 .../test/geeks_for_geeks_examples/README.md   |  6 ++
 16 files changed, 428 insertions(+)
 create mode 100644 rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N12_area.cpp
 create mode 100644 rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N12_area.v
 create mode 100644 rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N1_hello_world.cpp
 create mode 100644 rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N1_hello_world.v
 create mode 100644 rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N4_sum.cpp
 create mode 100644 rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N4_sum.v
 create mode 100644 rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N4_sum_a.cpp
 create mode 100644 rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N4_sum_a.v
 create mode 100644 rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap.cpp
 create mode 100644 rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap.v
 create mode 100644 rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap_a.cpp
 create mode 100644 rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap_a.v
 create mode 100644 rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N6_print_sizeof.cpp
 create mode 100644 rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N6_print_sizeof.v
 create mode 100644 rocq-brick-libstdcpp/test/geeks_for_geeks_examples/README.md

diff --git a/rocq-brick-libstdcpp/test/dune.inc b/rocq-brick-libstdcpp/test/dune.inc
index 7a4d9ff..7e1c50a 100644
--- a/rocq-brick-libstdcpp/test/dune.inc
+++ b/rocq-brick-libstdcpp/test/dune.inc
@@ -17,6 +17,69 @@
   	 (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 geeks_for_geeks_examples
+ (rule
+  (targets N12_area_cpp.v.stderr N12_area_cpp.v)
+  (alias test_ast)
+  (deps (:input N12_area.cpp) (glob_files_rec ../*.hpp) (universe))
+  (action
+  	 (with-stderr-to N12_area_cpp.v.stderr (run cpp2v -v %{input} -o N12_area_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps N12_area.cpp))
+)
+(subdir geeks_for_geeks_examples
+ (rule
+  (targets N1_hello_world_cpp.v.stderr N1_hello_world_cpp.v)
+  (alias test_ast)
+  (deps (:input N1_hello_world.cpp) (glob_files_rec ../*.hpp) (universe))
+  (action
+  	 (with-stderr-to N1_hello_world_cpp.v.stderr (run cpp2v -v %{input} -o N1_hello_world_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps N1_hello_world.cpp))
+)
+(subdir geeks_for_geeks_examples
+ (rule
+  (targets N4_sum_cpp.v.stderr N4_sum_cpp.v)
+  (alias test_ast)
+  (deps (:input N4_sum.cpp) (glob_files_rec ../*.hpp) (universe))
+  (action
+  	 (with-stderr-to N4_sum_cpp.v.stderr (run cpp2v -v %{input} -o N4_sum_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps N4_sum.cpp))
+)
+(subdir geeks_for_geeks_examples
+ (rule
+  (targets N4_sum_a_cpp.v.stderr N4_sum_a_cpp.v)
+  (alias test_ast)
+  (deps (:input N4_sum_a.cpp) (glob_files_rec ../*.hpp) (universe))
+  (action
+  	 (with-stderr-to N4_sum_a_cpp.v.stderr (run cpp2v -v %{input} -o N4_sum_a_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps N4_sum_a.cpp))
+)
+(subdir geeks_for_geeks_examples
+ (rule
+  (targets N5_swap_cpp.v.stderr N5_swap_cpp.v)
+  (alias test_ast)
+  (deps (:input N5_swap.cpp) (glob_files_rec ../*.hpp) (universe))
+  (action
+  	 (with-stderr-to N5_swap_cpp.v.stderr (run cpp2v -v %{input} -o N5_swap_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps N5_swap.cpp))
+)
+(subdir geeks_for_geeks_examples
+ (rule
+  (targets N5_swap_a_cpp.v.stderr N5_swap_a_cpp.v)
+  (alias test_ast)
+  (deps (:input N5_swap_a.cpp) (glob_files_rec ../*.hpp) (universe))
+  (action
+  	 (with-stderr-to N5_swap_a_cpp.v.stderr (run cpp2v -v %{input} -o N5_swap_a_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps N5_swap_a.cpp))
+)
+(subdir geeks_for_geeks_examples
+ (rule
+  (targets N6_print_sizeof_cpp.v.stderr N6_print_sizeof_cpp.v)
+  (alias test_ast)
+  (deps (:input N6_print_sizeof.cpp) (glob_files_rec ../*.hpp) (universe))
+  (action
+  	 (with-stderr-to N6_print_sizeof_cpp.v.stderr (run cpp2v -v %{input} -o N6_print_sizeof_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps N6_print_sizeof.cpp))
+)
 (subdir new
  (rule
   (targets demo_cpp.v.stderr demo_cpp.v)
diff --git a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N12_area.cpp b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N12_area.cpp
new file mode 100644
index 0000000..b7a8cbe
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N12_area.cpp
@@ -0,0 +1,32 @@
+// https://www.geeksforgeeks.org/cpp/cpp-program-to-find-area-and-perimeter-of-rectangle/
+
+// C++ program to find area
+// and perimeter of rectangle
+#include<iostream>
+using namespace std;
+
+// Utility function
+int areaRectangle(int a, int b)
+{
+   int area = a * b;
+   return area;
+}
+
+int perimeterRectangle(int a, int b)
+{
+   int perimeter = 2*(a + b);
+   return perimeter;
+}
+
+// Driver code
+int main()
+{
+  int a = 5;
+  int b = 6;
+  cout << "Area = " <<
+           areaRectangle(a, b) <<
+           endl;
+  cout << "Perimeter = " <<
+           perimeterRectangle(a, b);
+  return 0;
+}
diff --git a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N12_area.v b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N12_area.v
new file mode 100644
index 0000000..b1b7dc5
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N12_area.v
@@ -0,0 +1,37 @@
+Require Import skylabs.auto.cpp.prelude.proof.
+Require Import skylabs.brick.libstdcpp.iostream.spec.
+
+Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.N12_area_cpp.
+
+Import linearity.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv}.
+
+  Definition area_of_rectangle (side1 side2 : Z) := side1 * side2.
+  Definition perimeter_of_rectangle (side1 side2 : Z) := 2 * (side1 + side2).
+  Definition side1 := 5.
+  Definition side2 := 6.
+
+  cpp.spec "main()" from source as main_spec with (
+    \prepost{osM} _global "std::cout" |-> ostreamR 1$m osM
+    \pre{str} _global "std::cout" |-> ostream_contentR 1$m str
+    \post[Vint 0]
+      _global "std::cout" |-> ostream_contentR 1$m
+        (str ++ "Area = " ++ Z_to_string (area_of_rectangle side1 side2) ++ "\n" ++ "Perimeter = " ++ Z_to_string (perimeter_of_rectangle side1 side2))
+  ).
+
+  cpp.spec "areaRectangle(int, int)" from source inline.
+  cpp.spec "perimeterRectangle(int, int)" from source inline.
+
+  Lemma main_ok : verify[source] "main()".
+  Proof.
+    verify_shift; go.
+    iExists (_ : ostreamT → ostreamT), (_ : cstring.t → cstring.t); work with br_erefl; go.
+
+    banish_string_literals.
+    iModIntro.
+    work.
+    by rewrite -!(assoc_L BS.append).
+  Qed.
+End with_cpp.
diff --git a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N1_hello_world.cpp b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N1_hello_world.cpp
new file mode 100644
index 0000000..eef6f4f
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N1_hello_world.cpp
@@ -0,0 +1,12 @@
+// https://www.geeksforgeeks.org/cpp/writing-first-c-program-hello-world-example/
+#include <iostream>
+// #include <bits/stdc++.h>
+
+using namespace std;
+
+int main() {
+  // Printing the name using cout object
+  cout << "Hello World";
+
+  return 0;
+}
diff --git a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N1_hello_world.v b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N1_hello_world.v
new file mode 100644
index 0000000..968092f
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N1_hello_world.v
@@ -0,0 +1,20 @@
+Require Import skylabs.auto.cpp.prelude.proof.
+Require Import skylabs.brick.libstdcpp.iostream.spec.
+
+Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.N1_hello_world_cpp.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv}.
+
+  cpp.spec "main()" from source as main_spec with (
+    \prepost{osM} _global "std::cout" |-> ostreamR 1$m osM
+    \pre{str} _global "std::cout" |-> ostream_contentR 1$m str
+    \post[Vint 0]
+      _global "std::cout" |-> ostream_contentR 1$m (str ++ "Hello World")).
+
+  Lemma main_ok : verify[source] "main()".
+  Proof.
+    verify_spec; go.
+  Qed.
+
+End with_cpp.
diff --git a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N4_sum.cpp b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N4_sum.cpp
new file mode 100644
index 0000000..b4c759e
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N4_sum.cpp
@@ -0,0 +1,13 @@
+// https://www.geeksforgeeks.org/cpp/cpp-add-numbers/
+
+#include <iostream>
+using namespace std;
+
+int main() {
+    int a = 11, b = 9;
+
+    // Adding the two numbers and printing
+    // their sum
+    cout << a + b;
+    return 0;
+}
diff --git a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N4_sum.v b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N4_sum.v
new file mode 100644
index 0000000..ebed51a
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N4_sum.v
@@ -0,0 +1,20 @@
+Require Import skylabs.auto.cpp.prelude.proof.
+Require Import skylabs.brick.libstdcpp.iostream.spec.
+
+Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.N4_sum_cpp.
+
+Import linearity.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv}.
+
+  cpp.spec "main()" from source as main_spec with (
+    \prepost{osM} _global "std::cout" |-> ostreamR 1$m osM
+    \pre{str} _global "std::cout" |-> ostream_contentR 1$m str
+    \post[Vint 0]
+      _global "std::cout" |-> ostream_contentR 1$m (str ++ Z_to_string 20)
+  ).
+
+  Lemma main_ok : verify[source] "main()".
+  Proof. verify_spec; go. Qed.
+End with_cpp.
diff --git a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N4_sum_a.cpp b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N4_sum_a.cpp
new file mode 100644
index 0000000..bbadd7f
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N4_sum_a.cpp
@@ -0,0 +1,20 @@
+// https://www.geeksforgeeks.org/cpp/cpp-add-numbers/, 2nd version
+
+#include <iostream>
+using namespace std;
+
+int main() {
+    int a = 11, b = 9;
+
+    // If b is positive, increment a to b times
+    for (int i = 0; i < b; i++)
+        a++;
+
+    // If b is negative, decrement a to |b| times
+    for (int i = 0; i > b; i--)
+        a--;
+
+    cout << a;
+
+    return 0;
+}
diff --git a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N4_sum_a.v b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N4_sum_a.v
new file mode 100644
index 0000000..0ec0bc3
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N4_sum_a.v
@@ -0,0 +1,35 @@
+Require Import skylabs.auto.cpp.prelude.proof.
+Require Import skylabs.brick.libstdcpp.iostream.spec.
+
+Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.N4_sum_a_cpp.
+
+Import linearity.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv}.
+
+  cpp.spec "main()" from source as main_spec with (
+    \prepost{osM} _global "std::cout" |-> ostreamR 1$m osM
+    \pre{str} _global "std::cout" |-> ostream_contentR 1$m str
+    \post[Vint 0]
+      _global "std::cout" |-> ostream_contentR 1$m (str ++ Z_to_string 20)
+  ).
+
+  Lemma main_ok : verify[source] main_spec.
+  Proof.
+    verify_spec; go.
+
+    wp_for (fun ρ =>
+      \pre{i1} _local ρ "i" |-> intR 1$m i1
+      \pre _local ρ "a" |-> intR 1$m (11 + i1)
+      \require 0 <= i1 <= 9
+      \post* _local ρ "i" |-> anyR "int" 1$m
+      \post* _local ρ "a" |-> intR 1$m 20
+      \post emp
+    ).
+
+    go.
+    wp_if; go.
+    wp_for (fun ρ => emp); go.
+  Qed.
+End with_cpp.
diff --git a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap.cpp b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap.cpp
new file mode 100644
index 0000000..b3b635d
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap.cpp
@@ -0,0 +1,18 @@
+// https://www.geeksforgeeks.org/cpp/cpp-program-to-swap-two-numbers/
+
+#include <iostream>
+using namespace std;
+
+int main(){
+    int a = 2, b = 3;
+
+    cout << "Before swapping a = " << a << " , b = " << b << endl;
+
+    int temp;
+
+    temp = a;
+    a = b;
+    b = temp;
+    cout << "After swapping a = " << a << " , b = " << b << endl;
+    return 0;
+}
diff --git a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap.v b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap.v
new file mode 100644
index 0000000..e82bfcb
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap.v
@@ -0,0 +1,34 @@
+Require Import skylabs.auto.cpp.prelude.proof.
+Require Import skylabs.brick.libstdcpp.iostream.spec.
+
+Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.N5_swap_cpp.
+
+Import linearity.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv}.
+
+  cpp.spec "main()" from source as main_spec with (
+    \prepost{osM} _global "std::cout" |-> ostreamR 1$m osM
+    \pre{str} _global "std::cout" |-> ostream_contentR 1$m str
+    \post[Vint 0]
+      _global "std::cout" |-> ostream_contentR 1$m
+        (str ++
+        "Before swapping a = " ++
+        Z_to_string 2 ++ " , b = " ++ Z_to_string 3 ++ "\n" ++
+        "After swapping a = " ++ Z_to_string 3 ++ " , b = " ++ Z_to_string 2 ++ "\n"
+      )
+  ).
+
+  Lemma main_ok : verify[source] "main()".
+  Proof.
+    verify_shift; go.
+    (* iExists id, (fun str => str ++ "\n")%bs; go. *)
+    iExists (_ : ostreamT → ostreamT), (_ : cstring.t → cstring.t); work with br_erefl; go.
+    iExists (_ : ostreamT → ostreamT), (_ : cstring.t → cstring.t); work with br_erefl; go.
+    banish_string_literals.
+    iModIntro.
+    work.
+    by rewrite -!(assoc_L BS.append).
+  Qed.
+End with_cpp.
diff --git a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap_a.cpp b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap_a.cpp
new file mode 100644
index 0000000..c086682
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap_a.cpp
@@ -0,0 +1,16 @@
+// https://www.geeksforgeeks.org/cpp/cpp-program-to-swap-two-numbers/, 2nd version without using temporary variable
+#include <iostream>
+using namespace std;
+
+int main(){
+    int a = 2, b = 3;
+
+    cout << "Before swapping a = " << a << " , b = " << b << endl;
+
+    b = a + b;
+    a = b - a;
+    b = b - a;
+
+    cout << "After swapping a = " << a << " , b = " << b << endl;
+    return 0;
+}
diff --git a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap_a.v b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap_a.v
new file mode 100644
index 0000000..8c9e44c
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap_a.v
@@ -0,0 +1,35 @@
+Require Import skylabs.auto.cpp.prelude.proof.
+Require Import skylabs.brick.libstdcpp.iostream.spec.
+
+Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.N5_swap_a_cpp.
+
+Import linearity.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv}.
+
+  cpp.spec "main()" from source as main_spec with (
+    \prepost{osM} _global "std::cout" |-> ostreamR 1$m osM
+    \pre{str} _global "std::cout" |-> ostream_contentR 1$m str
+    \post[Vint 0]
+      _global "std::cout" |-> ostream_contentR 1$m
+        (str ++
+        "Before swapping a = " ++
+        Z_to_string 2 ++ " , b = " ++ Z_to_string 3 ++ "\n" ++
+        "After swapping a = " ++ Z_to_string 3 ++ " , b = " ++ Z_to_string 2 ++ "\n"
+      )
+  ).
+
+  Lemma main_ok : verify[source] "main()".
+  Proof.
+    verify_shift; go.
+    (* iExists id, (fun str => str ++ "\n")%bs; go. *)
+    iExists (_ : ostreamT → ostreamT), (_ : cstring.t → cstring.t); work with br_erefl; go.
+    iExists (_ : ostreamT → ostreamT), (_ : cstring.t → cstring.t); work with br_erefl; go.
+    banish_string_literals.
+    iModIntro.
+    work.
+    by rewrite -!(assoc_L BS.append).
+  Qed.
+End with_cpp.
+
diff --git a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N6_print_sizeof.cpp b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N6_print_sizeof.cpp
new file mode 100644
index 0000000..c7e00df
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N6_print_sizeof.cpp
@@ -0,0 +1,32 @@
+// https://www.geeksforgeeks.org/cpp/cpp-program-to-find-the-size-of-int-float-double-and-char/
+#include <iostream>
+using namespace std;
+
+int main()
+{
+    int integerType;
+    char charType;
+    float floatType;
+    double doubleType;
+
+    // Calculate and Print
+    // the size of integer type
+    cout << "Size of int is: " << sizeof(integerType)
+         << "\n";
+
+    // Calculate and Print
+    // the size of doubleType
+    cout << "Size of char is: " << sizeof(charType) << "\n";
+
+    // Calculate and Print
+    // the size of charType
+    cout << "Size of float is: " << sizeof(floatType)
+         << "\n";
+
+    // Calculate and Print
+    // the size of floatType
+    cout << "Size of double is: " << sizeof(doubleType)
+         << "\n";
+
+    return 0;
+}
diff --git a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N6_print_sizeof.v b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N6_print_sizeof.v
new file mode 100644
index 0000000..e4b6f57
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N6_print_sizeof.v
@@ -0,0 +1,35 @@
+Require Import skylabs.auto.cpp.prelude.proof.
+Require Import skylabs.brick.libstdcpp.iostream.spec.
+
+Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.N6_print_sizeof_cpp.
+
+Import linearity.
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, σ : genv}.
+
+  Definition newline := "
+"%bs.
+
+  cpp.spec "main()" from source as main_spec with (
+    \prepost{osM} _global "std::cout" |-> ostreamR 1$m osM
+    \pre{str} _global "std::cout" |-> ostream_contentR 1$m str
+    \post[Vint 0]
+      _global "std::cout" |-> ostream_contentR 1$m
+        (str ++
+        "Size of int is: " ++ Z_to_string 4 ++ newline ++
+        "Size of char is: " ++ Z_to_string 1 ++ newline ++
+        "Size of float is: " ++ Z_to_string 4 ++ newline ++
+        "Size of double is: " ++ Z_to_string 8 ++ newline)
+  ).
+
+  Lemma main_ok : verify[source] "main()".
+  Proof.
+    verify_shift; go.
+
+    banish_string_literals.
+    iModIntro.
+    work.
+    by rewrite -!(assoc_L BS.append).
+  Qed.
+End with_cpp.
diff --git a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/README.md b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/README.md
new file mode 100644
index 0000000..a315d1f
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/README.md
@@ -0,0 +1,6 @@
+Geeks 4 Geeks Example Verifications
+============================================
+
+This directory contains verifications of several example programs drawn from
+[geeksforgeeks.org](https://www.geeksforgeeks.org/cpp/cpp-programming-examples/).
+

From b38a92ded7b4d3172448be16aa39168e923461a2 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Fri, 6 Mar 2026 23:55:18 +0100
Subject: [PATCH 6/8] Dedup things to upstream

---
 rocq-brick-libstdcpp/proof/string/pred.v | 11 -----------
 1 file changed, 11 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/string/pred.v b/rocq-brick-libstdcpp/proof/string/pred.v
index f806a37..606e9e3 100644
--- a/rocq-brick-libstdcpp/proof/string/pred.v
+++ b/rocq-brick-libstdcpp/proof/string/pred.v
@@ -5,21 +5,10 @@ Require Import skylabs.auto.cpp.prelude.spec.
 Require Import skylabs.auto.cpp.elpi.derive.
 Require Export skylabs.cpp.string.
 
-(** TODO upstream *)
-#[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.` *)
-
 Require Import skylabs.brick.libstdcpp.string.inc_string_cpp.
 
 (** TODO: split this into pred.v and spec.v *)
 
-(** TODO upstream to auto *)
-#[global] Instance refine_bs_app' (str a b : BS.t) :
-  Refine1 true true (str ++ a = str ++ b)%bs [a = b].
-Proof. tac_refine. exact: (inj (BS.append str)). Qed.
 
 #[global] Notation string_type := bs (only parsing).
 

From 19f2b6ce99e07b3da7f6734ac00868c1920d14c5 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Fri, 6 Mar 2026 23:55:33 +0100
Subject: [PATCH 7/8] Final cleanups

---
 rocq-brick-libstdcpp/proof/iostream/pred.v | 10 +++++-----
 rocq-brick-libstdcpp/proof/string/pred.v   | 11 ++++++-----
 2 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/iostream/pred.v b/rocq-brick-libstdcpp/proof/iostream/pred.v
index d8cdec2..b90c51e 100644
--- a/rocq-brick-libstdcpp/proof/iostream/pred.v
+++ b/rocq-brick-libstdcpp/proof/iostream/pred.v
@@ -8,22 +8,22 @@ different style of specifications.
 Require Import skylabs.auto.cpp.prelude.proof.
 Require Export skylabs.cpp.string.
 
-(** TODO upstream *)
+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.` *)
 
-Require Import skylabs.brick.libstdcpp.iostream.inc_iostream_cpp.
-
-(** TODO: split this into pred.v and spec.v *)
-
 (** TODO upstream to auto *)
 #[global] Instance refine_bs_app' (str a b : BS.t) :
   Refine1 true true (str ++ a = str ++ b)%bs [a = b].
 Proof. tac_refine. exact: (inj (BS.append str)). Qed.
 
+(** TODO upstream END *)
+
 Section with_cpp.
   Context `{Σ : cpp_logic, σ : genv}.
 
diff --git a/rocq-brick-libstdcpp/proof/string/pred.v b/rocq-brick-libstdcpp/proof/string/pred.v
index 606e9e3..fdcebcf 100644
--- a/rocq-brick-libstdcpp/proof/string/pred.v
+++ b/rocq-brick-libstdcpp/proof/string/pred.v
@@ -7,18 +7,19 @@ Require Export skylabs.cpp.string.
 
 Require Import skylabs.brick.libstdcpp.string.inc_string_cpp.
 
-(** TODO: split this into pred.v and spec.v *)
+(**
+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}.
 
-  (* 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`
-   *)
   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.

From a492ee7e76fc88acb9b1f4dcf958571fcd03d87b Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <paolo@skylabs-ai.com>
Date: Sat, 7 Mar 2026 00:03:12 +0100
Subject: [PATCH 8/8] Drop redundant Refine instance

Implied by the `Inj` instance
---
 rocq-brick-libstdcpp/proof/iostream/pred.v | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/iostream/pred.v b/rocq-brick-libstdcpp/proof/iostream/pred.v
index b90c51e..3f86ebf 100644
--- a/rocq-brick-libstdcpp/proof/iostream/pred.v
+++ b/rocq-brick-libstdcpp/proof/iostream/pred.v
@@ -16,12 +16,6 @@ Require Import skylabs.brick.libstdcpp.iostream.inc_iostream_cpp.
 (** TODO upstream *)
 #[global] Bind Scope bs_scope with cstring.t.
 (* We only have `Bind Scope bs_scope with t.` inside `Module cstring.` *)
-
-(** TODO upstream to auto *)
-#[global] Instance refine_bs_app' (str a b : BS.t) :
-  Refine1 true true (str ++ a = str ++ b)%bs [a = b].
-Proof. tac_refine. exact: (inj (BS.append str)). Qed.
-
 (** TODO upstream END *)
 
 Section with_cpp.