cstring: reviewed specs, with test clients — slice 1

rocq-brick-libstdcpp/proof/cstring/inc_cstring.cpp

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

rocq-brick-libstdcpp/proof/cstring/model.v

@@ -0,0 +1,168 @@
+(*
+ * Copyright (c) 2026 SkyLabs AI, 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.prelude.numbers.
+Require Import skylabs.prelude.list_numbers.
+Require Import skylabs.prelude.bytestring.
+
+#[local] Set Primitive Projections.
+#[local] Open Scope Z_scope.
+
+Definition byte_ord (c : Byte.byte) : Z :=
+  Z.of_N (Byte.to_N c).
+
+Fixpoint strcmp (s1 s2 : bs) : Z :=
+  match s1, s2 with
+  | BS.EmptyString, BS.EmptyString => 0
+  | BS.EmptyString, BS.String c2 _ => - byte_ord c2
+  | BS.String c1 _, BS.EmptyString => byte_ord c1
+  | BS.String c1 rest1, BS.String c2 rest2 =>
+      if bool_decide (c1 = c2) then strcmp rest1 rest2
+      else byte_ord c1 - byte_ord c2
+  end.
+
+Fixpoint strncmp_nat (n : nat) (s1 s2 : bs) : Z :=
+  match n with
+  | O => 0
+  | S n' =>
+      match s1, s2 with
+      | BS.EmptyString, BS.EmptyString => 0
+      | BS.EmptyString, BS.String c2 _ => - byte_ord c2
+      | BS.String c1 _, BS.EmptyString => byte_ord c1
+      | BS.String c1 rest1, BS.String c2 rest2 =>
+          if bool_decide (c1 = c2) then strncmp_nat n' rest1 rest2
+          else byte_ord c1 - byte_ord c2
+      end
+  end.
+
+Definition strncmp (s1 s2 : bs) (n : N) : Z :=
+  strncmp_nat (N.to_nat n) s1 s2.
+
+Definition byte_of_int (c : Z) : Z :=
+  (c mod 256)%Z.
+
+Fixpoint strchr (s : bs) (c : Z) : option Z :=
+  match s with
+  | BS.EmptyString =>
+      if bool_decide (c = 0) then Some 0 else None
+  | BS.String ch rest =>
+      if bool_decide (c = byte_ord ch) then Some 0
+      else option_map (fun off => (1 + off)%Z) (strchr rest c)
+  end.
+
+Fixpoint strrchr (s : bs) (c : Z) : option Z :=
+  match s with
+  | BS.EmptyString =>
+      if bool_decide (c = 0) then Some 0 else None
+  | BS.String ch rest =>
+      match strrchr rest c with
+      | Some off => Some (1 + off)%Z
+      | None =>
+          if bool_decide (c = byte_ord ch) then Some 0 else None
+      end
+  end.
+
+Fixpoint contains (needle : Byte.byte) (haystack : bs) : bool :=
+  match haystack with
+  | BS.EmptyString => false
+  | BS.String ch rest =>
+      bool_decide (needle = ch) || contains needle rest
+  end.
+
+Fixpoint strspn (s accept : bs) : N :=
+  match s with
+  | BS.EmptyString => 0%N
+  | BS.String ch rest =>
+      if contains ch accept then N.succ (strspn rest accept) else 0%N
+  end.
+
+Fixpoint strcspn (s reject : bs) : N :=
+  match s with
+  | BS.EmptyString => 0%N
+  | BS.String ch rest =>
+      if contains ch reject then 0%N else N.succ (strcspn rest reject)
+  end.
+
+Fixpoint strpbrk (s accept : bs) : option Z :=
+  match s with
+  | BS.EmptyString => None
+  | BS.String ch rest =>
+      if contains ch accept then Some 0
+      else option_map (fun off => (1 + off)%Z) (strpbrk rest accept)
+  end.
+
+Fixpoint prefix (needle haystack : bs) : bool :=
+  match needle with
+  | BS.EmptyString => true
+  | BS.String n_ch n_rest =>
+      match haystack with
+      | BS.EmptyString => false
+      | BS.String h_ch h_rest =>
+          bool_decide (n_ch = h_ch) && prefix n_rest h_rest
+      end
+  end.
+
+Fixpoint strstr (haystack needle : bs) : option Z :=
+  match needle with
+  | BS.EmptyString => Some 0
+  | BS.String _ _ =>
+      match haystack with
+      | BS.EmptyString => None
+      | BS.String _ rest =>
+          if prefix needle haystack then Some 0
+          else option_map (fun off => (1 + off)%Z) (strstr rest needle)
+      end
+  end.
+
+Fixpoint memchr (bytes : list Z) (c : Z) : option Z :=
+  match bytes with
+  | nil => None
+  | b :: rest =>
+      if bool_decide (b = byte_of_int c) then Some 0
+      else option_map (fun off => (1 + off)%Z) (memchr rest c)
+  end.
+
+Fixpoint memcmp (bytes1 bytes2 : list Z) : Z :=
+  match bytes1, bytes2 with
+  | nil, nil => 0
+  | nil, b2 :: _ => - b2
+  | b1 :: _, nil => b1
+  | b1 :: rest1, b2 :: rest2 =>
+      if bool_decide (b1 = b2) then memcmp rest1 rest2 else b1 - b2
+  end.
+
+Definition memset (c n : Z) : list Z :=
+  replicateZ n (byte_of_int c).
+
+#[local] Open Scope bs_scope.
+
+Succeed Example strcmp_equal : strcmp "abc" "abc" = 0 := eq_refl.
+Succeed Example strcmp_less : strcmp "abc" "abd" = -1 := eq_refl.
+Succeed Example strcmp_greater : strcmp "abd" "abc" = 1 := eq_refl.
+Succeed Example strcmp_prefix_less : strcmp "ab" "abc" = -99 := eq_refl.
+Succeed Example strcmp_prefix_greater : strcmp "abc" "ab" = 99 := eq_refl.
+
+Succeed Example strncmp_zero : strncmp "abc" "abd" 0 = 0 := eq_refl.
+Succeed Example strncmp_equal_prefix : strncmp "abc" "abd" 2 = 0 := eq_refl.
+Succeed Example strncmp_diff_at_bound : strncmp "abc" "abd" 3 = -1 := eq_refl.
+
+Succeed Example strchr_found : strchr "banana" 98 = Some 0 := eq_refl.
+Succeed Example strchr_null : strchr "banana" 0 = Some 6 := eq_refl.
+Succeed Example strchr_missing : strchr "banana" 122 = None := eq_refl.
+
+Succeed Example strrchr_found : strrchr "banana" 97 = Some 5 := eq_refl.
+Succeed Example strrchr_null : strrchr "banana" 0 = Some 6 := eq_refl.
+
+Succeed Example strspn_prefix : strspn "abcde" "abc" = 3%N := eq_refl.
+Succeed Example strcspn_prefix : strcspn "abcde" "dx" = 3%N := eq_refl.
+Succeed Example strpbrk_found : strpbrk "abcdef" "xyc" = Some 2 := eq_refl.
+Succeed Example strstr_found : strstr "abracadabra" "cad" = Some 4 := eq_refl.
+Succeed Example strstr_empty : strstr "abracadabra" "" = Some 0 := eq_refl.
+
+Succeed Example memchr_found : memchr [97; 0; 98]%Z 98 = Some 2 := eq_refl.
+Succeed Example memchr_missing : memchr [97; 0; 98]%Z 122 = None := eq_refl.
+Succeed Example memcmp_equal : memcmp [97; 0]%Z [97; 0]%Z = 0 := eq_refl.
+Succeed Example memcmp_less : memcmp [97; 0; 120]%Z [97; 0; 121]%Z = -1 := eq_refl.
+Succeed Example memset_wrap : memset 291 2 = [35; 35]%Z := eq_refl.

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

@@ -0,0 +1,204 @@
+(*
+ * Copyright (c) 2026 SkyLabs AI, 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.specs.
+Require Import skylabs.auto.cpp.prelude.proof.
+
+Require Export skylabs.brick.libstdcpp.cstring.model.
+Require Import skylabs.brick.libstdcpp.cstring.inc_cstring_cpp.
+
+#[local] Set Primitive Projections.
+
+#[local] Open Scope Z_scope.
+
+Notation search_result p found :=
+  (match found with
+  | Some 0 => Vptr p
+  | Some off => Vptr (p .[ Tchar ! off ])
+  | None => Vptr nullptr
+  end) (only parsing).
+
+Notation byte_search_result byte_ty p found :=
+  match found with
+  | Some 0 => Vptr p
+  | Some off => Vptr (p .[ byte_ty ! off ])
+  | None => Vptr nullptr
+  end (only parsing).
+
+Section with_cpp.
+  Context `{Σ : cpp_logic, module ⊧ σ}.
+
+  cpp.spec "strlen" with
+    (\arg{s_p} "__s" (Vptr s_p)
+     \prepost{q s} s_p |-> cstring.R q s
+     \require valid<"unsigned long"> (cstring.strlen s)
+     \post[Vint (cstring.strlen s)] emp).
+
+  cpp.spec "strcmp" with
+    (\arg{s1_p} "__s1" (Vptr s1_p)
+     \arg{s2_p} "__s2" (Vptr s2_p)
+     \prepost{q1 s1} s1_p |-> cstring.R q1 s1
+     \prepost{q2 s2} s2_p |-> cstring.R q2 s2
+     \post[Vint (strcmp s1 s2)] emp).
+
+  cpp.spec "strncmp" with
+    (\arg{s1_p} "__s1" (Vptr s1_p)
+     \arg{s2_p} "__s2" (Vptr s2_p)
+     \arg{n} "__n" (Vn n)
+     \prepost{q1 s1} s1_p |-> cstring.R q1 s1
+     \prepost{q2 s2} s2_p |-> cstring.R q2 s2
+     \post[Vint (strncmp s1 s2 n)] emp).
+
+  cpp.spec "strchr(char*, int)" as strchr_mut_spec with
+    (\arg{s_p} "__s" (Vptr s_p)
+     \arg{c} "__c" (Vint c)
+     \prepost{q s} s_p |-> cstring.R q s
+     \require valid<"unsigned char"> c
+     \post[search_result s_p (strchr s c)] emp).
+
+  cpp.spec "strchr(const char*, int)" as strchr_const_spec with
+    (\arg{s_p} "__s" (Vptr s_p)
+     \arg{c} "__c" (Vint c)
+     \prepost{q s} s_p |-> cstring.R q s
+     \require valid<"unsigned char"> c
+     \post[search_result s_p (strchr s c)] emp).
+
+  cpp.spec "strrchr(char*, int)" as strrchr_mut_spec with
+    (\arg{s_p} "__s" (Vptr s_p)
+     \arg{c} "__c" (Vint c)
+     \prepost{q s} s_p |-> cstring.R q s
+     \require valid<"unsigned char"> c
+     \post[search_result s_p (strrchr s c)] emp).
+
+  cpp.spec "strrchr(const char*, int)" as strrchr_const_spec with
+    (\arg{s_p} "__s" (Vptr s_p)
+     \arg{c} "__c" (Vint c)
+     \prepost{q s} s_p |-> cstring.R q s
+     \require valid<"unsigned char"> c
+     \post[search_result s_p (strrchr s c)] emp).
+
+  cpp.spec "strspn" with
+    (\arg{s_p} "__s" (Vptr s_p)
+     \arg{accept_p} "__accept" (Vptr accept_p)
+     \prepost{q s} s_p |-> cstring.R q s
+     \prepost{accept_q accept} accept_p |-> cstring.R accept_q accept
+     \require valid<"unsigned long"> (strspn s accept)
+     \post[Vn (strspn s accept)] emp).
+
+  cpp.spec "strcspn" with
+    (\arg{s_p} "__s" (Vptr s_p)
+     \arg{reject_p} "__reject" (Vptr reject_p)
+     \prepost{q s} s_p |-> cstring.R q s
+     \prepost{reject_q reject} reject_p |-> cstring.R reject_q reject
+     \require valid<"unsigned long"> (strcspn s reject)
+     \post[Vn (strcspn s reject)] emp).
+
+  cpp.spec "strpbrk(char*, const char*)" as strpbrk_mut_spec with
+    (\arg{s_p} "__s" (Vptr s_p)
+     \arg{accept_p} "__accept" (Vptr accept_p)
+     \prepost{q s} s_p |-> cstring.R q s
+     \prepost{accept_q accept} accept_p |-> cstring.R accept_q accept
+     \post[search_result s_p (strpbrk s accept)] emp).
+
+  cpp.spec "strpbrk(const char*, const char*)" as strpbrk_const_spec with
+    (\arg{s_p} "__s" (Vptr s_p)
+     \arg{accept_p} "__accept" (Vptr accept_p)
+     \prepost{q s} s_p |-> cstring.R q s
+     \prepost{accept_q accept} accept_p |-> cstring.R accept_q accept
+     \post[search_result s_p (strpbrk s accept)] emp).
+
+  cpp.spec "strstr(char*, const char*)" as strstr_mut_spec with
+    (\arg{haystack_p} "__haystack" (Vptr haystack_p)
+     \arg{needle_p} "__needle" (Vptr needle_p)
+     \prepost{haystack_q haystack} haystack_p |-> cstring.R haystack_q haystack
+     \prepost{needle_q needle} needle_p |-> cstring.R needle_q needle
+     \post[search_result haystack_p (strstr haystack needle)] emp).
+
+  cpp.spec "strstr(const char*, const char*)" as strstr_const_spec with
+    (\arg{haystack_p} "__haystack" (Vptr haystack_p)
+     \arg{needle_p} "__needle" (Vptr needle_p)
+     \prepost{haystack_q haystack} haystack_p |-> cstring.R haystack_q haystack
+     \prepost{needle_q needle} needle_p |-> cstring.R needle_q needle
+     \post[search_result haystack_p (strstr haystack needle)] emp).
+
+(*  sound but weak in C++17: memchr behaves as if it reads the bytes
+    sequentially and stops as soon as a matching bytes is found: if the array
+    pointed to by ptr is smaller than count, but the match is found within the
+    array, the behavior is well-defined. *)
+  cpp.spec "memchr(void*, int, unsigned long)" as memchr_mut_spec with
+    (\arg{s_p} "__s" (Vptr s_p)
+     \arg{c} "__c" (Vint c)
+     \arg{n} "__n" (Vint n)
+     \prepost{q hi bytes} s_p |-> arrayLR Tuchar 0 hi
+       (fun b : Z => ucharR q b) bytes
+     \require match memchr bytes c with
+              | Some off => True
+              | None => (n <= hi)%Z
+              end
+     (*equivalently: \require hi >= n \/ (hi < n /\ exists off, memchr bytes c = Some off)*)
+     \post[byte_search_result Tuchar s_p
+       (memchr (takeZ n bytes) c)] emp).
+
+  cpp.spec "memchr(const void*, int, unsigned long)" as memchr_const_spec with
+    (\arg{s_p} "__s" (Vptr s_p)
+     \arg{c} "__c" (Vint c)
+     \arg{n} "__n" (Vint n)
+     \prepost{q hi bytes} s_p |-> arrayLR Tuchar 0 hi
+       (fun b : Z => ucharR q b) bytes
+     \require match memchr bytes c with
+              | Some off => True
+              | None => (n <= hi)%Z
+              end
+     (*equivalently: \require hi >= n \/ (hi < n /\ exists off, memchr bytes c = Some off)*)
+     \post[byte_search_result Tuchar s_p
+       (memchr (takeZ n bytes) c)] emp).
+
+   cpp.spec "memchr(void*, int, unsigned long)" as memchr_mut_simple_spec with
+    (\arg{s_p} "__s" (Vptr s_p)
+     \arg{c} "__c" (Vint c)
+     \arg{n} "__n" (Vint n)
+     \prepost{q bytes} s_p |-> arrayLR Tuchar 0 n (fun b : Z => ucharR q b) bytes
+     \post[byte_search_result Tuchar s_p (memchr bytes c)] emp).
+
+  cpp.spec "memchr(const void*, int, unsigned long)" as memchr_const_simple_spec with
+    (\arg{s_p} "__s" (Vptr s_p)
+     \arg{c} "__c" (Vint c)
+     \arg{n} "__n" (Vint n)
+     \prepost{q bytes} s_p |-> arrayLR Tuchar 0 n (fun b : Z => ucharR q b) bytes
+     \post[byte_search_result Tuchar s_p (memchr bytes c)] emp).
+
+  cpp.spec "memcmp" with
+    (\arg{s1_p} "__s1" (Vptr s1_p)
+     \arg{s2_p} "__s2" (Vptr s2_p)
+     \arg{z} "__n" (Vint z)
+     \prepost{q1 bytes1} s1_p |-> arrayLR Tuchar 0 z (fun b : Z => ucharR q1 b) bytes1
+     \prepost{q2 bytes2} s2_p |-> arrayLR Tuchar 0 z (fun b : Z => ucharR q2 b) bytes2
+     \post[Vint (memcmp bytes1 bytes2)] emp).
+
+  cpp.spec "memset" with
+    (\arg{s_p} "__s" (Vptr s_p)
+     \arg{c} "__c" (Vint c)
+     \arg{z} "__n" (Vint z)
+     \pre{l} s_p |-> arrayLR Tuchar 0 z (fun _ : unit => anyR Tuchar 1$m) l (*(replicateZ z tt)*)
+     \post[Vptr s_p] s_p |-> arrayLR Tuchar 0 z (fun b : Z => ucharR 1$m b) (memset c z)).
+
+  cpp.spec "memcpy" with
+    (\arg{dest_p} "__dest" (Vptr dest_p)
+     \arg{src_p} "__src" (Vptr src_p)
+     \arg{z} "__n" (Vint z)
+     \prepost{q bytes} src_p |-> arrayLR Tuchar 0 z (fun b : Z => ucharR q b) bytes
+     \pre{l} dest_p |-> arrayLR Tuchar 0 z (fun _ : unit => anyR Tuchar 1$m) l (*(replicateZ z tt)*)
+     \post[Vptr dest_p] dest_p |-> arrayLR Tuchar 0 z (fun b : Z => ucharR 1$m b) bytes).
+
+  (*Sound but weak: overlapping buffers not supported here*)
+  cpp.spec "memmove" with
+    (\arg{dest_p} "__dest" (Vptr dest_p)
+     \arg{src_p} "__src" (Vptr src_p)
+     \arg{z} "__n" (Vint z)
+     \prepost{q bytes} src_p |-> arrayLR Tuchar 0 z (fun b : Z => ucharR q b) bytes
+     \pre{l} dest_p |-> arrayLR Tuchar 0 z (fun _ : unit => anyR Tuchar 1$m) l (*(replicateZ z tt)*)
+     \post[Vptr dest_p] dest_p |-> arrayLR Tuchar 0 z (fun b : Z => ucharR 1$m b) bytes).
+
+End with_cpp.

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 cstring
+ (rule
+  (targets inc_cstring_cpp.v.stderr inc_cstring_cpp.v)
+  (alias test_ast)
+  (deps (:input inc_cstring.cpp) (glob_files_rec ../*.hpp) (universe))
+  (action
+  	 (with-stderr-to inc_cstring_cpp.v.stderr (run cpp2v -v %{input} -o inc_cstring_cpp.v --no-elaborate  -- -std=c++20 -stdlib=libstdc++ ))))
+ (alias (name srcs) (deps inc_cstring.cpp))
+)
 (subdir iostream
  (rule
   (targets inc_iostream_cpp.v.stderr inc_iostream_cpp.v)