From 79b073255b50a21d0a1f3ac284d46f7aa6ba2bd9 Mon Sep 17 00:00:00 2001 From: Lennart Beringer Date: Fri, 1 May 2026 03:42:29 -0400 Subject: [PATCH 1/5] Proofs of reviewed specs for slice 1 --- .../proof/cstring/inc_cstring.cpp | 1 + rocq-brick-libstdcpp/proof/cstring/model.v | 168 +++++++ rocq-brick-libstdcpp/proof/cstring/spec.v | 204 ++++++++ rocq-brick-libstdcpp/proof/dune.inc | 9 + rocq-brick-libstdcpp/test/cstring/proof.v | 468 ++++++++++++++++++ rocq-brick-libstdcpp/test/cstring/test.cpp | 282 +++++++++++ rocq-brick-libstdcpp/test/dune.inc | 9 + 7 files changed, 1141 insertions(+) create mode 100644 rocq-brick-libstdcpp/proof/cstring/inc_cstring.cpp create mode 100644 rocq-brick-libstdcpp/proof/cstring/model.v create mode 100644 rocq-brick-libstdcpp/proof/cstring/spec.v create mode 100644 rocq-brick-libstdcpp/test/cstring/proof.v create mode 100644 rocq-brick-libstdcpp/test/cstring/test.cpp diff --git a/rocq-brick-libstdcpp/proof/cstring/inc_cstring.cpp b/rocq-brick-libstdcpp/proof/cstring/inc_cstring.cpp new file mode 100644 index 0000000..819890a --- /dev/null +++ b/rocq-brick-libstdcpp/proof/cstring/inc_cstring.cpp @@ -0,0 +1 @@ +#include diff --git a/rocq-brick-libstdcpp/proof/cstring/model.v b/rocq-brick-libstdcpp/proof/cstring/model.v new file mode 100644 index 0000000..1537350 --- /dev/null +++ b/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. diff --git a/rocq-brick-libstdcpp/proof/cstring/spec.v b/rocq-brick-libstdcpp/proof/cstring/spec.v new file mode 100644 index 0000000..3a4eb5c --- /dev/null +++ b/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. diff --git a/rocq-brick-libstdcpp/proof/dune.inc b/rocq-brick-libstdcpp/proof/dune.inc index b1133fe..7819b9a 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 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) diff --git a/rocq-brick-libstdcpp/test/cstring/proof.v b/rocq-brick-libstdcpp/test/cstring/proof.v new file mode 100644 index 0000000..f0a685e --- /dev/null +++ b/rocq-brick-libstdcpp/test/cstring/proof.v @@ -0,0 +1,468 @@ +(* + * 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.prelude.proof. +Require Import skylabs.brick.libstdcpp.cassert.spec. +Require Import skylabs.brick.libstdcpp.cstring.spec. +Require Export skylabs.cpp.string. + +Require Import skylabs.brick.libstdcpp.test.cstring.test_cpp. + +Import normalize.only_provable_norm. +Import normalize.normalize_ptr. +Import refine_lib. +Import expr_join. + +#[local] Hint Resolve delayed_case.smash_delayed_case_B | 1000 : br_hints. +#[local] Hint Resolve delayed_case.expr_join.smash_delayed_case_B | 1000 : br_hints. + +#[only(cfracsplittable)] derive cstring.R. (*Upstream into auto*) + +Section with_cpp. + Context `{Σ : cpp_logic} {σ:genv} . (*`{MOD : module ⊧ σ}.*) + + cpp.spec "test_strlen()" from module default. + Lemma test_strlen_ok : verify[module] "test_strlen()". + Proof. verify_spec; go. Qed. + + cpp.spec "test_strcmp()" from module default. + Lemma test_strcmp_ok : verify[module] "test_strcmp()". + Proof. verify_spec; go. Qed. + + cpp.spec "test_strncmp()" from module default. + Lemma test_strncmp_ok : verify[module] "test_strncmp()". + Proof. verify_spec; go. Qed. + + #[local] Fixpoint split_bytes_at_null (bytes : list N) : + option (list N * list N) := + match bytes with + | nil => None + | 0%N :: tail => Some (nil, tail) + | b :: rest => + match split_bytes_at_null rest with + | Some (prefix, tail) => Some (b :: prefix, tail) + | None => None + end + end. + + #[local] Lemma split_bytes_at_null_sound bytes prefix tail : + split_bytes_at_null bytes = Some (prefix, tail) -> + bytes = prefix ++ 0%N :: tail /\ + List.Forall (fun b => b <> 0%N) prefix. + Proof. + revert prefix tail. + induction bytes as [|b bytes IH]; intros prefix tail Hsplit; [done|]. + destruct b as [|p]. + - simpl in Hsplit. inversion Hsplit; subst. + split; [reflexivity|constructor]. + - simpl in Hsplit. + destruct (split_bytes_at_null bytes) as [[prefix' tail']|] eqn:Hrec; + [|done]. + inversion Hsplit; subst prefix tail. clear Hsplit. + specialize (IH _ _ eq_refl) as [Hbytes Hfor]. + split. + + simpl. rewrite Hbytes. reflexivity. + + constructor; [discriminate|exact Hfor]. + Qed. + + #[local] Lemma split_bytes_at_null_complete prefix tail : + List.Forall (fun b => b <> 0%N) prefix -> + split_bytes_at_null (prefix ++ 0%N :: tail) = Some (prefix, tail). + Proof. + induction prefix as [|b prefix IH]; intros Hfor. + - reflexivity. + - inversion Hfor as [|? ? Hb Hfor']; subst. + destruct b as [|p]; [done|]. + simpl. + rewrite (IH Hfor'). + reflexivity. + Qed. + + #[local] Definition split_bytes_at_cstring (bytes : list N) : + option (list N * list N) := + match split_bytes_at_null bytes with + | Some (prefix, tail) => Some (prefix ++ [0%N], tail) + | None => None + end. + + #[local] Lemma split_bytes_at_cstring_sound bytes zs tail : + split_bytes_at_cstring bytes = Some (zs, tail) -> + bytes = zs ++ tail /\ + exists prefix, + zs = prefix ++ [0%N] /\ + List.Forall (fun b => b <> 0%N) prefix. + Proof. + rewrite /split_bytes_at_cstring. + destruct (split_bytes_at_null bytes) as [[prefix tail']|] eqn:Hsplit; + [|done]. + intros Hcstring. + inversion Hcstring; subst zs tail. clear Hcstring. + pose proof (split_bytes_at_null_sound _ _ _ Hsplit) as [-> Hfor]. + split. + - change (prefix ++ 0%N :: tail' = (prefix ++ 0%N :: nil) ++ tail'). + rewrite <- app_assoc. + reflexivity. + - eexists. split. + + reflexivity. + + exact Hfor. + Qed. + + (* Currently dead but provable lemmas + #[local] Lemma split_bytes_at_cstring_complete prefix tail : + List.Forall (fun b => b <> 0%N) prefix -> + split_bytes_at_cstring (prefix ++ [0%N] ++ tail) = + Some (prefix ++ [0%N], tail). + Proof. + intros Hfor. + rewrite /split_bytes_at_cstring. + rewrite (split_bytes_at_null_complete prefix tail Hfor). + reflexivity. + Qed. + + #[local] Lemma split_bytes_at_null_spec bytes prefix tail : + split_bytes_at_null bytes = Some (prefix, tail) <-> + bytes = prefix ++ 0%N :: tail /\ + List.Forall (fun b => b <> 0%N) prefix. + Proof. + split. + - apply split_bytes_at_null_sound. + - intros [-> Hfor]. + exact (split_bytes_at_null_complete _ _ Hfor). + Qed. + #[local] Lemma split_bytes_at_cstring_spec bytes zs tail : + split_bytes_at_cstring bytes = Some (zs, tail) <-> + bytes = zs ++ tail /\ + exists prefix, + zs = prefix ++ [0%N] /\ + List.Forall (fun b => b <> 0%N) prefix. + Proof. + split. + - apply split_bytes_at_cstring_sound. + - intros [Hbytes [prefix [Hzs Hfor]]]. + subst zs bytes. + rewrite <- app_assoc. + exact (split_bytes_at_cstring_complete _ _ Hfor). + Qed. + *) + + #[local] Fixpoint pack (zs : list N) : option cstring.t := + match zs with + | nil => None + | 0%N :: nil => Some BS.EmptyString + | 0%N :: _ => None + | b :: rest => + match Byte.of_N b, pack rest with + | Some ch, Some s => Some (BS.String ch s) + | _, _ => None + end + end. + + #[local] Lemma pack_sound zs s : + pack zs = Some s -> + cstring.to_zstring s = zs. + Proof. + revert s. + induction zs as [|b zs IH]; intros s Hpack; [done|]. + destruct b as [|p]. + - destruct zs as [|b zs]. + + simpl in Hpack. inversion Hpack; subst s. + rewrite cstring.to_zstring_unfold. + reflexivity. + + done. + - destruct (Byte.of_N (N.pos p)) as [ch|] eqn:Hbyte. + + destruct (pack zs) as [s'|] eqn:Hpack'. + * rewrite /pack Hbyte /= in Hpack. + fold pack in Hpack. + rewrite Hpack' in Hpack. + injection Hpack as <-. + pose proof (IH s' eq_refl) as Hzs. + rewrite cstring.to_zstring_unfold. + rewrite cstring.to_zstring_unfold in Hzs. + simpl. + rewrite Hzs. + assert (Hto : Byte.to_N ch = N.pos p). + { apply Byte.to_of_N. exact Hbyte. } + pose proof (Byte.to_N_bounded ch) as Hbound_le. + assert (Hbound : (Byte.to_N ch < 256)%N) by lia. + rewrite Ascii.ascii_of_byte_via_N. + rewrite (Ascii.N_ascii_embedding _ Hbound). + rewrite Hto. + reflexivity. + * rewrite /pack Hbyte /= in Hpack. + fold pack in Hpack. + rewrite Hpack' in Hpack. + discriminate. + + rewrite /pack Hbyte /= in Hpack. + discriminate. + Qed. + + #[local] Lemma pack_WF zs s : + pack zs = Some s -> + cstring.WF s. + Proof. + revert s. + induction zs as [|b zs IH]; intros s Hpack; [done|]. + destruct b as [|p]. + - destruct zs as [|b zs]. + + simpl in Hpack. inversion Hpack; subst s. + apply cstring.WF_nil. + + done. + - destruct (Byte.of_N (N.pos p)) as [ch|] eqn:Hbyte. + + destruct (pack zs) as [s'|] eqn:Hpack'. + * rewrite /pack Hbyte /= in Hpack. + fold pack in Hpack. + rewrite Hpack' in Hpack. + injection Hpack as <-. + pose proof (IH s' eq_refl) as Hwf'. + apply cstring.WF_cons. + { intro Hzero. + apply (f_equal Byte.to_N) in Hzero. + assert (Hto : Byte.to_N ch = N.pos p). + { apply Byte.to_of_N. exact Hbyte. } + rewrite Hto in Hzero. + discriminate. } + { exact Hwf'. } + * rewrite /pack Hbyte /= in Hpack. + fold pack in Hpack. + rewrite Hpack' in Hpack. + discriminate. + + rewrite /pack Hbyte /= in Hpack. + discriminate. + Qed. + + #[local] Definition unpack_cstring (bytes : list N) : + option (cstring.t * list N) := + match split_bytes_at_cstring bytes with + | Some (zs, tail) => + match pack zs with + | Some s => Some (s, tail) + | None => None + end + | None => None + end. + + #[local] Lemma unpack_cstring_sound bytes s tail : + unpack_cstring bytes = Some (s, tail) -> + bytes = cstring.to_zstring s ++ tail /\ + cstring.WF s. + Proof. + rewrite /unpack_cstring. + destruct (split_bytes_at_cstring bytes) as [[zs tail']|] eqn:Hsplit; + [|done]. + destruct (pack zs) as [s'|] eqn:Hpack; [|done]. + intros Hunpack. + inversion Hunpack; subst s tail. clear Hunpack. + pose proof (split_bytes_at_cstring_sound _ _ _ Hsplit) as [Hbytes _]. + pose proof (pack_sound _ _ Hpack) as Hzs. + pose proof (pack_WF _ _ Hpack) as Hwf. + split. + - rewrite Hbytes. + rewrite Hzs. + reflexivity. + - exact Hwf. + Qed. + + #[local] Lemma arrayLR_cstring q bytes m tail (p : ptr) s : + bytes = cstring.to_zstring s ++ tail -> + cstring.WF s -> + p |-> arrayLR "char" 0 m (λ v : N, charR q v) bytes ⊢ + [| m = lengthZ bytes |] ∗ + p |-> cstring.R q s ∗ + p |-> arrayLR "char" (m - lengthZ tail) m (λ v : N, charR q v) tail. + Proof. + intros -> Hwf; work. + rewrite arrayLR.unlock _at_sep. + arith_simpl; work. + rewrite _at_sub_0; [|done]. + rewrite /cstring.R /zstring.R; iFrame; done. + Qed. + Hint Resolve arrayLR_cstring : sl_opacity. + + #[local] Lemma cstring_arrayLR q bytes m tail (p : ptr) s : + bytes = cstring.to_zstring s ++ tail -> + cstring.WF s -> + [| m = lengthZ bytes |] ∗ + p |-> cstring.R q s ∗ + p |-> arrayLR "char" (m - lengthZ tail) m (λ v : N, charR q v) tail ⊢ + p |-> arrayLR "char" 0 m (λ v : N, charR q v) bytes. + Proof. + intros -> Hwf; work. + rewrite lengthN_app; arith_simpl. + rewrite /cstring.R /zstring.R; work. + rewrite arrayLR.unlock; arith_simpl; work. + rewrite _at_sub_0; [trivial|done]. + Qed. + Hint Resolve cstring_arrayLR : sl_opacity. + + #[local, program] Definition arrayLR_open_cstring_C + (p : ptr) q k bytes s tail + (Hex : unpack_cstring bytes =[Vm]=> Some (s, tail)) := + \cancelx + \consuming p |-> arrayLR "char" 0 k (λ v : N, charR q v) bytes + \bound qq ss + \proving p |-> cstring.R qq ss + \through [| qq = q |] + \through [| ss = s |] + \deduce p |-> arrayLR "char" (k - lengthZ tail) k + (λ v : N, charR q v) tail + \end@{mpred}. + Next Obligation. + intros p q k bytes s tail Hs%RedEq_eq. + pose proof (unpack_cstring_sound _ _ _ Hs) as [Hbytes0 Hwf0]. work. + rewrite arrayLR_cstring . work. by rewrite app_nil_r. done. + Qed. + #[local] Hint Resolve arrayLR_open_cstring_C : sl_opacity. + + Lemma at_charR_anyR (p : ptr) q x : + p |-> charR q x ⊢ p |-> anyR (Tchar_ char_type.Cchar) q. + Proof. + apply heap_pred._at_cancel. + apply primR_anyR. + Qed. + Lemma arrayR_charR_arrayR_anyR (p : ptr) q xs : + p |-> arrayR (Tchar_ char_type.Cchar) (fun c : N => charR q c) xs ⊢ + p |-> arrayR (Tchar_ char_type.Cchar) + (fun _ : unit => anyR (Tchar_ char_type.Cchar) q) + (replicateN (lengthN xs) ()). + Proof. + revert p. + induction xs as [|x xs IH]. + all: intros p. + - rewrite /lengthN /= !arrayR_nil. reflexivity. + - rewrite arrayR_cons !_at_sep _at_offsetR. + iIntros "(Hty & Hx & Hxs)". + replace (lengthN (x :: xs)) with (N.succ (lengthN xs)) by + (rewrite /lengthN Nat2N.inj_succ; reflexivity). + rewrite replicateN_S. + rewrite arrayR_cons !_at_sep _at_offsetR. + iFrame "Hty". + iSplitL "Hx". + + iApply (at_charR_anyR with "Hx"). + + iApply (IH with "Hxs"). + Qed. + + Lemma arrayLR_charR_arrayLR_anyR (p : ptr) q xs : + p |-> arrayLR (Tchar_ char_type.Cchar) 0 (lengthZ xs) + (fun c : N => charR q c) xs ⊢ + p |-> arrayLR (Tchar_ char_type.Cchar) 0 (lengthZ xs) + (fun _ : unit => anyR (Tchar_ char_type.Cchar) q) + (replicateN (lengthN xs) ()). + Proof. + rewrite arrayLR.unlock _at_sep. + iIntros "[_ Harr]". + rewrite _at_offsetR _at_sub_0; [|done]. + iPoseProof (arrayR_charR_arrayR_anyR _ q with "Harr") as "Harr". + rewrite /arrayLR. + iSplit. + - iPureIntro. + unfold lengthZ, lengthN, replicateN. + rewrite length_replicate. + rewrite Nat2N.id. + lia. + - rewrite _at_offsetR _at_sub_0; [|done]. + iExact "Harr". + Qed. + + #[local, program] Definition arrayLR_close_cstring_C + (p : ptr) q mid k tail s + (Hmid : mid = lengthZ (cstring.to_zstring s)) + (Htailk : (mid = k - lengthZ tail)%Z) := + \cancelx + \consuming p |-> cstring.R q s + \consuming p |-> arrayLR "char" mid k (λ v : N, charR q v) tail + \proving p |-> arrayLR "char" 0 k + (λ _ : unit, anyR "char" q) (replicateN (Z.to_N k) ()) + \end@{mpred}. + Next Obligation. + intros p q mid k tail s Hmid Htailk. + iIntros "[Hs Htail]". + rewrite /cstring.R /zstring.R. + iDestruct "Hs" as "[Hs %Hwf]". + assert (Hk : k = lengthZ (cstring.to_zstring s ++ tail)). + { rewrite lengthN_app. arith_simpl. lia. } + clear Hmid. + subst mid. + iPoseProof + (cstring_arrayLR q (cstring.to_zstring s ++ tail) k tail p s eq_refl Hwf + with "[Hs Htail]") + as "Harr". + { iSplit. + - iPureIntro. exact Hk. + - rewrite /cstring.R /zstring.R. + iSplitL "Hs". + + iFrame. iPureIntro. exact Hwf. + + iFrame "Htail". } + rewrite Hk N2Z.id. + iPoseProof (arrayLR_charR_arrayLR_anyR _ q (cstring.to_zstring s ++ tail) + with "Harr") as "Harr". + iExact "Harr". + Qed. + #[local] Hint Resolve arrayLR_close_cstring_C : sl_opacity. + + cpp.spec "test_strlen_array_buffer()" from module default. + Lemma test_strlen_array_buffer_ok : + verify[module] "test_strlen_array_buffer()". + Proof. + verify_spec; go. + Qed. + + cpp.spec "test_strcmp_array_buffer()" from module default. + Lemma test_strcmp_array_buffer_ok : + verify[module] "test_strcmp_array_buffer()". + Proof. + verify_spec; go. + Qed. + + cpp.spec "test_strncmp_array_buffer()" from module default. + Lemma test_strncmp_array_buffer_ok : + verify[module] "test_strncmp_array_buffer()". + Proof. + verify_spec; go. + Qed. + + cpp.spec "test_strchr()" from module default. + Lemma test_strchr_ok : verify[module] "test_strchr()". + Proof. + verify_spec; go. + Arith.arith_simpl; go. + Arith.arith_simpl; go. + Qed. + + cpp.spec "test_strrchr()" from module default. + Lemma test_strrchr_ok : verify[module] "test_strrchr()". + Proof. + verify_spec; go. + Arith.arith_simpl; go. + Arith.arith_simpl; go. + Qed. + + cpp.spec "test_strspn()" from module default. + Lemma test_strspn_ok : verify[module] "test_strspn()". + Proof. verify_spec; go. Qed. + + cpp.spec "test_strcspn()" from module default. + Lemma test_strcspn_ok : verify[module] "test_strcspn()". + Proof. verify_spec; go. Qed. + + cpp.spec "test_strpbrk()" from module default. + Lemma test_strpbrk_ok : verify[module] "test_strpbrk()". + Proof. + verify_spec; go. + Arith.arith_simpl; go. + Qed. + + cpp.spec "test_strstr()" from module default. + Lemma test_strstr_ok : verify[module] "test_strstr()". + Proof. + verify_spec; go. + Arith.arith_simpl; go. + Arith.arith_simpl; go. + Qed. + + cpp.spec "test_cstring_slice1()" from module default. + Lemma test_cstring_slice1_ok : verify[module] "test_cstring_slice1()". + Proof. verify_spec; go. Qed. + +End with_cpp. diff --git a/rocq-brick-libstdcpp/test/cstring/test.cpp b/rocq-brick-libstdcpp/test/cstring/test.cpp new file mode 100644 index 0000000..ab855c4 --- /dev/null +++ b/rocq-brick-libstdcpp/test/cstring/test.cpp @@ -0,0 +1,282 @@ +#include +#include + +void test_strlen() { + assert(std::strlen("") == 0); + assert(std::strlen("a") == 1); + assert(std::strlen("abc") == 3); +} + +void test_strlen_embedded_null() { + assert(std::strlen("ab\0cd") == 2); +} + +void test_strcmp() { + assert(std::strcmp("", "") == 0); + assert(std::strcmp("abc", "abc") == 0); + assert(std::strcmp("abc", "abd") < 0); + assert(std::strcmp("abd", "abc") > 0); + assert(std::strcmp("ab", "abc") < 0); + assert(std::strcmp("abc", "ab") > 0); +} + +void test_strcmp_embedded_null() { + assert(std::strcmp("ab\0x", "ab\0y") == 0); +} + +void test_strncmp() { + assert(std::strncmp("abc", "abd", 0) == 0); + assert(std::strncmp("abc", "abd", 2) == 0); + assert(std::strncmp("abc", "abd", 3) < 0); + assert(std::strncmp("abd", "abc", 3) > 0); + assert(std::strncmp("ab", "abc", 2) == 0); + assert(std::strncmp("ab", "abc", 3) < 0); +} + +void test_strncmp_embedded_null() { + assert(std::strncmp("ab\0x", "ab\0y", 4) == 0); +} + +void test_strlen_array_buffer() { + char s[] = {'a', 'b', '\0', 'c', 'd', '\0'}; + assert(std::strlen(s) == 2); +} + +void test_strcmp_array_buffer() { + char x[] = {'a', 'b', '\0', 'x', '\0'}; + char y[] = {'a', 'b', '\0', 'y', '\0'}; + assert(std::strcmp(x, y) == 0); +} + +void test_strncmp_array_buffer() { + char x[] = {'a', 'b', '\0', 'x', '\0'}; + char y[] = {'a', 'b', '\0', 'y', '\0'}; + assert(std::strncmp(x, y, 4) == 0); +} + +void test_strchr() { + const char *s = "banana"; + const char *empty = ""; + assert(std::strchr(s, 'b') == s); + assert(std::strchr(s, 'n') == s + 2); + assert(std::strchr(s, 'z') == nullptr); + assert(std::strchr(s, '\0') == s + 6); + assert(std::strchr(empty, 'a') == nullptr); + assert(std::strchr(empty, '\0') == empty); +} + +void test_strrchr() { + const char *s = "banana"; + const char *empty = ""; + assert(std::strrchr(s, 'a') == s + 5); + assert(std::strrchr(s, 'b') == s); + assert(std::strrchr(s, 'z') == nullptr); + assert(std::strrchr(s, '\0') == s + 6); + assert(std::strrchr(empty, 'a') == nullptr); + assert(std::strrchr(empty, '\0') == empty); +} + +void test_strspn() { + assert(std::strspn("abcde", "abc") == 3); + assert(std::strspn("abcde", "ba") == 2); + assert(std::strspn("abc", "") == 0); + assert(std::strspn("", "abc") == 0); + assert(std::strspn("aaaa", "a") == 4); + assert(std::strspn("abc", "xyz") == 0); +} + +void test_strcspn() { + assert(std::strcspn("abcde", "dx") == 3); + assert(std::strcspn("abcde", "a") == 0); + assert(std::strcspn("abc", "") == 3); + assert(std::strcspn("", "abc") == 0); + assert(std::strcspn("abc", "xyz") == 3); +} + +void test_strpbrk() { + const char *s = "abcdef"; + assert(std::strpbrk(s, "xyc") == s + 2); + assert(std::strpbrk(s, "fa") == s); + assert(std::strpbrk(s, "xyz") == nullptr); + assert(std::strpbrk(s, "") == nullptr); + assert(std::strpbrk("", "abc") == nullptr); +} + +void test_strstr() { + const char *s = "abracadabra"; + const char *empty = ""; + assert(std::strstr(s, "abra") == s); + assert(std::strstr(s, "cad") == s + 4); + assert(std::strstr(s, "dab") == s + 6); + assert(std::strstr(s, "xyz") == nullptr); + assert(std::strstr(s, "") == s); + assert(std::strstr(empty, "") == empty); + assert(std::strstr(empty, "a") == nullptr); +} + +void test_search_embedded_null_array_buffer() { + char s[] = {'a', 'b', '\0', 'b', 'c', '\0'}; + assert(std::strchr(s, 'b') == s + 1); + assert(std::strchr(s, 'c') == nullptr); + assert(std::strchr(s, '\0') == s + 2); + assert(std::strrchr(s, 'b') == s + 1); + assert(std::strrchr(s, '\0') == s + 2); + assert(std::strspn(s, "abc") == 2); + assert(std::strcspn(s, "c") == 2); + assert(std::strpbrk(s, "c") == nullptr); + assert(std::strpbrk(s, "b") == s + 1); + assert(std::strstr(s, "bc") == nullptr); + assert(std::strstr(s, "b") == s + 1); + assert(std::strstr(s, "") == s); +} + +void test_memchr() { + unsigned char s[] = {'a', 'b', 'c', 'a'}; + assert(std::memchr(s, 'a', 4) == s); + assert(std::memchr(s, 'c', 4) == s + 2); + assert(std::memchr(s, 'z', 4) == nullptr); + assert(std::memchr(s, 'a', 0) == nullptr); + assert(std::memchr(s + 1, 'a', 3) == s + 3); +} + +void test_memchr_embedded_null() { + unsigned char s[] = {'a', '\0', 'b', '\0'}; + assert(std::memchr(s, '\0', 4) == s + 1); + assert(std::memchr(s + 2, '\0', 2) == s + 3); + assert(std::memchr(s, 'b', 4) == s + 2); +} + +void test_memcmp() { + unsigned char abc[] = {'a', 'b', 'c'}; + unsigned char abd[] = {'a', 'b', 'd'}; + unsigned char ab[] = {'a', 'b'}; + + assert(std::memcmp(abc, abc, 3) == 0); + assert(std::memcmp(abc, abd, 3) < 0); + assert(std::memcmp(abd, abc, 3) > 0); + assert(std::memcmp(abc, abd, 2) == 0); + assert(std::memcmp(abc, ab, 0) == 0); +} + +void test_memcmp_embedded_null() { + unsigned char x[] = {'a', '\0', 'x'}; + unsigned char y[] = {'a', '\0', 'y'}; + + assert(std::memcmp(x, y, 2) == 0); + assert(std::memcmp(x, y, 3) < 0); + assert(std::memcmp(y, x, 3) > 0); +} + +void test_memset() { + unsigned char s[] = {'a', 'b', 'c', 'd'}; + + assert(std::memset(s, 'x', 2) == s); + assert(s[0] == 'x'); + assert(s[1] == 'x'); + assert(s[2] == 'c'); + assert(s[3] == 'd'); + + assert(std::memset(s + 2, 0x123, 1) == s + 2); + assert(s[2] == static_cast(0x123)); + assert(s[3] == 'd'); +} + +void test_memset_embedded_null() { + unsigned char s[] = {'a', 'b', 'c', 'd'}; + + assert(std::memset(s + 1, '\0', 2) == s + 1); + assert(s[0] == 'a'); + assert(s[1] == '\0'); + assert(s[2] == '\0'); + assert(s[3] == 'd'); +} + +void test_memcpy() { + unsigned char src[] = {'a', 'b', 'c', 'd'}; + unsigned char dst[] = {'w', 'x', 'y', 'z'}; + + assert(std::memcpy(dst, src, 3) == dst); + assert(dst[0] == 'a'); + assert(dst[1] == 'b'); + assert(dst[2] == 'c'); + assert(dst[3] == 'z'); + assert(src[0] == 'a'); + assert(src[3] == 'd'); + + assert(std::memcpy(dst + 1, src + 2, 0) == dst + 1); + assert(dst[0] == 'a'); + assert(dst[1] == 'b'); +} + +void test_memcpy_embedded_null() { + unsigned char src[] = {'a', '\0', 'b', '\0'}; + unsigned char dst[] = {'w', 'x', 'y', 'z'}; + + assert(std::memcpy(dst, src, 4) == dst); + assert(dst[0] == 'a'); + assert(dst[1] == '\0'); + assert(dst[2] == 'b'); + assert(dst[3] == '\0'); +} + +void test_memmove() { + unsigned char src[] = {'a', 'b', 'c', 'd'}; + unsigned char dst[] = {'w', 'x', 'y', 'z'}; + + assert(std::memmove(dst, src, 4) == dst); + assert(dst[0] == 'a'); + assert(dst[1] == 'b'); + assert(dst[2] == 'c'); + assert(dst[3] == 'd'); + + assert(std::memmove(dst + 1, src + 1, 0) == dst + 1); + assert(dst[1] == 'b'); +} + +void test_memmove_overlap() { + char forward[] = {'a', 'b', 'c', 'd', 'e', 'f', '\0'}; + char backward[] = {'a', 'b', 'c', 'd', 'e', 'f', '\0'}; + + assert(std::memmove(forward + 2, forward, 4) == forward + 2); + assert(forward[0] == 'a'); + assert(forward[1] == 'b'); + assert(forward[2] == 'a'); + assert(forward[3] == 'b'); + assert(forward[4] == 'c'); + assert(forward[5] == 'd'); + assert(forward[6] == '\0'); + + assert(std::memmove(backward, backward + 2, 4) == backward); + assert(backward[0] == 'c'); + assert(backward[1] == 'd'); + assert(backward[2] == 'e'); + assert(backward[3] == 'f'); + assert(backward[4] == 'e'); + assert(backward[5] == 'f'); + assert(backward[6] == '\0'); +} + +void test_memmove_embedded_null() { + char s[] = {'a', '\0', 'b', 'c', '\0'}; + + assert(std::memmove(s + 1, s, 4) == s + 1); + assert(s[0] == 'a'); + assert(s[1] == 'a'); + assert(s[2] == '\0'); + assert(s[3] == 'b'); + assert(s[4] == 'c'); +} + +void test_cstring_slice1() { + test_strlen(); + test_strcmp(); + test_strncmp(); +} + +void test_cstring_slice4() { + test_memchr(); + test_memcmp(); + test_memset(); + test_memcpy(); + test_memmove(); +} diff --git a/rocq-brick-libstdcpp/test/dune.inc b/rocq-brick-libstdcpp/test/dune.inc index 916b195..8401364 100644 --- a/rocq-brick-libstdcpp/test/dune.inc +++ b/rocq-brick-libstdcpp/test/dune.inc @@ -17,6 +17,15 @@ (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 cstring + (rule + (targets test_cpp.v.stderr test_cpp.v) + (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 --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) From ec100576e28ad97e463fd26bdc6622565eb956f6 Mon Sep 17 00:00:00 2001 From: Lennart Beringer Date: Wed, 6 May 2026 06:09:00 -0400 Subject: [PATCH 2/5] Ported litmus test proofs to new docker image by replacing replicateN by replicateZ in helper lemmas/hints --- rocq-brick-libstdcpp/test/cstring/proof.v | 30 ++++++++++++++++------- 1 file changed, 21 insertions(+), 9 deletions(-) diff --git a/rocq-brick-libstdcpp/test/cstring/proof.v b/rocq-brick-libstdcpp/test/cstring/proof.v index f0a685e..707a1ae 100644 --- a/rocq-brick-libstdcpp/test/cstring/proof.v +++ b/rocq-brick-libstdcpp/test/cstring/proof.v @@ -321,21 +321,32 @@ Section with_cpp. apply heap_pred._at_cancel. apply primR_anyR. Qed. + + Lemma replicateZ_lengthZ_eq_replicateN_lengthN {A : Type} (xs : list A) (x : unit) : + replicateZ (lengthZ xs) x = replicateN (lengthN xs) x. + Proof. + by rewrite /replicateZ N2Z.id. + Qed. + Lemma arrayR_charR_arrayR_anyR (p : ptr) q xs : p |-> arrayR (Tchar_ char_type.Cchar) (fun c : N => charR q c) xs ⊢ p |-> arrayR (Tchar_ char_type.Cchar) (fun _ : unit => anyR (Tchar_ char_type.Cchar) q) - (replicateN (lengthN xs) ()). + (replicateZ (lengthZ xs) ()). Proof. revert p. induction xs as [|x xs IH]. all: intros p. - - rewrite /lengthN /= !arrayR_nil. reflexivity. + - rewrite /replicateZ N2Z.id /= !arrayR_nil. reflexivity. - rewrite arrayR_cons !_at_sep _at_offsetR. iIntros "(Hty & Hx & Hxs)". - replace (lengthN (x :: xs)) with (N.succ (lengthN xs)) by - (rewrite /lengthN Nat2N.inj_succ; reflexivity). - rewrite replicateN_S. + replace (replicateZ (lengthZ (x :: xs)) ()) with + (() :: replicateZ (lengthZ xs) ()). + 2:{ + rewrite !replicateZ_lengthZ_eq_replicateN_lengthN. + rewrite /lengthN Nat2N.inj_succ replicateN_S. + reflexivity. + } rewrite arrayR_cons !_at_sep _at_offsetR. iFrame "Hty". iSplitL "Hx". @@ -348,7 +359,7 @@ Section with_cpp. (fun c : N => charR q c) xs ⊢ p |-> arrayLR (Tchar_ char_type.Cchar) 0 (lengthZ xs) (fun _ : unit => anyR (Tchar_ char_type.Cchar) q) - (replicateN (lengthN xs) ()). + (replicateZ (lengthZ xs) ()). Proof. rewrite arrayLR.unlock _at_sep. iIntros "[_ Harr]". @@ -357,7 +368,8 @@ Section with_cpp. rewrite /arrayLR. iSplit. - iPureIntro. - unfold lengthZ, lengthN, replicateN. + rewrite replicateZ_lengthZ_eq_replicateN_lengthN. + unfold lengthN, replicateN. rewrite length_replicate. rewrite Nat2N.id. lia. @@ -373,7 +385,7 @@ Section with_cpp. \consuming p |-> cstring.R q s \consuming p |-> arrayLR "char" mid k (λ v : N, charR q v) tail \proving p |-> arrayLR "char" 0 k - (λ _ : unit, anyR "char" q) (replicateN (Z.to_N k) ()) + (λ _ : unit, anyR "char" q) (replicateZ k ()) \end@{mpred}. Next Obligation. intros p q mid k tail s Hmid Htailk. @@ -394,7 +406,7 @@ Section with_cpp. iSplitL "Hs". + iFrame. iPureIntro. exact Hwf. + iFrame "Htail". } - rewrite Hk N2Z.id. + rewrite Hk. iPoseProof (arrayLR_charR_arrayLR_anyR _ q (cstring.to_zstring s ++ tail) with "Harr") as "Harr". iExact "Harr". From 88cf8af5ac0f7f245ec40bd9ea137b5d861c7501 Mon Sep 17 00:00:00 2001 From: Lennart Beringer Date: Wed, 6 May 2026 08:22:03 -0400 Subject: [PATCH 3/5] Tweaked the search_result and byte_search_result notations and repaired proofs; some new normalize_ptr proofs steps should be eliminated later --- rocq-brick-libstdcpp/proof/cstring/spec.v | 15 +++++++++--- rocq-brick-libstdcpp/test/cstring/proof.v | 29 +++++++++++++++++++---- 2 files changed, 37 insertions(+), 7 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/cstring/spec.v b/rocq-brick-libstdcpp/proof/cstring/spec.v index 3a4eb5c..d92193d 100644 --- a/rocq-brick-libstdcpp/proof/cstring/spec.v +++ b/rocq-brick-libstdcpp/proof/cstring/spec.v @@ -13,7 +13,7 @@ Require Import skylabs.brick.libstdcpp.cstring.inc_cstring_cpp. #[local] Open Scope Z_scope. -Notation search_result p found := +(*Notation search_result p found := (match found with | Some 0 => Vptr p | Some off => Vptr (p .[ Tchar ! off ]) @@ -25,10 +25,19 @@ Notation byte_search_result byte_ty p found := | Some 0 => Vptr p | Some off => Vptr (p .[ byte_ty ! off ]) | None => Vptr nullptr - end (only parsing). + end (only parsing).*) + +Notation byte_search_result := (fun byte_ty p found => +Vptr (match found with + | Some off => (p .[ byte_ty ! off ]) + | None => nullptr + end)) (only parsing). + +Notation search_result := (fun p found => + (byte_search_result Tchar p found)) (only parsing). Section with_cpp. - Context `{Σ : cpp_logic, module ⊧ σ}. +Context `{Σ : cpp_logic, module ⊧ σ}. cpp.spec "strlen" with (\arg{s_p} "__s" (Vptr s_p) diff --git a/rocq-brick-libstdcpp/test/cstring/proof.v b/rocq-brick-libstdcpp/test/cstring/proof.v index 707a1ae..74b4729 100644 --- a/rocq-brick-libstdcpp/test/cstring/proof.v +++ b/rocq-brick-libstdcpp/test/cstring/proof.v @@ -413,6 +413,13 @@ Section with_cpp. Qed. #[local] Hint Resolve arrayLR_close_cstring_C : sl_opacity. + #[local] Lemma char_ptr_sub_0 (p : ptr) : + p.[ "char" ! 0 ] = p. + Proof. + assert (Hsz : is_Some (size_of σ "char")) by (vm_compute; eauto). + exact (offset_ptr_sub_0 p "char" Hsz). + Qed. + cpp.spec "test_strlen_array_buffer()" from module default. Lemma test_strlen_array_buffer_ok : verify[module] "test_strlen_array_buffer()". @@ -438,16 +445,24 @@ Section with_cpp. Lemma test_strchr_ok : verify[module] "test_strchr()". Proof. verify_spec; go. + normalize_ptrs. Arith.arith_simpl; go. - Arith.arith_simpl; go. + normalize_ptrs. + Arith.arith_simpl. + - contradiction. + - rewrite char_ptr_sub_0 in H. contradiction. Qed. cpp.spec "test_strrchr()" from module default. Lemma test_strrchr_ok : verify[module] "test_strrchr()". Proof. verify_spec; go. + normalize_ptrs. Arith.arith_simpl; go. - Arith.arith_simpl; go. + normalize_ptrs. + Arith.arith_simpl. + - contradiction. + - rewrite char_ptr_sub_0 in H. contradiction. Qed. cpp.spec "test_strspn()" from module default. @@ -462,15 +477,21 @@ Section with_cpp. Lemma test_strpbrk_ok : verify[module] "test_strpbrk()". Proof. verify_spec; go. - Arith.arith_simpl; go. + normalize_ptrs. + Arith.arith_simpl. + contradiction. Qed. cpp.spec "test_strstr()" from module default. Lemma test_strstr_ok : verify[module] "test_strstr()". Proof. verify_spec; go. + normalize_ptrs. Arith.arith_simpl; go. - Arith.arith_simpl; go. + normalize_ptrs. + Arith.arith_simpl. + - contradiction. + - rewrite char_ptr_sub_0 in H. contradiction. Qed. cpp.spec "test_cstring_slice1()" from module default. From d68e5ffba67e66ed79f4bcf16c9a5e704c1186df Mon Sep 17 00:00:00 2001 From: Lennart Beringer Date: Wed, 6 May 2026 08:36:48 -0400 Subject: [PATCH 4/5] Replaced option_map .. with monadic operator; made two hints #[local]; removed commented-out code --- rocq-brick-libstdcpp/proof/cstring/spec.v | 14 -------------- 1 file changed, 14 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/cstring/spec.v b/rocq-brick-libstdcpp/proof/cstring/spec.v index d92193d..bd92a3b 100644 --- a/rocq-brick-libstdcpp/proof/cstring/spec.v +++ b/rocq-brick-libstdcpp/proof/cstring/spec.v @@ -13,20 +13,6 @@ Require Import skylabs.brick.libstdcpp.cstring.inc_cstring_cpp. #[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).*) - Notation byte_search_result := (fun byte_ty p found => Vptr (match found with | Some off => (p .[ byte_ty ! off ]) From 34eee1d412f6b405915ff0df10a786600f9f85aa Mon Sep 17 00:00:00 2001 From: Lennart Beringer Date: Wed, 6 May 2026 08:53:23 -0400 Subject: [PATCH 5/5] Replaced option_map .. with monadic operator; made two hints #[local]; removed commented-out code; activated weak specs of memchr --- rocq-brick-libstdcpp/proof/cstring/model.v | 12 ++++++++---- rocq-brick-libstdcpp/proof/cstring/spec.v | 7 +++---- rocq-brick-libstdcpp/test/cstring/proof.v | 4 ++-- 3 files changed, 13 insertions(+), 10 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/cstring/model.v b/rocq-brick-libstdcpp/proof/cstring/model.v index 1537350..5144727 100644 --- a/rocq-brick-libstdcpp/proof/cstring/model.v +++ b/rocq-brick-libstdcpp/proof/cstring/model.v @@ -49,7 +49,8 @@ Fixpoint strchr (s : bs) (c : Z) : option Z := 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) + (*else option_map (fun off => (1 + off)%Z) (strchr rest c)*) + else Z.succ <$> (strchr rest c) end. Fixpoint strrchr (s : bs) (c : Z) : option Z := @@ -90,7 +91,8 @@ Fixpoint strpbrk (s accept : bs) : option Z := | 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) + (*else option_map (fun off => (1 + off)%Z) (strpbrk rest accept)*) + else Z.succ <$> (strpbrk rest accept) end. Fixpoint prefix (needle haystack : bs) : bool := @@ -112,7 +114,8 @@ Fixpoint strstr (haystack needle : bs) : option Z := | BS.EmptyString => None | BS.String _ rest => if prefix needle haystack then Some 0 - else option_map (fun off => (1 + off)%Z) (strstr rest needle) + (*else option_map (fun off => (1 + off)%Z) (strstr rest needle)*) + else Z.succ <$> (strstr rest needle) end end. @@ -121,7 +124,8 @@ Fixpoint memchr (bytes : list Z) (c : Z) : option Z := | 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) + (*else option_map (fun off => (1 + off)%Z) (memchr rest c)*) + else Z.succ <$> (memchr rest c) end. Fixpoint memcmp (bytes1 bytes2 : list Z) : Z := diff --git a/rocq-brick-libstdcpp/proof/cstring/spec.v b/rocq-brick-libstdcpp/proof/cstring/spec.v index bd92a3b..2072476 100644 --- a/rocq-brick-libstdcpp/proof/cstring/spec.v +++ b/rocq-brick-libstdcpp/proof/cstring/spec.v @@ -118,10 +118,7 @@ Context `{Σ : cpp_logic, module ⊧ σ}. \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. *) +(* Strong but unsound before C++17, and awkward cpp.spec "memchr(void*, int, unsigned long)" as memchr_mut_spec with (\arg{s_p} "__s" (Vptr s_p) \arg{c} "__c" (Vint c) @@ -149,7 +146,9 @@ Context `{Σ : cpp_logic, module ⊧ σ}. (*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). +*) +(* sound, but weak in C++17*) 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) diff --git a/rocq-brick-libstdcpp/test/cstring/proof.v b/rocq-brick-libstdcpp/test/cstring/proof.v index 74b4729..be866a5 100644 --- a/rocq-brick-libstdcpp/test/cstring/proof.v +++ b/rocq-brick-libstdcpp/test/cstring/proof.v @@ -278,7 +278,7 @@ Section with_cpp. rewrite _at_sub_0; [|done]. rewrite /cstring.R /zstring.R; iFrame; done. Qed. - Hint Resolve arrayLR_cstring : sl_opacity. + #[local] Hint Resolve arrayLR_cstring : sl_opacity. #[local] Lemma cstring_arrayLR q bytes m tail (p : ptr) s : bytes = cstring.to_zstring s ++ tail -> @@ -294,7 +294,7 @@ Section with_cpp. rewrite arrayLR.unlock; arith_simpl; work. rewrite _at_sub_0; [trivial|done]. Qed. - Hint Resolve cstring_arrayLR : sl_opacity. + #[local] Hint Resolve cstring_arrayLR : sl_opacity. #[local, program] Definition arrayLR_open_cstring_C (p : ptr) q k bytes s tail