From 9fff975696fa1de35a08506f877360548fdf2878 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Thu, 12 Feb 2026 23:56:36 -0500 Subject: [PATCH 01/13] A sketch of a refinement-based setup. --- rocq-brick-libstdcpp/proof/iostream/spec.v | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/iostream/spec.v b/rocq-brick-libstdcpp/proof/iostream/spec.v index 3851fd6..ee5f29e 100644 --- a/rocq-brick-libstdcpp/proof/iostream/spec.v +++ b/rocq-brick-libstdcpp/proof/iostream/spec.v @@ -14,14 +14,25 @@ Require Import skylabs.brick.libstdcpp.iostream.inc_iostream_cpp. Section with_cpp. Context `{Σ : cpp_logic, σ : genv}. + Parameter ostreamR : cQp.t -> gname -> Rep. + + (** This is effectively an <> that yields the characters and then continues *) + Parameter ostream_yield : gname -> string -> mpred -> mpred. + + #[global] Instance: LearnEqF1 ostreamR := ltac:(solve_learnable). + (* #[global] Instance: LearnEqF1 ostream_contentR := ltac:(solve_learnable). *) + + Parameter istreamT : Type. + Parameter istreamR : cQp.t -> istreamT -> Rep. + #[global] Instance: LearnEqF1 istreamR := ltac:(solve_learnable). + cpp.spec "std::operator<<>(std::basic_ostream>&, 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 + \prepost{γ} osP |-> ostreamR 1$m γ \arg{strP} "" (Vptr strP) \prepost{q__s strM} strP |-> cstring.R q__s strM - \post[Vptr osP] - osP |-> ostream_contentR 1$m (str ++ strM)). + \pre{Q} ostream_yield γ _ Q + \post[Vptr osP] Q) Parameter Z_to_string : Z -> cstring.t. #[global] Declare Instance Z_to_string_inj : Inj eq eq Z_to_string. From 159dce6be3ff41ccad49b83943fe1b9cadda1c0d Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Wed, 4 Mar 2026 23:17:00 -0500 Subject: [PATCH 02/13] Fleshing out the example. --- rocq-brick-libstdcpp/proof/iostream/spec.v | 97 +++++++++++++++------- 1 file changed, 69 insertions(+), 28 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/iostream/spec.v b/rocq-brick-libstdcpp/proof/iostream/spec.v index ee5f29e..d51dbfb 100644 --- a/rocq-brick-libstdcpp/proof/iostream/spec.v +++ b/rocq-brick-libstdcpp/proof/iostream/spec.v @@ -11,58 +11,82 @@ Require Export skylabs.brick.libstdcpp.iostream.pred. Require Import skylabs.brick.libstdcpp.iostream.inc_iostream_cpp. +(* +Variant io_align : Set := left | right | internal. +Variant io_base : Set := dec | hex | oct. +Variant io_float : Set := fixed | scientific | hexfloat | defaultfloat. + +Record ioflags : Set := +{ boolalpha : bool +; showbase : bool +; showpoint : bool +; showpos : bool +; uppercase : bool +; align : io_align +; float : io_float +}. +*) + +(* TODO: it probably makes sense to separate istream, ostream, and iomanip *) + Section with_cpp. Context `{Σ : cpp_logic, σ : genv}. + Parameter gname : Set. + + (** TODO: Add support for *) Parameter ostreamR : cQp.t -> gname -> Rep. + Parameter ostream_rest : gname -> Qp -> bs -> mpred. (** This is effectively an <> that yields the characters and then continues *) - Parameter ostream_yield : gname -> string -> mpred -> mpred. + Definition ostream_yield (γ : gname) (s : bs) (K : mpred) : mpred := + AC << ∀ rest, ostream_rest γ 1 (s ++ rest) >> @ ⊤ , ⊤ + << ostream_rest γ 1 rest , COMM emp >>. #[global] Instance: LearnEqF1 ostreamR := ltac:(solve_learnable). (* #[global] Instance: LearnEqF1 ostream_contentR := ltac:(solve_learnable). *) + (* Parameter istreamT : Type. Parameter istreamR : cQp.t -> istreamT -> Rep. #[global] Instance: LearnEqF1 istreamR := ltac:(solve_learnable). + *) cpp.spec "std::operator<<>(std::basic_ostream>&, const char*)" from source as ostream_insert_spec with ( \arg{osP} "" (Vptr osP) \prepost{γ} osP |-> ostreamR 1$m γ \arg{strP} "" (Vptr strP) \prepost{q__s strM} strP |-> cstring.R q__s strM - \pre{Q} ostream_yield γ _ Q - \post[Vptr osP] Q) + \pre{Q} ostream_yield γ strM Q + \post[Vptr osP] Q). - Parameter Z_to_string : Z -> cstring.t. - #[global] Declare Instance Z_to_string_inj : Inj eq eq Z_to_string. + Parameter format_int : Z -> bs. + #[global] Declare Instance format_int_inj : Inj eq eq format_int. (** TODO: find an implementation!*) cpp.spec "std::basic_ostream>::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) + \prepost{γ} this |-> ostreamR 1$m γ + \pre{Q} ostream_yield γ (format_int n) Q + \post[Vptr this] Q ). cpp.spec "std::basic_ostream>::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) + \prepost{γ} this |-> ostreamR 1$m γ + \pre{Q} ostream_yield γ (format_int n) Q + \post[Vptr this] Q ). - Definition iostream_manip_spec state_f contents_f : WpSpec_cpp_val := ( + Definition iostream_manip_spec 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)). + \pre{γ} osP |-> ostreamR 1$m γ + \post* osP |-> ostreamR 1$m γ + \pre{Q} ostream_yield γ contents_f Q + \post[Vptr osP] Q). Definition ostream_cpp_type : type := "std::basic_ostream>&". @@ -70,26 +94,27 @@ Section with_cpp. tFunction ostream_cpp_type [ostream_cpp_type]. cpp.spec "std::endl>(std::basic_ostream>&)" from source as endl_spec with ( - \exact Reduce iostream_manip_spec (fun osM => osM) (fun str => str ++ "\n")%bs + \exact Reduce iostream_manip_spec "\n"%bs ). (* This is the overload taking the endl manipulator. *) (* https://eel.is/c++draft/output.streams#ostream.inserters *) +<<<<<<< HEAD:rocq-brick-libstdcpp/proof/iostream/spec.v cpp.spec "std::basic_ostream>::operator<<(std::basic_ostream>&(*)(std::basic_ostream>&))" from source as ostream_insert_string_spec with ( +======= + + cpp.spec "std::basic_ostream>::operator<<(std::basic_ostream>&(*)(std::basic_ostream>&))" from source as ostream_insert_string_spec with ( +>>>>>>> 7ed54b8 (Fleshing out the example.):rocq-brick-libstdcpp/test/geeks_for_geeks_examples/spec.v \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) + \pre{spec} os_f |-> unmaterialized_specR iostream_manip_kind spec + (* ^^ this would be *slightly* more general if it took a materialized specification *) + \pre{Q} (spec [Vref this] (fun v => [| v = Vvoid |] ** Q)) + \post[Vptr this] Q ). +<<<<<<< HEAD:rocq-brick-libstdcpp/proof/iostream/spec.v (** NOTE: this specification is weak because it does not connect to the actual stream "contents". *) cpp.spec "std::basic_istream>::operator>>(int&)" @@ -104,3 +129,19 @@ Section with_cpp. ). End with_cpp. +======= + (* + 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. +*) +>>>>>>> 7ed54b8 (Fleshing out the example.):rocq-brick-libstdcpp/test/geeks_for_geeks_examples/spec.v From e35dff2296572ccd5c4fc9c381008d554c53d0d7 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Wed, 8 Apr 2026 15:53:16 -0400 Subject: [PATCH 03/13] Re-organize the refinement setup Introduce a generic [SepHandler] that embeds arbitrary actions into predicate transformers. --- rocq-brick-libstdcpp/proof/iostream/spec.v | 237 +++++++++++---------- 1 file changed, 126 insertions(+), 111 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/iostream/spec.v b/rocq-brick-libstdcpp/proof/iostream/spec.v index d51dbfb..a571e17 100644 --- a/rocq-brick-libstdcpp/proof/iostream/spec.v +++ b/rocq-brick-libstdcpp/proof/iostream/spec.v @@ -29,119 +29,134 @@ Record ioflags : Set := (* TODO: it probably makes sense to separate istream, ostream, and iomanip *) -Section with_cpp. - Context `{Σ : cpp_logic, σ : genv}. +(** A handler for events as a predicate transformer. + Generally, this will be an that proves that is a valid next event. + *) +Class SepHandler (PROP : bi) (evt : Set) : Type := +{ do : evt -> PROP -> PROP + (** This is effectively an <> that performs the event and then continues *) +}. + +(** Events that send output. + + For most buffered streams, writes go to the buffer and are only guaranteed + to be sent to the consumer on a [Flush]. + *) +Variant output_event : Set := +| Write (_ : Byte.byte). + +Variant input_event : Set := +| Read (_ : Byte.byte). + +(** The behavior of an [ostream] is described by a handler of an [output_event] *) +Notation Ostream := (SepHandler mpred output_event). +Notation Istream := (SepHandler mpred input_event). + +Module ostream. Parameter gname : Set. (** TODO: Add support for *) - Parameter ostreamR : cQp.t -> gname -> Rep. - Parameter ostream_rest : gname -> Qp -> bs -> mpred. - - (** This is effectively an <> that yields the characters and then continues *) - Definition ostream_yield (γ : gname) (s : bs) (K : mpred) : mpred := - AC << ∀ rest, ostream_rest γ 1 (s ++ rest) >> @ ⊤ , ⊤ - << ostream_rest γ 1 rest , COMM emp >>. - - #[global] Instance: LearnEqF1 ostreamR := ltac:(solve_learnable). - (* #[global] Instance: LearnEqF1 ostream_contentR := ltac:(solve_learnable). *) - - (* - Parameter istreamT : Type. - Parameter istreamR : cQp.t -> istreamT -> Rep. - #[global] Instance: LearnEqF1 istreamR := ltac:(solve_learnable). - *) - - cpp.spec "std::operator<<>(std::basic_ostream>&, const char*)" from source as ostream_insert_spec with ( - \arg{osP} "" (Vptr osP) - \prepost{γ} osP |-> ostreamR 1$m γ - \arg{strP} "" (Vptr strP) - \prepost{q__s strM} strP |-> cstring.R q__s strM - \pre{Q} ostream_yield γ strM Q - \post[Vptr osP] Q). - - Parameter format_int : Z -> bs. - #[global] Declare Instance format_int_inj : Inj eq eq format_int. - (** TODO: find an implementation!*) - - cpp.spec "std::basic_ostream>::operator<<(int)" from source as ostream_print_int_spec with ( - \this this - \arg{n} "" (Vint n) - \prepost{γ} this |-> ostreamR 1$m γ - \pre{Q} ostream_yield γ (format_int n) Q - \post[Vptr this] Q - ). - - cpp.spec "std::basic_ostream>::operator<<(unsigned long)" from source as ostream_print_ulong_spec with ( - \this this - \arg{n} "" (Vint n) - \prepost{γ} this |-> ostreamR 1$m γ - \pre{Q} ostream_yield γ (format_int n) Q - \post[Vptr this] Q - ). - - Definition iostream_manip_spec contents_f : WpSpec_cpp_val := ( - \arg{osP : ptr} "" (Vptr osP) - (* XXX: manipulators can modify [osM]! *) - \pre{γ} osP |-> ostreamR 1$m γ - \post* osP |-> ostreamR 1$m γ - \pre{Q} ostream_yield γ contents_f Q - \post[Vptr osP] Q). - - Definition ostream_cpp_type : type := - "std::basic_ostream>&". - Definition iostream_manip_kind : okind := - tFunction ostream_cpp_type [ostream_cpp_type]. - - cpp.spec "std::endl>(std::basic_ostream>&)" from source as endl_spec with ( - \exact Reduce iostream_manip_spec "\n"%bs - ). - - (* This is the overload taking the endl manipulator. *) - (* https://eel.is/c++draft/output.streams#ostream.inserters *) -<<<<<<< HEAD:rocq-brick-libstdcpp/proof/iostream/spec.v - cpp.spec "std::basic_ostream>::operator<<(std::basic_ostream>&(*)(std::basic_ostream>&))" - from source as ostream_insert_string_spec with ( -======= - - cpp.spec "std::basic_ostream>::operator<<(std::basic_ostream>&(*)(std::basic_ostream>&))" from source as ostream_insert_string_spec with ( ->>>>>>> 7ed54b8 (Fleshing out the example.):rocq-brick-libstdcpp/test/geeks_for_geeks_examples/spec.v - \this this - \arg{os_f} "" (Vptr os_f) - \pre{spec} os_f |-> unmaterialized_specR iostream_manip_kind spec - (* ^^ this would be *slightly* more general if it took a materialized specification *) - \pre{Q} (spec [Vref this] (fun v => [| v = Vvoid |] ** Q)) - \post[Vptr this] Q - ). - -<<<<<<< HEAD:rocq-brick-libstdcpp/proof/iostream/spec.v - (** NOTE: this specification is weak because it does not connect to the - actual stream "contents". *) - cpp.spec "std::basic_istream>::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. -======= - (* - 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. + Parameter R : forall `{Σ : cpp_logic} {σ : genv}, Ostream -> gname -> cQp.t -> Rep. + + Section with_cpp. + Context `{Σ : cpp_logic, σ : genv}. + + #[global] Instance: Cbn (Learn (learn_eq ==> learn_eq ==> any ==> learn_hints.fin) R). + Proof. solve_learnable. Qed. + + Fixpoint bs_dos {_ : Ostream} (bs : bs) (K : mpred) : mpred := + match bs with + | BS.EmptyString => K + | BS.String b bs => do (Write b) $ bs_dos bs K + end. + + cpp.spec "std::operator<<>(std::basic_ostream>&, const char*)" + from source as ostream_insert_spec with ( + \arg{osP} "" (Vptr osP) + \prepost{OS γ} osP |-> R OS γ 1$m + \arg{strP} "" (Vptr strP) + \prepost{q__s strM} strP |-> cstring.R q__s strM + \pre{Q} bs_dos strM Q + \post[Vptr osP] Q). + + Parameter format_int : Z -> bs. + #[global] Declare Instance format_int_inj : Inj eq eq format_int. + (** TODO: find an implementation!*) + + cpp.spec "std::basic_ostream>::operator<<(int)" + from source as ostream_print_int_spec with ( + \this this + \arg{n} "" (Vint n) + \prepost{OS γ} this |-> R OS γ 1$m + \pre{Q} bs_dos (format_int n) Q + \post[Vptr this] Q + ). + + cpp.spec "std::basic_ostream>::operator<<(unsigned long)" + from source as ostream_print_ulong_spec with ( + \this this + \arg{n} "" (Vint n) + \prepost{OS γ} this |-> R OS γ 1$m + \pre{Q} bs_dos (format_int n) Q + \post[Vptr this] Q + ). + + Definition iostream_manip_spec contents_f : WpSpec_cpp_val := ( + \arg{osP : ptr} "" (Vptr osP) + (* XXX: manipulators can cause output! *) + \prepost{OS γ} osP |-> R OS γ 1$m + \pre{Q} bs_dos contents_f Q + \post[Vptr osP] Q). + + Definition ostream_cpp_type : type := + "std::basic_ostream>&". + Definition iostream_manip_kind : okind := + tFunction ostream_cpp_type [ostream_cpp_type]. + + cpp.spec "std::endl>(std::basic_ostream>&)" + from source as endl_spec with ( + \exact Reduce iostream_manip_spec "\n"%bs + ). + + (* This is the overload taking the endl manipulator. *) + (* https://eel.is/c++draft/output.streams#ostream.inserters *) + cpp.spec "std::basic_ostream>::operator<<(std::basic_ostream>&(*)(std::basic_ostream>&))" + from source as ostream_insert_string_spec with ( + \this this + \arg{os_f} "" (Vptr os_f) + \pre{spec} os_f |-> unmaterialized_specR iostream_manip_kind spec + (* ^^ this would be *slightly* more general if it took a materialized specification *) + \pre{Q} (spec [Vref this] (fun v => [| v = Vvoid |] ** Q)) + \post[Vptr this] Q + ). + + (** NOTE: this specification is weak because it does not connect to the + actual stream "contents". *) + cpp.spec "std::basic_istream>::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. +End ostream. + +Module istream. + Parameter gname : Set. + Parameter R : forall `{Σ : cpp_logic} {σ : genv}, Istream -> gname -> cQp.t -> Rep. -(* -#[export] Hint Resolve ostream_contentR_aggressiveC : br_hints. -*) ->>>>>>> 7ed54b8 (Fleshing out the example.):rocq-brick-libstdcpp/test/geeks_for_geeks_examples/spec.v + Section with_cpp. + Context `{Σ : cpp_logic, σ : genv}. + + #[global] Instance: Cbn (Learn (learn_eq ==> learn_eq ==> any ==> learn_hints.fin) R). + Proof. solve_learnable. Qed. + + End with_cpp. + +End istream. From 88d17a5e1d4e84fa99af2a8adbde516f0205ff51 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Mon, 13 Apr 2026 14:58:34 -0400 Subject: [PATCH 04/13] WIP --- rocq-brick-libstdcpp/proof/iostream/pred.v | 82 +++++++++------ rocq-brick-libstdcpp/proof/iostream/spec.v | 49 +++------ .../geeks_for_geeks_examples/N1_hello_world.v | 99 ++++++++++++++++++- .../test/geeks_for_geeks_examples/N5_swap.v | 10 +- 4 files changed, 173 insertions(+), 67 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/iostream/pred.v b/rocq-brick-libstdcpp/proof/iostream/pred.v index 3f86ebf..9fbcaea 100644 --- a/rocq-brick-libstdcpp/proof/iostream/pred.v +++ b/rocq-brick-libstdcpp/proof/iostream/pred.v @@ -18,31 +18,57 @@ Require Import skylabs.brick.libstdcpp.iostream.inc_iostream_cpp. (* We only have `Bind Scope bs_scope with t.` inside `Module cstring.` *) (** TODO upstream END *) -Section with_cpp. - Context `{Σ : cpp_logic, σ : genv}. - - Parameter ostreamT : Type. - Parameter ostreamR : cQp.t -> ostreamT -> Rep. - Parameter ostream_contentR : cQp.t -> cstring.t -> Rep. - (* TODO: type_ptr *) - #[only(cfracsplittable)] derive ostreamR. - #[only(cfracsplittable)] derive ostream_contentR. - - #[global] Instance: LearnEqF1 ostreamR := ltac:(solve_learnable). - #[global] Instance: LearnEqF1 ostream_contentR := ltac:(solve_learnable). - - Parameter istreamT : Type. - Parameter istreamR : cQp.t -> istreamT -> Rep. - #[only(cfracsplittable)] derive istreamR. - #[global] Instance: LearnEqF1 istreamR := ltac:(solve_learnable). - - Lemma ostream_contentR_aggressive (os_p : ptr) q str str': - os_p |-> ostream_contentR q str ⊢ - [| str = str' |] -∗ - os_p |-> ostream_contentR q str'. - Proof. work. Qed. - Definition ostream_contentR_aggressiveC := [CANCEL] ostream_contentR_aggressive. - -End with_cpp. - -#[export] Hint Resolve ostream_contentR_aggressiveC : br_hints. +(** A handler for events as a predicate transformer. + + Generally, this will be an that proves that is a valid next event. + *) +Class SepHandler (PROP : bi) (evt : Set) : Type := +{ do : evt -> PROP -> PROP + (** This is effectively an <> that performs the event and then continues *) +}. + +(** Events that send output. + + For most buffered streams, writes go to the buffer and are only guaranteed + to be sent to the consumer on a [Flush]. + *) +Variant output_event : Set := + | Write (_ : Byte.byte). + +Variant input_event : Set := + | Read (_ : Byte.byte). + +(** The behavior of an [ostream] is described by a handler of an [output_event] *) +Notation Ostream := (SepHandler mpred output_event). +Notation Istream := (SepHandler mpred input_event). + +Module ostream. + Parameter gname : Set. + + (** TODO: Add support for *) + Parameter R : forall `{Σ : cpp_logic} {σ : genv}, Ostream -> gname -> cQp.t -> Rep. + #[only(cfracsplittable)] derive R. + + Section with_cpp. + Context `{Σ : cpp_logic, σ : genv}. + + #[global] Instance: Cbn (Learn (learn_eq ==> learn_eq ==> any ==> learn_hints.fin) R). + Proof. solve_learnable. Qed. + + End with_cpp. +End ostream. + +Module istream. + Parameter gname : Set. + Parameter R : forall `{Σ : cpp_logic} {σ : genv}, Istream -> gname -> cQp.t -> Rep. + #[only(cfracsplittable)] derive R. + + Section with_cpp. + Context `{Σ : cpp_logic, σ : genv}. + + #[global] Instance: Cbn (Learn (learn_eq ==> learn_eq ==> any ==> learn_hints.fin) R). + Proof. solve_learnable. Qed. + + End with_cpp. + +End istream. diff --git a/rocq-brick-libstdcpp/proof/iostream/spec.v b/rocq-brick-libstdcpp/proof/iostream/spec.v index a571e17..38284a6 100644 --- a/rocq-brick-libstdcpp/proof/iostream/spec.v +++ b/rocq-brick-libstdcpp/proof/iostream/spec.v @@ -29,29 +29,6 @@ Record ioflags : Set := (* TODO: it probably makes sense to separate istream, ostream, and iomanip *) -(** A handler for events as a predicate transformer. - - Generally, this will be an that proves that is a valid next event. - *) -Class SepHandler (PROP : bi) (evt : Set) : Type := -{ do : evt -> PROP -> PROP - (** This is effectively an <> that performs the event and then continues *) -}. - -(** Events that send output. - - For most buffered streams, writes go to the buffer and are only guaranteed - to be sent to the consumer on a [Flush]. - *) -Variant output_event : Set := -| Write (_ : Byte.byte). - -Variant input_event : Set := -| Read (_ : Byte.byte). - -(** The behavior of an [ostream] is described by a handler of an [output_event] *) -Notation Ostream := (SepHandler mpred output_event). -Notation Istream := (SepHandler mpred input_event). Module ostream. Parameter gname : Set. @@ -131,18 +108,6 @@ Module ostream. \post[Vptr this] Q ). - (** NOTE: this specification is weak because it does not connect to the - actual stream "contents". *) - cpp.spec "std::basic_istream>::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. End ostream. @@ -157,6 +122,20 @@ Module istream. #[global] Instance: Cbn (Learn (learn_eq ==> learn_eq ==> any ==> learn_hints.fin) R). Proof. solve_learnable. Qed. + (** NOTE: this specification is weak because it does not connect to the + actual stream "contents". *) + cpp.spec "std::basic_istream>::operator>>(int&)" + from source as istream_take_int_spec with ( + \this this + \pre{IS isM} this |-> istream.R IS isM 1$m + \arg{nP} "" (Vptr nP) + \pre nP |-> anyR "int" 1$m + \post[Vptr this] Exists isM' n, + this |-> istream.R IS isM' 1$m ** + nP |-> intR 1$m n + ). + + End with_cpp. End istream. 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 index 329fc3f..65999ea 100644 --- 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 @@ -1,22 +1,115 @@ Require Import skylabs.auto.cpp.prelude.proof. Require Import skylabs.brick.libstdcpp.iostream.spec. +Require Import skylabs.iris.extra.base_logic.lib.spectra. + + Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.N1_hello_world_cpp. Import linearity. +(* BEGIN UPSTREAM *) +Definition appG {evt : Type} (lts : LTS evt) (Σ : gFunctors) : Type := + inG Σ (auth_setR (lts_state lts)). + +(* END UPSTREAM *) + + + +Inductive only_output : bs -> option output_event -> bs -> Prop := +| output_char {c} {b : bs} : only_output (BS.String c b) (Some $ Write c) b +| skip {bs} : only_output bs None bs. + +Definition the_app : LTS output_event := + {| Sts._state := bs + ; Sts._init_state := fun x => x = "Hello World"%bs + ; Sts._step := only_output |}. + Section with_cpp. Context `{Σ : cpp_logic, σ : genv}. + Context `{SPECTRA : !appG the_app _}. + + #[program] + Instance HelloWorld : App.app := + {| App.evt := output_event + ; App.lts := the_app + ; App.inG := _ + |}. + Next Obligation. + unshelve eapply mpred_prop.mpred_has_usual_own. apply SPECTRA. + Defined. + + #[program] + Definition OS (E : coPset) γ : Ostream := + {| do evt K := + let is_write : propset (App.evt HelloWorld) := PropSet (A:=App.evt HelloWorld) (fun x => x = evt) in + Step.gen_requester HelloWorld E masks.default γ is_write (fun _ => K) + |}. 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 + \prepost{γ osM} _global "std::cout" |-> ostream.R (OS ⊤ γ) osM 1$m + \pre AuthSet.frag γ {[ "Hello World"%bs ]} \post[Vint 0] - _global "std::cout" |-> ostream_contentR 1$m (str ++ "Hello World")). + AuthSet.frag γ {[ ""%bs ]}). + + #[program] + Definition gen_requester_C {BS c cs} (_ : TCUnify BS (BS.String c cs) ):= + \cancelx + \using{γ} AuthSet.frag γ {[ BS ]} + \proving{E K} Step.gen_requester HelloWorld ⊤ E γ {[ x | x = Write c ]} K + \through AuthSet.frag γ {[ cs ]} -∗ K (Write c) + \end. + Next Obligation. + intros. inversion t; subst; clear t. + simpl; intros. + work. + rewrite /Step.gen_requester /Step.gen_requester_learn. + iAcIntro. + rewrite /commit_acc. + simpl. + iExists {[ BS.String c cs ]}. + simpl. + Require Import skylabs.upstream.cpp.misc_hints. + work. + iApply fupd_mask_intro. admit. + iIntros "Hclose". + work. + iSplitR. + iPureIntro. + { split. + eexists; set_solver. + intros. admit. } + iIntros. iMod "Hclose". + iModIntro. + work. + assert (x = Write c) by admit. + iDestruct "Hclose" as "_". + iStopProof. + rewrite AuthSet.frag_proper. reflexivity. + admit. + Admitted. + Hint Resolve gen_requester_C : sl_opacity. + + Instance bs_dos_positive {OS: Ostream} b Q : IsPositive Q (ostream.bs_dos b Q) (ostream.bs_dos b). + Proof. + constructor. done. + constructor. intros. + induction b; simpl. + { iIntros "X"; iApply ("X" $! ()). } + { iIntros "X". admit. } + Admitted. Lemma main_ok : verify[source] "main()". Proof. + Opaque ostream.bs_dos. verify_shift; go. + Set Typeclasses Debug. + Set Typeclasses Debug Verbosity 1. + Hint Extern 0 (IsExistential ?X) => match goal with + | H : IsExistential _ |- _ => exact H + end : typeclass_instances. + work using canonical_Q. + Transparent ostream.bs_dos. banish_string_literals. iModIntro. go. 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 index e82bfcb..ccb57be 100644 --- a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap.v +++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap.v @@ -8,8 +8,16 @@ Import linearity. Section with_cpp. Context `{Σ : cpp_logic, σ : genv}. + Inductive only_output : bs -> output_event -> bs -> Prop := + | output_char c {b : bs} : only_output (BS.String c b) (Write c) b. + Require Import skylabs.iris.extra.base_logic.lib.spectra. + + About AuthSet.frag. + + cpp.spec "main()" from source as main_spec with ( - \prepost{osM} _global "std::cout" |-> ostreamR 1$m osM + \prepost{osM} _global "std::cout" |-> ostream.R 1$m osM + \pre AuthSet.frag γ {[ ]} \pre{str} _global "std::cout" |-> ostream_contentR 1$m str \post[Vint 0] _global "std::cout" |-> ostream_contentR 1$m From 966c93e42dc00391c6877becd9035aa91b2b1eb4 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Wed, 15 Apr 2026 16:56:04 -0400 Subject: [PATCH 05/13] Working on the proofs. --- rocq-brick-libstdcpp/proof/iostream/pred.v | 5 +- rocq-brick-libstdcpp/proof/iostream/spec.v | 2 +- .../geeks_for_geeks_examples/N1_hello_world.v | 166 ++++++++++++------ .../test/geeks_for_geeks_examples/N5_swap.v | 16 +- 4 files changed, 126 insertions(+), 63 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/iostream/pred.v b/rocq-brick-libstdcpp/proof/iostream/pred.v index 9fbcaea..726cddb 100644 --- a/rocq-brick-libstdcpp/proof/iostream/pred.v +++ b/rocq-brick-libstdcpp/proof/iostream/pred.v @@ -8,6 +8,8 @@ different style of specifications. Require Import skylabs.auto.cpp.prelude.proof. Require Export skylabs.cpp.string. +Require Import skylabs.auto.hints.kont. + Require Import skylabs.brick.libstdcpp.iostream.inc_iostream_cpp. (** TODO upstream START *) @@ -23,8 +25,9 @@ Require Import skylabs.brick.libstdcpp.iostream.inc_iostream_cpp. Generally, this will be an that proves that is a valid next event. *) Class SepHandler (PROP : bi) (evt : Set) : Type := -{ do : evt -> PROP -> PROP +{ do : propset evt -> (evt -> PROP) -> PROP (** This is effectively an <> that performs the event and then continues *) +; do_frame : forall evtP, ProperFrame (T:=[tele (_ : evt)]) (do evtP) }. (** Events that send output. diff --git a/rocq-brick-libstdcpp/proof/iostream/spec.v b/rocq-brick-libstdcpp/proof/iostream/spec.v index 38284a6..dfe7452 100644 --- a/rocq-brick-libstdcpp/proof/iostream/spec.v +++ b/rocq-brick-libstdcpp/proof/iostream/spec.v @@ -45,7 +45,7 @@ Module ostream. Fixpoint bs_dos {_ : Ostream} (bs : bs) (K : mpred) : mpred := match bs with | BS.EmptyString => K - | BS.String b bs => do (Write b) $ bs_dos bs K + | BS.String b bs => do {[Write b]} $ fun _ => bs_dos bs K end. cpp.spec "std::operator<<>(std::basic_ostream>&, const char*)" 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 index 65999ea..ab84c57 100644 --- 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 @@ -12,6 +12,46 @@ Import linearity. Definition appG {evt : Type} (lts : LTS evt) (Σ : gFunctors) : Type := inG Σ (auth_setR (lts_state lts)). +Section to_spectra. + Context {PROP : bi}. + Context {HAS_FUPD : BiFUpd PROP} {GHOSTLY : prop_constraints.Ghostly PROP}. + Context `{SPECTRA : @appG evt lts Σ}. + + #[global] Instance requester_frame' T app E γ ps (F : (T -t> PROP) -> [tele (_:App.evt app)] -t> PROP) : + kont.ProperFrame (PROP:=PROP) (T:=tele_snoc T [tele (_:App.evt app)]) + (fun K : tele_snoc T [tele _ : App.evt app] -t> PROP => Forall x : App.evt app, + let xxx :tele_arg [tele _ : App.evt app] := [tele_arg (x : App.evt app)] in + F (tele_bind (fun t : T => tele_app K (tele_arg_snoc t xxx))) x)%I -> + kont.ProperFrame (PROP:=PROP) (T:=T) (fun K => Step.requester app E γ ps (F K)). + Proof. + clear. intros. + constructor; simpl; intros. + rewrite /Step.requester. + iIntros "K". + Admitted. + + #[global] Instance requester_frame app E γ ps : + kont.ProperFrame (PROP:=PROP) (T:=[tele (_:App.evt app)]) (fun K => Step.requester app E γ ps K). + Proof. + clear. intros. + constructor; simpl; intros. + rewrite /Step.requester. + iIntros "K". + Admitted. + + Instance gen_requester_frame {TT:tele} {a b c d e} (F : (TT -t> _) -> _ -> _): + (forall x, kont.ProperFrame (T:=tele_snoc TT (App.evt a)) (fun K : (tele_snoc TT (App.evt a)) -t> _ => F (tele_bind (fun v => tele_app K (tele_arg_snoc v x))) x)) -> + kont.ProperFrame (T:=TT) (fun K => Step.gen_requester a b c d e (F K)). + Proof. Admitted. + + Lemma frag_frag_exact {T : Type} {_ : prop_constraints.HasUsualOwn PROP (auth_setR T)} γ val : + AuthSet.frag γ {[ val ]} ⊣⊢@{PROP} AuthSet.frag_exact γ val. + Proof. reflexivity. Qed. + Definition frag_frag_exact_F := [FWD<-] @frag_frag_exact. + Definition frag_frag_exact_B := [BWD<-] @frag_frag_exact. + +End to_spectra. +#[global] Hint Resolve frag_frag_exact_B frag_frag_exact_F : sl_opacity. (* END UPSTREAM *) @@ -22,13 +62,27 @@ Inductive only_output : bs -> option output_event -> bs -> Prop := Definition the_app : LTS output_event := {| Sts._state := bs - ; Sts._init_state := fun x => x = "Hello World"%bs ; Sts._step := only_output |}. Section with_cpp. Context `{Σ : cpp_logic, σ : genv}. Context `{SPECTRA : !appG the_app _}. + (* TODO: upstream this *) + #[global] + Instance bs_dos_positive {OS: Ostream} b + : kont.ProperFrame (T:=[tele]) (fun K => ostream.bs_dos b K). + Proof. + constructor; intros. + induction b; simpl. + { iIntros "X"; iApply ("X" $! ()). } + { iIntros "X". destruct OS. + iApply (do_frame {[Write b]}).(kont._frame). + iIntros ([?[]]); simpl. + iApply IHb. iAssumption. } + Qed. + + #[program] Instance HelloWorld : App.app := {| App.evt := output_event @@ -42,9 +96,8 @@ Section with_cpp. #[program] Definition OS (E : coPset) γ : Ostream := {| do evt K := - let is_write : propset (App.evt HelloWorld) := PropSet (A:=App.evt HelloWorld) (fun x => x = evt) in - Step.gen_requester HelloWorld E masks.default γ is_write (fun _ => K) - |}. + Step.requester HelloWorld E γ evt K + |}%I. cpp.spec "main()" from source as main_spec with ( \prepost{γ osM} _global "std::cout" |-> ostream.R (OS ⊤ γ) osM 1$m @@ -52,67 +105,76 @@ Section with_cpp. \post[Vint 0] AuthSet.frag γ {[ ""%bs ]}). + Class AnyStep {T E} (step : T -> option E -> T -> Prop) (Pre : propset T) (evt : E) (Post : propset T) : Prop := + { _safe : forall s, s ∈ Pre -> exists s', step s (Some evt) s' + ; _steps_to : forall s', s' ∈ Post -> ∃ s, s ∈ Pre /\ step s (Some evt) s' }. + Hint Mode AnyStep + + + + + - : typeclass_instances. + + Instance only_output_any_step {c cs} : AnyStep only_output {[ BS.String c cs ]} (Write c) {[ cs ]}. + Proof. + constructor; inversion 1; subst. + { eexists; constructor. } + { eexists; repeat constructor. } + Qed. + + #[global] Instance authset_frag_exact_learn : forall γ, Cbn (Learn (learn_eq ==> learn_hints.fin) (fun x => AuthSet.frag γ {[x]})). + Proof. clear. Admitted. + Hint Resolve authset_frag_exact_learn : sl_opacity. + + (* The early commit version + #[program] + Definition requester_ec_C (app : App.app) {s : _} s' evt + (ANY_STEP : AnyStep app.(App.lts).(Sts._step) {[s]} evt s'):= + \cancelx + \using{γ} AuthSet.frag γ {[s]} + \proving{E K} Step.requester app E γ {[ evt ]} K + \through{s'} [| AnyStep app.(App.lts).(Sts._step) {[s]} evt s' |] + \through AuthSet.frag γ s' -∗ K evt + \end@{mpredI}. + Next Obligation. Abort. + *) + #[program] - Definition gen_requester_C {BS c cs} (_ : TCUnify BS (BS.String c cs) ):= + Definition requester_C (app : App.app) {s : _} s' evt + (ANY_STEP : AnyStep app.(App.lts).(Sts._step) {[s]} evt s'):= \cancelx - \using{γ} AuthSet.frag γ {[ BS ]} - \proving{E K} Step.gen_requester HelloWorld ⊤ E γ {[ x | x = Write c ]} K - \through AuthSet.frag γ {[ cs ]} -∗ K (Write c) - \end. + \using{γ} AuthSet.frag γ {[s]} + \proving{E K} Step.requester app E γ {[ evt ]} K + \through AuthSet.frag γ s' -∗ K evt + \end@{mpredI}. Next Obligation. - intros. inversion t; subst; clear t. - simpl; intros. + intros. work. - rewrite /Step.gen_requester /Step.gen_requester_learn. + rewrite /Step.requester. iAcIntro. rewrite /commit_acc. simpl. - iExists {[ BS.String c cs ]}. - simpl. - Require Import skylabs.upstream.cpp.misc_hints. - work. - iApply fupd_mask_intro. admit. + iApply fupd_mask_intro; [ by set_solver | ]. iIntros "Hclose". work. + iExists s. work. iSplitR. - iPureIntro. - { split. - eexists; set_solver. - intros. admit. } - iIntros. iMod "Hclose". - iModIntro. + { iPureIntro. + intros. destruct ANY_STEP. + inversion H; subst. apply _safe0. done. } + iIntros (?) "[% Hfrag]". iMod "Hclose". work. - assert (x = Write c) by admit. - iDestruct "Hclose" as "_". - iStopProof. - rewrite AuthSet.frag_proper. reflexivity. - admit. - Admitted. - Hint Resolve gen_requester_C : sl_opacity. + iDestruct (AuthSet.frag_upd with "Hfrag") as ">Hfrag"; last by iModIntro; iFrame. + inversion ANY_STEP. + inversion H; subst; clear H. + intros ? Hin. apply _steps_to0 in Hin. + inversion Hin as [?[??]]. + inversion H; subst. done. + Qed. + Hint Resolve requester_C : sl_opacity. + + Import kont. + + Definition X := @requester_C HelloWorld. + Hint Resolve X : sl_opacity. - Instance bs_dos_positive {OS: Ostream} b Q : IsPositive Q (ostream.bs_dos b Q) (ostream.bs_dos b). - Proof. - constructor. done. - constructor. intros. - induction b; simpl. - { iIntros "X"; iApply ("X" $! ()). } - { iIntros "X". admit. } - Admitted. Lemma main_ok : verify[source] "main()". - Proof. - Opaque ostream.bs_dos. - verify_shift; go. - Set Typeclasses Debug. - Set Typeclasses Debug Verbosity 1. - Hint Extern 0 (IsExistential ?X) => match goal with - | H : IsExistential _ |- _ => exact H - end : typeclass_instances. - work using canonical_Q. - Transparent ostream.bs_dos. - banish_string_literals. - iModIntro. - go. - Qed. + Proof. verify_shift; go; banish_string_literals; iModIntro; go. Qed. End with_cpp. 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 index ccb57be..c9177ba 100644 --- a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap.v +++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap.v @@ -12,20 +12,18 @@ Section with_cpp. | output_char c {b : bs} : only_output (BS.String c b) (Write c) b. Require Import skylabs.iris.extra.base_logic.lib.spectra. - About AuthSet.frag. - + Definition behavior (a b : Z) : bs := + "Before swapping a = " ++ + Z_to_string a ++ " , b = " ++ Z_to_string b ++ "\n" ++ + "After swapping a = " ++ Z_to_string b ++ " , b = " ++ Z_to_string a ++ "\n". cpp.spec "main()" from source as main_spec with ( \prepost{osM} _global "std::cout" |-> ostream.R 1$m osM - \pre AuthSet.frag γ {[ ]} + \pre AuthSet.frag γ {[ behavior 3 2 ]} \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" - ) + _global "std::cout" |-> ostream_contentR 1$m ** + AuthSet.frag γ {[ ""%bs ]} ). Lemma main_ok : verify[source] "main()". From 4ec8a0457c073c08d86b01ed1487613da2ff22d4 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Tue, 21 Apr 2026 12:10:11 -0400 Subject: [PATCH 06/13] Proof cleanup --- rocq-brick-libstdcpp/proof/iostream/pred.v | 1 + rocq-brick-libstdcpp/proof/iostream/spec.v | 15 ++ .../geeks_for_geeks_examples/N1_hello_world.v | 183 +++++++++--------- 3 files changed, 106 insertions(+), 93 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/iostream/pred.v b/rocq-brick-libstdcpp/proof/iostream/pred.v index 726cddb..ef7df67 100644 --- a/rocq-brick-libstdcpp/proof/iostream/pred.v +++ b/rocq-brick-libstdcpp/proof/iostream/pred.v @@ -29,6 +29,7 @@ Class SepHandler (PROP : bi) (evt : Set) : Type := (** This is effectively an <> that performs the event and then continues *) ; do_frame : forall evtP, ProperFrame (T:=[tele (_ : evt)]) (do evtP) }. +#[global] Hint Opaque do : sl_opacity. (** Events that send output. diff --git a/rocq-brick-libstdcpp/proof/iostream/spec.v b/rocq-brick-libstdcpp/proof/iostream/spec.v index dfe7452..d54201d 100644 --- a/rocq-brick-libstdcpp/proof/iostream/spec.v +++ b/rocq-brick-libstdcpp/proof/iostream/spec.v @@ -47,6 +47,21 @@ Module ostream. | BS.EmptyString => K | BS.String b bs => do {[Write b]} $ fun _ => bs_dos bs K end. + #[global] Hint Opaque bs_dos : sl_opacity. + + #[global] + Instance bs_dos_positive {OS: Ostream} b + : kont.ProperFrame (T:=[tele]) (bs_dos b). + Proof. + constructor; intros. + induction b; simpl. + { iIntros "X"; iApply ("X" $! ()). } + { iIntros "X". destruct OS. + iApply (do_frame {[Write b]}).(kont._frame). + iIntros ([?[]]); simpl. + iApply IHb. iAssumption. } + Qed. + cpp.spec "std::operator<<>(std::basic_ostream>&, const char*)" from source as ostream_insert_spec with ( 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 index ab84c57..b66e57f 100644 --- 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 @@ -17,114 +17,61 @@ Section to_spectra. Context {HAS_FUPD : BiFUpd PROP} {GHOSTLY : prop_constraints.Ghostly PROP}. Context `{SPECTRA : @appG evt lts Σ}. - #[global] Instance requester_frame' T app E γ ps (F : (T -t> PROP) -> [tele (_:App.evt app)] -t> PROP) : - kont.ProperFrame (PROP:=PROP) (T:=tele_snoc T [tele (_:App.evt app)]) - (fun K : tele_snoc T [tele _ : App.evt app] -t> PROP => Forall x : App.evt app, - let xxx :tele_arg [tele _ : App.evt app] := [tele_arg (x : App.evt app)] in - F (tele_bind (fun t : T => tele_app K (tele_arg_snoc t xxx))) x)%I -> - kont.ProperFrame (PROP:=PROP) (T:=T) (fun K => Step.requester app E γ ps (F K)). + Lemma tele_snoc_arg_snoc {TT T} (x : tele_snoc TT T) : exists ys y, + x = tele_arg_snoc ys y. Proof. - clear. intros. - constructor; simpl; intros. - rewrite /Step.requester. - iIntros "K". - Admitted. + clear. + induction TT; simpl in *. + { destruct x. exists tele_arg_tail, tele_arg_head. destruct tele_arg_tail. done. } + { destruct x. + destruct (H tele_arg_head tele_arg_tail) as [?[??]]. + subst. exists (TeleArgCons (f:=fun _ => _) tele_arg_head x), x0. done. } + Qed. + Lemma tele_app_bind_snoc {TT : tele} T U (x : T) : forall (xs : TT) (f : _ -> _ -> U), + tele_app (tele_bind_snoc f) (tele_arg_snoc xs x) = f xs x. + Proof. + clear. induction TT; intros. + { destruct xs; done. } + { destruct xs. etrans. apply H. done. } + Qed. - #[global] Instance requester_frame app E γ ps : - kont.ProperFrame (PROP:=PROP) (T:=[tele (_:App.evt app)]) (fun K => Step.requester app E γ ps K). + #[global] Instance requester_frame' T app E γ ps (F : (T -t> PROP) -> [tele (_:App.evt app)] -t> PROP) + : + (forall x, kont.ProperFrame (PROP:=PROP) (T:=T) (fun K => F K x)) -> + kont.ProperFrame (PROP:=PROP) (T:=T) (fun K => Step.requester app E γ ps (F K)). Proof. - clear. intros. - constructor; simpl; intros. + intros. + constructor. + iIntros (??) "K H". rewrite /Step.requester. - iIntros "K". - Admitted. - - Instance gen_requester_frame {TT:tele} {a b c d e} (F : (TT -t> _) -> _ -> _): - (forall x, kont.ProperFrame (T:=tele_snoc TT (App.evt a)) (fun K : (tele_snoc TT (App.evt a)) -t> _ => F (tele_bind (fun v => tele_app K (tele_arg_snoc v x))) x)) -> - kont.ProperFrame (T:=TT) (fun K => Step.gen_requester a b c d e (F K)). - Proof. Admitted. + iApply (atomic_commit_ppost_wand with "[H]") => //. + simpl. + iIntros (? e); destruct (H e). + iApply _frame. done. + Qed. - Lemma frag_frag_exact {T : Type} {_ : prop_constraints.HasUsualOwn PROP (auth_setR T)} γ val : + Context {T : Type} {HAS_OWN : prop_constraints.HasUsualOwn PROP (auth_setR T)}. + Lemma frag_frag_exact γ val : AuthSet.frag γ {[ val ]} ⊣⊢@{PROP} AuthSet.frag_exact γ val. Proof. reflexivity. Qed. Definition frag_frag_exact_F := [FWD<-] @frag_frag_exact. Definition frag_frag_exact_B := [BWD<-] @frag_frag_exact. -End to_spectra. -#[global] Hint Resolve frag_frag_exact_B frag_frag_exact_F : sl_opacity. -(* END UPSTREAM *) - - - -Inductive only_output : bs -> option output_event -> bs -> Prop := -| output_char {c} {b : bs} : only_output (BS.String c b) (Some $ Write c) b -| skip {bs} : only_output bs None bs. - -Definition the_app : LTS output_event := - {| Sts._state := bs - ; Sts._step := only_output |}. - -Section with_cpp. - Context `{Σ : cpp_logic, σ : genv}. - Context `{SPECTRA : !appG the_app _}. - - (* TODO: upstream this *) #[global] - Instance bs_dos_positive {OS: Ostream} b - : kont.ProperFrame (T:=[tele]) (fun K => ostream.bs_dos b K). - Proof. - constructor; intros. - induction b; simpl. - { iIntros "X"; iApply ("X" $! ()). } - { iIntros "X". destruct OS. - iApply (do_frame {[Write b]}).(kont._frame). - iIntros ([?[]]); simpl. - iApply IHb. iAssumption. } - Qed. - - - #[program] - Instance HelloWorld : App.app := - {| App.evt := output_event - ; App.lts := the_app - ; App.inG := _ - |}. - Next Obligation. - unshelve eapply mpred_prop.mpred_has_usual_own. apply SPECTRA. - Defined. - - #[program] - Definition OS (E : coPset) γ : Ostream := - {| do evt K := - Step.requester HelloWorld E γ evt K - |}%I. - - cpp.spec "main()" from source as main_spec with ( - \prepost{γ osM} _global "std::cout" |-> ostream.R (OS ⊤ γ) osM 1$m - \pre AuthSet.frag γ {[ "Hello World"%bs ]} - \post[Vint 0] - AuthSet.frag γ {[ ""%bs ]}). + Instance authset_frag_exact_learn {γ} : + Cbn (Learn (learn_eq ==> learn_hints.fin) (fun x => AuthSet.frag γ {[x]})). + Proof. clear. solve_learnable. Qed. + Hint Resolve authset_frag_exact_learn : sl_opacity. Class AnyStep {T E} (step : T -> option E -> T -> Prop) (Pre : propset T) (evt : E) (Post : propset T) : Prop := { _safe : forall s, s ∈ Pre -> exists s', step s (Some evt) s' ; _steps_to : forall s', s' ∈ Post -> ∃ s, s ∈ Pre /\ step s (Some evt) s' }. Hint Mode AnyStep + + + + + - : typeclass_instances. - Instance only_output_any_step {c cs} : AnyStep only_output {[ BS.String c cs ]} (Write c) {[ cs ]}. - Proof. - constructor; inversion 1; subst. - { eexists; constructor. } - { eexists; repeat constructor. } - Qed. - - #[global] Instance authset_frag_exact_learn : forall γ, Cbn (Learn (learn_eq ==> learn_hints.fin) (fun x => AuthSet.frag γ {[x]})). - Proof. clear. Admitted. - Hint Resolve authset_frag_exact_learn : sl_opacity. (* The early commit version #[program] - Definition requester_ec_C (app : App.app) {s : _} s' evt - (ANY_STEP : AnyStep app.(App.lts).(Sts._step) {[s]} evt s'):= + Definition requester_ec_C (app : App.app) (s : _) s' evt := \cancelx \using{γ} AuthSet.frag γ {[s]} \proving{E K} Step.requester app E γ {[ evt ]} K @@ -135,13 +82,13 @@ Section with_cpp. *) #[program] - Definition requester_C (app : App.app) {s : _} s' evt + Definition requester_C {_ : BiBUpdFUpd PROP} (app : App.app) (s : _) s' evt (ANY_STEP : AnyStep app.(App.lts).(Sts._step) {[s]} evt s'):= \cancelx \using{γ} AuthSet.frag γ {[s]} \proving{E K} Step.requester app E γ {[ evt ]} K \through AuthSet.frag γ s' -∗ K evt - \end@{mpredI}. + \end@{PROP}. Next Obligation. intros. work. @@ -152,13 +99,15 @@ Section with_cpp. iApply fupd_mask_intro; [ by set_solver | ]. iIntros "Hclose". work. - iExists s. work. + iExists s. + rewrite /AuthSet.frag_exact. work. iSplitR. { iPureIntro. intros. destruct ANY_STEP. inversion H; subst. apply _safe0. done. } iIntros (?) "[% Hfrag]". iMod "Hclose". work. + iApply bupd_fupd. iDestruct (AuthSet.frag_upd with "Hfrag") as ">Hfrag"; last by iModIntro; iFrame. inversion ANY_STEP. inversion H; subst; clear H. @@ -168,12 +117,60 @@ Section with_cpp. Qed. Hint Resolve requester_C : sl_opacity. +End to_spectra. +#[global] Hint Resolve frag_frag_exact_B frag_frag_exact_F : sl_opacity. +(* END UPSTREAM *) + + + +Inductive only_output : bs -> option output_event -> bs -> Prop := +| output_char {c} {b : bs} : only_output (BS.String c b) (Some $ Write c) b +| skip {bs} : only_output bs None bs. + +Instance only_output_any_step {c cs} : AnyStep only_output {[ BS.String c cs ]} (Write c) {[ cs ]}. +Proof. + constructor; inversion 1; subst. + { eexists; constructor. } + { eexists; repeat constructor. } +Qed. + +Definition output_app (init : bs -> Prop) : LTS output_event := + {| Sts._state := bs + ; Sts._init_state := init + ; Sts._step := only_output |}. + +Section with_cpp. + Context `{Σ : cpp_logic, σ : genv}. + + (* TODO: upstream this *) + + Context `{SPECTRA : !appG (output_app (eq "Hello World"%bs)) _Σ}. + + #[program] + Instance HelloWorld : App.app := + {| App.evt := output_event + ; App.lts := output_app (eq "Hello World"%bs) + ; App.inG := _ + |}. + Next Obligation. + unshelve eapply mpred_prop.mpred_has_usual_own. apply SPECTRA. + Defined. + + #[program] + Definition OS (E : coPset) γ : Ostream := + {| do evt K := Step.requester HelloWorld E γ evt K |}%I. + + cpp.spec "main()" from source as main_spec with ( + \prepost{γ osM} _global "std::cout" |-> ostream.R (OS ⊤ γ) osM 1$m + \pre AuthSet.frag γ {[ "Hello World"%bs ]} + \post[Vint 0] + AuthSet.frag γ {[ ""%bs ]}). + Import kont. - Definition X := @requester_C HelloWorld. + Definition X := requester_C HelloWorld. Hint Resolve X : sl_opacity. - Lemma main_ok : verify[source] "main()". Proof. verify_shift; go; banish_string_literals; iModIntro; go. Qed. From a07a78c378456cc5f03a7528bb6a06f27dbbf2d0 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Fri, 24 Apr 2026 06:27:56 -0400 Subject: [PATCH 07/13] Changing the event interface to [N] Other cleanup to start expanding. --- rocq-brick-libstdcpp/proof/iostream/pred.v | 4 +- rocq-brick-libstdcpp/proof/iostream/spec.v | 14 +- .../geeks_for_geeks_examples/N1_hello_world.v | 132 +-------------- .../test/geeks_for_geeks_examples/prelude.v | 155 ++++++++++++++++++ 4 files changed, 169 insertions(+), 136 deletions(-) create mode 100644 rocq-brick-libstdcpp/test/geeks_for_geeks_examples/prelude.v diff --git a/rocq-brick-libstdcpp/proof/iostream/pred.v b/rocq-brick-libstdcpp/proof/iostream/pred.v index ef7df67..36a831c 100644 --- a/rocq-brick-libstdcpp/proof/iostream/pred.v +++ b/rocq-brick-libstdcpp/proof/iostream/pred.v @@ -37,10 +37,10 @@ Class SepHandler (PROP : bi) (evt : Set) : Type := to be sent to the consumer on a [Flush]. *) Variant output_event : Set := - | Write (_ : Byte.byte). + | Write (_ : N). Variant input_event : Set := - | Read (_ : Byte.byte). + | Read (_ : N). (** The behavior of an [ostream] is described by a handler of an [output_event] *) Notation Ostream := (SepHandler mpred output_event). diff --git a/rocq-brick-libstdcpp/proof/iostream/spec.v b/rocq-brick-libstdcpp/proof/iostream/spec.v index d54201d..889af1a 100644 --- a/rocq-brick-libstdcpp/proof/iostream/spec.v +++ b/rocq-brick-libstdcpp/proof/iostream/spec.v @@ -42,26 +42,31 @@ Module ostream. #[global] Instance: Cbn (Learn (learn_eq ==> learn_eq ==> any ==> learn_hints.fin) R). Proof. solve_learnable. Qed. - Fixpoint bs_dos {_ : Ostream} (bs : bs) (K : mpred) : mpred := + Fixpoint bs_dos {OS : Ostream} (bs : bs) (K : mpred) : mpred := match bs with | BS.EmptyString => K - | BS.String b bs => do {[Write b]} $ fun _ => bs_dos bs K + | BS.String b bs => do {[Write $ Byte.to_N b]} $ fun _ => bs_dos bs K end. #[global] Hint Opaque bs_dos : sl_opacity. #[global] - Instance bs_dos_positive {OS: Ostream} b + Instance bs_dos_proper_frame {OS: Ostream} b : kont.ProperFrame (T:=[tele]) (bs_dos b). Proof. constructor; intros. induction b; simpl. { iIntros "X"; iApply ("X" $! ()). } { iIntros "X". destruct OS. - iApply (do_frame {[Write b]}).(kont._frame). + iApply (do_frame {[Write $ Byte.to_N b]}).(kont._frame). iIntros ([?[]]); simpl. iApply IHb. iAssumption. } Qed. + #[global] + Instance bs_dos_positive_proper_frame_eta {OS: Ostream} b + : kont.ProperFrame (T:=[tele]) (fun x => bs_dos b x). + Proof. apply bs_dos_proper_frame. Qed. + cpp.spec "std::operator<<>(std::basic_ostream>&, const char*)" from source as ostream_insert_spec with ( @@ -150,7 +155,6 @@ Module istream. nP |-> intR 1$m n ). - End with_cpp. End istream. 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 index b66e57f..33f8b7b 100644 --- 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 @@ -3,137 +3,12 @@ Require Import skylabs.brick.libstdcpp.iostream.spec. Require Import skylabs.iris.extra.base_logic.lib.spectra. +Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.prelude. Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.N1_hello_world_cpp. Import linearity. -(* BEGIN UPSTREAM *) -Definition appG {evt : Type} (lts : LTS evt) (Σ : gFunctors) : Type := - inG Σ (auth_setR (lts_state lts)). - -Section to_spectra. - Context {PROP : bi}. - Context {HAS_FUPD : BiFUpd PROP} {GHOSTLY : prop_constraints.Ghostly PROP}. - Context `{SPECTRA : @appG evt lts Σ}. - - Lemma tele_snoc_arg_snoc {TT T} (x : tele_snoc TT T) : exists ys y, - x = tele_arg_snoc ys y. - Proof. - clear. - induction TT; simpl in *. - { destruct x. exists tele_arg_tail, tele_arg_head. destruct tele_arg_tail. done. } - { destruct x. - destruct (H tele_arg_head tele_arg_tail) as [?[??]]. - subst. exists (TeleArgCons (f:=fun _ => _) tele_arg_head x), x0. done. } - Qed. - Lemma tele_app_bind_snoc {TT : tele} T U (x : T) : forall (xs : TT) (f : _ -> _ -> U), - tele_app (tele_bind_snoc f) (tele_arg_snoc xs x) = f xs x. - Proof. - clear. induction TT; intros. - { destruct xs; done. } - { destruct xs. etrans. apply H. done. } - Qed. - - #[global] Instance requester_frame' T app E γ ps (F : (T -t> PROP) -> [tele (_:App.evt app)] -t> PROP) - : - (forall x, kont.ProperFrame (PROP:=PROP) (T:=T) (fun K => F K x)) -> - kont.ProperFrame (PROP:=PROP) (T:=T) (fun K => Step.requester app E γ ps (F K)). - Proof. - intros. - constructor. - iIntros (??) "K H". - rewrite /Step.requester. - iApply (atomic_commit_ppost_wand with "[H]") => //. - simpl. - iIntros (? e); destruct (H e). - iApply _frame. done. - Qed. - - Context {T : Type} {HAS_OWN : prop_constraints.HasUsualOwn PROP (auth_setR T)}. - Lemma frag_frag_exact γ val : - AuthSet.frag γ {[ val ]} ⊣⊢@{PROP} AuthSet.frag_exact γ val. - Proof. reflexivity. Qed. - Definition frag_frag_exact_F := [FWD<-] @frag_frag_exact. - Definition frag_frag_exact_B := [BWD<-] @frag_frag_exact. - - #[global] - Instance authset_frag_exact_learn {γ} : - Cbn (Learn (learn_eq ==> learn_hints.fin) (fun x => AuthSet.frag γ {[x]})). - Proof. clear. solve_learnable. Qed. - Hint Resolve authset_frag_exact_learn : sl_opacity. - - Class AnyStep {T E} (step : T -> option E -> T -> Prop) (Pre : propset T) (evt : E) (Post : propset T) : Prop := - { _safe : forall s, s ∈ Pre -> exists s', step s (Some evt) s' - ; _steps_to : forall s', s' ∈ Post -> ∃ s, s ∈ Pre /\ step s (Some evt) s' }. - Hint Mode AnyStep + + + + + - : typeclass_instances. - - - (* The early commit version - #[program] - Definition requester_ec_C (app : App.app) (s : _) s' evt := - \cancelx - \using{γ} AuthSet.frag γ {[s]} - \proving{E K} Step.requester app E γ {[ evt ]} K - \through{s'} [| AnyStep app.(App.lts).(Sts._step) {[s]} evt s' |] - \through AuthSet.frag γ s' -∗ K evt - \end@{mpredI}. - Next Obligation. Abort. - *) - - #[program] - Definition requester_C {_ : BiBUpdFUpd PROP} (app : App.app) (s : _) s' evt - (ANY_STEP : AnyStep app.(App.lts).(Sts._step) {[s]} evt s'):= - \cancelx - \using{γ} AuthSet.frag γ {[s]} - \proving{E K} Step.requester app E γ {[ evt ]} K - \through AuthSet.frag γ s' -∗ K evt - \end@{PROP}. - Next Obligation. - intros. - work. - rewrite /Step.requester. - iAcIntro. - rewrite /commit_acc. - simpl. - iApply fupd_mask_intro; [ by set_solver | ]. - iIntros "Hclose". - work. - iExists s. - rewrite /AuthSet.frag_exact. work. - iSplitR. - { iPureIntro. - intros. destruct ANY_STEP. - inversion H; subst. apply _safe0. done. } - iIntros (?) "[% Hfrag]". iMod "Hclose". - work. - iApply bupd_fupd. - iDestruct (AuthSet.frag_upd with "Hfrag") as ">Hfrag"; last by iModIntro; iFrame. - inversion ANY_STEP. - inversion H; subst; clear H. - intros ? Hin. apply _steps_to0 in Hin. - inversion Hin as [?[??]]. - inversion H; subst. done. - Qed. - Hint Resolve requester_C : sl_opacity. - -End to_spectra. -#[global] Hint Resolve frag_frag_exact_B frag_frag_exact_F : sl_opacity. -(* END UPSTREAM *) - - - -Inductive only_output : bs -> option output_event -> bs -> Prop := -| output_char {c} {b : bs} : only_output (BS.String c b) (Some $ Write c) b -| skip {bs} : only_output bs None bs. - -Instance only_output_any_step {c cs} : AnyStep only_output {[ BS.String c cs ]} (Write c) {[ cs ]}. -Proof. - constructor; inversion 1; subst. - { eexists; constructor. } - { eexists; repeat constructor. } -Qed. - Definition output_app (init : bs -> Prop) : LTS output_event := {| Sts._state := bs ; Sts._init_state := init @@ -163,8 +38,7 @@ Section with_cpp. cpp.spec "main()" from source as main_spec with ( \prepost{γ osM} _global "std::cout" |-> ostream.R (OS ⊤ γ) osM 1$m \pre AuthSet.frag γ {[ "Hello World"%bs ]} - \post[Vint 0] - AuthSet.frag γ {[ ""%bs ]}). + \post[Vint 0] AuthSet.frag γ {[ ""%bs ]}). Import kont. @@ -172,6 +46,6 @@ Section with_cpp. Hint Resolve X : sl_opacity. Lemma main_ok : verify[source] "main()". - Proof. verify_shift; go; banish_string_literals; iModIntro; go. Qed. + Proof. verify_shift; go. banish_string_literals. iModIntro; go. Qed. End with_cpp. diff --git a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/prelude.v b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/prelude.v new file mode 100644 index 0000000..6fe975e --- /dev/null +++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/prelude.v @@ -0,0 +1,155 @@ +Require Export skylabs.auto.cpp.prelude.proof. +Require Export skylabs.brick.libstdcpp.iostream.spec. + +Require Export skylabs.iris.extra.base_logic.lib.spectra. + +(* BEGIN UPSTREAM *) +Definition appG {evt : Type} (lts : LTS evt) (Σ : gFunctors) : Type := + inG Σ (auth_setR (lts_state lts)). + +Section to_tele. + Lemma tele_snoc_arg_snoc {TT T} (x : tele_snoc TT T) : exists ys y, + x = tele_arg_snoc ys y. + Proof. + clear. + induction TT; simpl in *. + { destruct x. exists tele_arg_tail, tele_arg_head. destruct tele_arg_tail. done. } + { destruct x. + destruct (H tele_arg_head tele_arg_tail) as [?[??]]. + subst. exists (TeleArgCons (f:=fun _ => _) tele_arg_head x), x0. done. } + Qed. + Lemma tele_app_bind_snoc {TT : tele} T U (x : T) : forall (xs : TT) (f : _ -> _ -> U), + tele_app (tele_bind_snoc f) (tele_arg_snoc xs x) = f xs x. + Proof. + clear. induction TT; intros. + { destruct xs; done. } + { destruct xs. etrans. apply H. done. } + Qed. +End to_tele. + +(* FOR SPECTRA *) +Section operational. + Context {T E} (step : T -> option E -> T -> Prop). + + Class AnyStep (Pre : propset T) (evt : E) (Post : propset T) : Prop := + { _safe : forall s, s ∈ Pre -> exists s', step s (Some evt) s' + ; _steps_to : forall s', s' ∈ Post -> ∃ s, s ∈ Pre /\ step s (Some evt) s' }. + + + Inductive AnySteps (Pre : propset T) : list E -> propset T -> Prop := + | Finish {Post} {_ : ∅ ⊂ Post} (_ : Post ⊆ Pre) : AnySteps Pre [] Post + | Refine {Pre'} {_ : ∅ ⊂ Pre} (_ : Pre' ⊆ Pre) {es Post} : + AnySteps Pre' es Post -> AnySteps Pre es Post + | Step {evt Post} + (SAFE : forall s, s ∈ Pre -> ∃ s', step s (Some evt) s') + (STEPS_TO : forall s', s' ∈ Post -> ∃ s, s ∈ Pre /\ step s (Some evt) s') + : AnySteps Pre [evt] Post. + +End operational. +#[global] Hint Mode AnyStep + + + + + - : typeclass_instances. +#[global] Hint Mode AnySteps + + + + + - : typeclass_instances. + + +Section to_spectra. + Context {PROP : bi}. + Context {HAS_FUPD : BiFUpd PROP} {GHOSTLY : prop_constraints.Ghostly PROP}. + Context `{SPECTRA : @appG evt lts Σ}. + + + #[global] Instance requester_frame' T app E γ ps (F : (T -t> PROP) -> [tele (_:App.evt app)] -t> PROP) + : + (forall x, kont.ProperFrame (PROP:=PROP) (T:=T) (fun K => F K x)) -> + kont.ProperFrame (PROP:=PROP) (T:=T) (fun K => Step.requester app E γ ps (F K)). + Proof. + intros. + constructor. + iIntros (??) "K H". + rewrite /Step.requester. + iApply (atomic_commit_ppost_wand with "[H]") => //. + simpl. + iIntros (? e); destruct (H e). + iApply _frame. done. + Qed. + + Context {T : Type} {HAS_OWN : prop_constraints.HasUsualOwn PROP (auth_setR T)}. + Lemma frag_frag_exact γ val : + AuthSet.frag γ {[ val ]} ⊣⊢@{PROP} AuthSet.frag_exact γ val. + Proof. reflexivity. Qed. + Definition frag_frag_exact_F := [FWD<-] @frag_frag_exact. + Definition frag_frag_exact_B := [BWD<-] @frag_frag_exact. + + #[global] + Instance authset_frag_exact_learn {γ} : + Cbn (Learn (learn_eq ==> learn_hints.fin) (fun x => AuthSet.frag γ {[x]})). + Proof. clear. solve_learnable. Qed. + Hint Resolve authset_frag_exact_learn : sl_opacity. + + + (* The early commit version + #[program] + Definition requester_ec_C (app : App.app) (s : _) s' evt := + \cancelx + \using{γ} AuthSet.frag γ {[s]} + \proving{E K} Step.requester app E γ {[ evt ]} K + \through{s'} [| AnyStep app.(App.lts).(Sts._step) {[s]} evt s' |] + \through AuthSet.frag γ s' -∗ K evt + \end@{mpredI}. + Next Obligation. Abort. + *) + + #[program] + Definition requester_C {_ : BiBUpdFUpd PROP} (app : App.app) (s : _) s' evt + (ANY_STEP : AnyStep app.(App.lts).(Sts._step) {[s]} evt s'):= + \cancelx + \using{γ} AuthSet.frag γ {[s]} + \proving{E K} Step.requester app E γ {[ evt ]} K + \through AuthSet.frag γ s' -∗ K evt + \end@{PROP}. + Next Obligation. + intros. + work. + rewrite /Step.requester. + iAcIntro. + rewrite /commit_acc. + simpl. + iApply fupd_mask_intro; [ by set_solver | ]. + iIntros "Hclose". + work. + iExists s. + rewrite /AuthSet.frag_exact. work. + iSplitR. + { iPureIntro. + intros. destruct ANY_STEP. + inversion H; subst. apply _safe0. done. } + iIntros (?) "[% Hfrag]". iMod "Hclose". + work. + iApply bupd_fupd. + iDestruct (AuthSet.frag_upd with "Hfrag") as ">Hfrag"; last by iModIntro; iFrame. + inversion ANY_STEP. + inversion H; subst; clear H. + intros ? Hin. apply _steps_to0 in Hin. + inversion Hin as [?[??]]. + inversion H; subst. done. + Qed. + Hint Resolve requester_C : sl_opacity. + +End to_spectra. +#[global] Hint Resolve frag_frag_exact_B frag_frag_exact_F : sl_opacity. +(* END UPSTREAM *) + + +(** The step relation for a simple LTS that uses [bs] as the state. + + This LTS only supports output transitions. + *) +Inductive only_output : bs -> option output_event -> bs -> Prop := +| output_char {c} {b : bs} : only_output (BS.String c b) (Some $ Write c) b +| skip {bs} : only_output bs None bs. + +#[global] +Instance only_output_any_step {c cs} : AnyStep only_output {[ BS.String c cs ]} (Write c) {[ cs ]}. +Proof. + constructor; inversion 1; subst. + { eexists; constructor. } + { eexists; repeat constructor. } +Qed. From 635fd64987112a027a4069337dab9f80e06fdc12 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Thu, 30 Apr 2026 23:02:34 -0400 Subject: [PATCH 08/13] Proof of [N4_sum] --- rocq-brick-libstdcpp/proof/iostream/itree.v | 106 ++++++++++++++++++ rocq-brick-libstdcpp/proof/iostream/pred.v | 46 +++++++- rocq-brick-libstdcpp/proof/iostream/spec.v | 34 +++--- .../geeks_for_geeks_examples/N1_hello_world.v | 1 + .../test/geeks_for_geeks_examples/N4_sum.v | 54 +++++++-- .../test/geeks_for_geeks_examples/prelude.v | 72 ++++++++++-- 6 files changed, 276 insertions(+), 37 deletions(-) create mode 100644 rocq-brick-libstdcpp/proof/iostream/itree.v diff --git a/rocq-brick-libstdcpp/proof/iostream/itree.v b/rocq-brick-libstdcpp/proof/iostream/itree.v new file mode 100644 index 0000000..e0e4b77 --- /dev/null +++ b/rocq-brick-libstdcpp/proof/iostream/itree.v @@ -0,0 +1,106 @@ +CoInductive itree {E : Type -> Type} {T : Type} : Type := +| Ret (_ : T) +| Tau (_ : itree) +| Do {U} (_ : E U) (_ : U -> itree). +#[global] Arguments itree E T : clear implicits. + +Section with_E. + Context {E : Type -> Type}. + + CoFixpoint bind {T U} (it : itree E T) (k : T -> itree E U) : itree E U := + match it with + | Ret v => k v + | Tau it => Tau (bind it k) + | Do e k' => Do e (fun x => bind (k' x) k) + end. + +End with_E. + +Require Import stdpp.numbers. + +Variant input_char : Type -> Type := + | read : input_char N. + +Require Import stdpp.base. +Require Import stdpp.numbers. + +(** [is_ws] returns true if the character is a standard whitespace. + Uses stdpp's bool_decide to evaluate the logical disjunction. *) +Definition is_ws (c : N) : bool := + bool_decide (c = 32 \/ c = 10 \/ c = 13 \/ c = 9)%N. + +(** [as_digit] returns [Some d] if the character is between '0' and '9'. + Uses stdpp's bool_decide to evaluate the logical conjunction. *) +Definition as_digit (c : N) : option N := + if bool_decide (48 <= c /\ c <= 57)%N then + Some (c - 48)%N + else + None. + +(** [read_int] reads characters using [Do read] and parses + the string as an integer. For example, the characters + <1>, <2>, <\n> would return <('\n', 12)>. + + The function accepts both positive and negative integers. + + The first component is the "overread", the first byte read that + is not part of the number. + *) +CoFixpoint read_int : itree input_char (N * Z) := + (* Internal state machine to accumulate parsed digits *) + let cofix loop (sign : Z) (acc : Z) : itree input_char (N * Z) := + Do read (fun c => + match as_digit c with + | Some digit => + loop sign (acc * 10 + Z.of_N digit)%Z + | None => + (* Not a digit: return the delimiter character and the final signed integer *) + Ret (c, (sign * acc)%Z) + end + ) + in + + Do read (fun c => + if (c =? 45)%N then + (* Encountered '-' (ASCII 45) -> Start reading negative number *) + loop (-1)%Z 0%Z + + else if (c =? 43)%N then + (* Encountered '+' (ASCII 43) -> Start reading positive number *) + loop 1%Z 0%Z + + else if is_ws c then + (* Whitespace (space, \n, \r, \t) -> Co-recursively skip *) + read_int + + else match as_digit c with + | Some digit => + (* Encountered a digit -> Start accumulating a positive number *) + loop 1%Z (Z.of_N digit) + | None => + (* Unexpected character before any digits -> Abort and return 0 *) + Ret (c, 0%Z) + end + ). + + +Require Import skylabs.prelude.sts. + +Section as_lts. + Context {E : Type -> Type}. + Context {Evt : Type}. + + Context {as_evt : forall {T}, E T -> T -> Evt}. + + + Variant itree_step : itree E unit -> option Evt -> itree E unit -> Prop := + | step_do {T} {act : E T} (r : T) k + : itree_step (Do act k) (Some $ as_evt _ act r) (k r) + | step_tau {k} + : itree_step (Tau k) None k. + + Definition itree_lts (it : itree E unit) : LTS Evt := + {| Sts._state := itree E unit + ; Sts._init_state := eq it + ; Sts._step := itree_step |}. +End as_lts. diff --git a/rocq-brick-libstdcpp/proof/iostream/pred.v b/rocq-brick-libstdcpp/proof/iostream/pred.v index 36a831c..de4cf94 100644 --- a/rocq-brick-libstdcpp/proof/iostream/pred.v +++ b/rocq-brick-libstdcpp/proof/iostream/pred.v @@ -10,6 +10,8 @@ Require Export skylabs.cpp.string. Require Import skylabs.auto.hints.kont. +Require Import skylabs.brick.libstdcpp.iostream.itree. + Require Import skylabs.brick.libstdcpp.iostream.inc_iostream_cpp. (** TODO upstream START *) @@ -24,13 +26,55 @@ Require Import skylabs.brick.libstdcpp.iostream.inc_iostream_cpp. Generally, this will be an that proves that is a valid next event. *) -Class SepHandler (PROP : bi) (evt : Set) : Type := +Class SepHandler (PROP : bi) (evt : Type) : Type := { do : propset evt -> (evt -> PROP) -> PROP (** This is effectively an <> that performs the event and then continues *) ; do_frame : forall evtP, ProperFrame (T:=[tele (_ : evt)]) (do evtP) +; do_ne : forall n, Proper ((≡) ==> pointwise_relation _ (dist n) ==> (dist n)) do }. #[global] Hint Opaque do : sl_opacity. +(* TODO: these should be replaced by library definitions *) +Section interp_itree. + Context {PROP : bi}. + Context {PROP_LATER : BiLaterContractive PROP}. + + Context {E : Type -> Type}. + Context {Evt : Type}. + Variable as_evt : forall {T}, E T -> T -> Evt. + + Context (SH : SepHandler PROP Evt). + + #[local] + Definition interp_do_body {T} (K : T -> PROP) (rec : itree E T -d> PROP) : itree E T -d> PROP := + funI it => + match it with + | Ret v => K v + | Tau x => |> rec x + | Do act k => + letI* evt := do {[ evt | exists r, evt = as_evt act r ]} in + ∃ r, [| evt = as_evt act r |] ∗ |> rec (k r) + end. + + #[local] + Instance interp_do_body_contractive {T} {K : T -> PROP} : Contractive (interp_do_body K). + Proof using PROP_LATER. + repeat intro. + destruct x0; simpl; try eauto. + { apply later_contractive. constructor. + intros. apply H. done. } + { eapply do_ne. done. + intro. apply bi.exist_ne; intro. apply bi.sep_ne. done. apply later_contractive. + constructor; intros; apply H; done. } + Qed. + + Definition interp_itree {T} (it : itree E T) (K : T -> PROP) : PROP := + fixpoint (A:=_ -d> PROP) (interp_do_body K) it. + +End interp_itree. +#[global] Arguments interp_itree {PROP _ E Event} as_evt {SepHandler _} it _%_I : rename. + + (** Events that send output. For most buffered streams, writes go to the buffer and are only guaranteed diff --git a/rocq-brick-libstdcpp/proof/iostream/spec.v b/rocq-brick-libstdcpp/proof/iostream/spec.v index 889af1a..f623731 100644 --- a/rocq-brick-libstdcpp/proof/iostream/spec.v +++ b/rocq-brick-libstdcpp/proof/iostream/spec.v @@ -8,6 +8,7 @@ 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.itree. Require Import skylabs.brick.libstdcpp.iostream.inc_iostream_cpp. @@ -31,17 +32,9 @@ Record ioflags : Set := Module ostream. - Parameter gname : Set. - - (** TODO: Add support for *) - Parameter R : forall `{Σ : cpp_logic} {σ : genv}, Ostream -> gname -> cQp.t -> Rep. - Section with_cpp. Context `{Σ : cpp_logic, σ : genv}. - #[global] Instance: Cbn (Learn (learn_eq ==> learn_eq ==> any ==> learn_hints.fin) R). - Proof. solve_learnable. Qed. - Fixpoint bs_dos {OS : Ostream} (bs : bs) (K : mpred) : mpred := match bs with | BS.EmptyString => K @@ -71,7 +64,7 @@ Module ostream. cpp.spec "std::operator<<>(std::basic_ostream>&, const char*)" from source as ostream_insert_spec with ( \arg{osP} "" (Vptr osP) - \prepost{OS γ} osP |-> R OS γ 1$m + \prepost{OS γ} osP |-> ostream.R OS γ 1$m \arg{strP} "" (Vptr strP) \prepost{q__s strM} strP |-> cstring.R q__s strM \pre{Q} bs_dos strM Q @@ -85,7 +78,7 @@ Module ostream. from source as ostream_print_int_spec with ( \this this \arg{n} "" (Vint n) - \prepost{OS γ} this |-> R OS γ 1$m + \prepost{OS γ} this |-> ostream.R OS γ 1$m \pre{Q} bs_dos (format_int n) Q \post[Vptr this] Q ). @@ -94,7 +87,7 @@ Module ostream. from source as ostream_print_ulong_spec with ( \this this \arg{n} "" (Vint n) - \prepost{OS γ} this |-> R OS γ 1$m + \prepost{OS γ} this |-> ostream.R OS γ 1$m \pre{Q} bs_dos (format_int n) Q \post[Vptr this] Q ). @@ -102,7 +95,7 @@ Module ostream. Definition iostream_manip_spec contents_f : WpSpec_cpp_val := ( \arg{osP : ptr} "" (Vptr osP) (* XXX: manipulators can cause output! *) - \prepost{OS γ} osP |-> R OS γ 1$m + \prepost{OS γ} osP |-> ostream.R OS γ 1$m \pre{Q} bs_dos contents_f Q \post[Vptr osP] Q). @@ -133,26 +126,25 @@ Module ostream. End ostream. Module istream. - Parameter gname : Set. - Parameter R : forall `{Σ : cpp_logic} {σ : genv}, Istream -> gname -> cQp.t -> Rep. - Section with_cpp. Context `{Σ : cpp_logic, σ : genv}. - #[global] Instance: Cbn (Learn (learn_eq ==> learn_eq ==> any ==> learn_hints.fin) R). - Proof. solve_learnable. Qed. + Definition as_event (T : Type) (act : input_char T) : T -> input_event := + match act in input_char T return T -> _ with + | read => fun n => Read n + end. - (** NOTE: this specification is weak because it does not connect to the - actual stream "contents". *) cpp.spec "std::basic_istream>::operator>>(int&)" from source as istream_take_int_spec with ( \this this \pre{IS isM} this |-> istream.R IS isM 1$m - \arg{nP} "" (Vptr nP) + \arg{nP} "" (Vref nP) \pre nP |-> anyR "int" 1$m + \pre{K : Z -> mpred} interp_itree as_event read_int (K ∘ snd) \post[Vptr this] Exists isM' n, this |-> istream.R IS isM' 1$m ** - nP |-> intR 1$m n + nP |-> intR 1$m n ** + K n ). End with_cpp. 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 index 33f8b7b..fb0a7f2 100644 --- 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 @@ -34,6 +34,7 @@ Section with_cpp. #[program] Definition OS (E : coPset) γ : Ostream := {| do evt K := Step.requester HelloWorld E γ evt K |}%I. + Next Obligation. intros. repeat intro. by apply requester_ne. Qed. cpp.spec "main()" from source as main_spec with ( \prepost{γ osM} _global "std::cout" |-> ostream.R (OS ⊤ γ) osM 1$m 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 index ebed51a..6b651e1 100644 --- a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N4_sum.v +++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N4_sum.v @@ -1,20 +1,58 @@ -Require Import skylabs.auto.cpp.prelude.proof. -Require Import skylabs.brick.libstdcpp.iostream.spec. - +Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.prelude. Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.N4_sum_cpp. Import linearity. +Definition output_app (init : bs -> Prop) : LTS output_event := + {| Sts._state := bs + ; Sts._init_state := init + ; Sts._step := only_output |}. + + Section with_cpp. Context `{Σ : cpp_logic, σ : genv}. + Context `{SPECTRA : !appG (output_app (eq $ ostream.format_int 20)) _Σ}. + + #[program] + Instance Sum : App.app := + {| App.evt := output_event + ; App.lts := output_app (eq $ ostream.format_int 20) + ; App.inG := _ + |}. + Next Obligation. + unshelve eapply mpred_prop.mpred_has_usual_own. apply SPECTRA. + Defined. + + #[program] + Definition OS (E : coPset) γ : Ostream := + {| do evt K := Step.requester Sum E γ evt K |}%I. + Next Obligation. repeat intro. apply requester_ne; done. Qed. + + Definition X := Step.requester Sum. + #[local] Hint Resolve X : sl_opacity. + + #[program] + Definition bs_dos_steps_C (s : bs) (s' : propset (Sts._state (App.lts Sum))) str + (ANY_STEPS : AnySteps only_output {[s]} ((fun x => Write x) <$> BS.string_to_bytes str) s') := + \cancelx + \using{γ} AuthSet.frag γ {[s]} + \proving{K : mpredI} ostream.bs_dos (OS:=OS ⊤ γ) str K + \through (AuthSet.frag γ s' -∗ K) + \end@{mpredI}. + Next Obligation. + simpl. + intros. + iIntros "F" (?) "K". + rewrite /Step.requester. + Admitted. + Hint Resolve bs_dos_steps_C : sl_opacity. 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) - ). + \prepost{γ osM} _global "std::cout" |-> ostream.R (OS ⊤ γ) osM 1$m + \pre AuthSet.frag γ {[ ostream.format_int 20 ]} + \post[Vint 0] AuthSet.frag γ {[ ""%bs ]}). 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/prelude.v b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/prelude.v index 6fe975e..01d578f 100644 --- a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/prelude.v +++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/prelude.v @@ -38,14 +38,15 @@ Section operational. Inductive AnySteps (Pre : propset T) : list E -> propset T -> Prop := | Finish {Post} {_ : ∅ ⊂ Post} (_ : Post ⊆ Pre) : AnySteps Pre [] Post + | Step {evt evts Mid Post} + (_ : AnyStep Pre evt Mid) + (_ : AnySteps Mid evts Post) + : AnySteps Pre (evt :: evts) Post | Refine {Pre'} {_ : ∅ ⊂ Pre} (_ : Pre' ⊆ Pre) {es Post} : - AnySteps Pre' es Post -> AnySteps Pre es Post - | Step {evt Post} - (SAFE : forall s, s ∈ Pre -> ∃ s', step s (Some evt) s') - (STEPS_TO : forall s', s' ∈ Post -> ∃ s, s ∈ Pre /\ step s (Some evt) s') - : AnySteps Pre [evt] Post. + AnySteps Pre' es Post -> AnySteps Pre es Post. End operational. +Existing Class AnySteps. #[global] Hint Mode AnyStep + + + + + - : typeclass_instances. #[global] Hint Mode AnySteps + + + + + - : typeclass_instances. @@ -133,6 +134,18 @@ Section to_spectra. Qed. Hint Resolve requester_C : sl_opacity. + #[global] + Instance requester_ne {app E γ} : + forall n, Proper ((≡) ==> pointwise_relation _ (dist n) ==> dist n) (Step.requester app E γ). + Proof. + repeat intro. + apply atomic_commit_ne => //; repeat intro; + repeat match goal with + | h : tele_arg _ |- _ => destruct h + end; simpl; repeat f_equiv; eauto. + by setoid_rewrite H. + Qed. + End to_spectra. #[global] Hint Resolve frag_frag_exact_B frag_frag_exact_F : sl_opacity. (* END UPSTREAM *) @@ -143,13 +156,58 @@ End to_spectra. This LTS only supports output transitions. *) Inductive only_output : bs -> option output_event -> bs -> Prop := -| output_char {c} {b : bs} : only_output (BS.String c b) (Some $ Write c) b +| output_char {c} {b : bs} : only_output (BS.String c b) (Some $ Write $ Byte.to_N c) b | skip {bs} : only_output bs None bs. #[global] -Instance only_output_any_step {c cs} : AnyStep only_output {[ BS.String c cs ]} (Write c) {[ cs ]}. +Instance only_output_any_step {c cs} : AnyStep only_output {[ BS.String c cs ]} (Write $ Byte.to_N c) {[ cs ]}. Proof. constructor; inversion 1; subst. { eexists; constructor. } { eexists; repeat constructor. } Qed. + +#[global] +Instance final_any_steps {str str' : bs} : + str = str' -> + AnySteps only_output {[str]} + ((λ x : N, Write x) <$> BS.string_to_bytes (str')) + {[""%bs]}. +Proof. + intros; subst. + clear. + induction str'. + { constructor; set_solver. } + { simpl. + econstructor; [ | eassumption ]. + constructor. + { intros. exists str'. + inversion H; subst. constructor. } + { inversion 1; subst. + eexists _; split. set_solver. + constructor. } } +Qed. + +#[global] +Instance initial_any_steps {str str' rest : bs} : + str = str' -> + AnySteps only_output {[str ++ rest]}%bs + ((λ x : N, Write x) <$> BS.string_to_bytes (str')) + {[rest]}. +Proof. + intros; subst. + clear. + revert rest. + induction str'. + { constructor; set_solver. } + { simpl. + econstructor; [ | eapply IHstr' ]. + { constructor. + { intros. exists (str' ++ rest)%bs. + inversion H; subst. + have->: (BS.String b str' ++ rest = BS.String b (str' ++ rest))%bs by done. + constructor. } + { inversion 1; subst. + eexists _; split. set_solver. + constructor. } } } +Qed. From 1dda8d71fc95e15333ad29d95aa1bc62e2f8050d Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Fri, 1 May 2026 08:17:01 -0400 Subject: [PATCH 09/13] Fix iostream spec --- rocq-brick-libstdcpp/proof/iostream/spec.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/iostream/spec.v b/rocq-brick-libstdcpp/proof/iostream/spec.v index f623731..e0228f5 100644 --- a/rocq-brick-libstdcpp/proof/iostream/spec.v +++ b/rocq-brick-libstdcpp/proof/iostream/spec.v @@ -106,7 +106,8 @@ Module ostream. cpp.spec "std::endl>(std::basic_ostream>&)" from source as endl_spec with ( - \exact Reduce iostream_manip_spec "\n"%bs + \exact Reduce iostream_manip_spec " +"%bs ). (* This is the overload taking the endl manipulator. *) @@ -117,7 +118,7 @@ Module ostream. \arg{os_f} "" (Vptr os_f) \pre{spec} os_f |-> unmaterialized_specR iostream_manip_kind spec (* ^^ this would be *slightly* more general if it took a materialized specification *) - \pre{Q} (spec [Vref this] (fun v => [| v = Vvoid |] ** Q)) + \pre{Q} (spec [Vref this] (fun v => [| v = Vptr this |] ** Q)) \post[Vptr this] Q ). From 6d28ca42340c667ec7a658619b37f1f3170ea8ca Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Fri, 1 May 2026 08:17:13 -0400 Subject: [PATCH 10/13] Verify the [_swap_a] files --- .../test/geeks_for_geeks_examples/N4_sum_a.v | 54 ++++++- .../test/geeks_for_geeks_examples/N5_swap.v | 145 +++++++++++++++--- .../test/geeks_for_geeks_examples/N5_swap_a.v | 5 +- 3 files changed, 173 insertions(+), 31 deletions(-) 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 index 0ec0bc3..aa428db 100644 --- 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 @@ -1,19 +1,63 @@ Require Import skylabs.auto.cpp.prelude.proof. Require Import skylabs.brick.libstdcpp.iostream.spec. +Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.prelude. + Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.N4_sum_a_cpp. Import linearity. +#[local] Open Scope Z_scope. + +Definition output_app (init : bs -> Prop) : LTS output_event := + {| Sts._state := bs + ; Sts._init_state := init + ; Sts._step := only_output |}. + + Section with_cpp. Context `{Σ : cpp_logic, σ : genv}. + Context `{SPECTRA : !appG (output_app (eq $ ostream.format_int 20)) _Σ}. + + #[program] + Instance Sum : App.app := + {| App.evt := output_event + ; App.lts := output_app (eq $ ostream.format_int 20) + ; App.inG := _ + |}. + Next Obligation. + unshelve eapply mpred_prop.mpred_has_usual_own. apply SPECTRA. + Defined. + + #[program] + Definition OS (E : coPset) γ : Ostream := + {| do evt K := Step.requester Sum E γ evt K |}%I. + Next Obligation. repeat intro. apply requester_ne; done. Qed. + + Definition X := Step.requester Sum. + #[local] Hint Resolve X : sl_opacity. + + #[program] + Definition bs_dos_steps_C (s : bs) (s' : propset (Sts._state (App.lts Sum))) str + (ANY_STEPS : AnySteps only_output {[s]} ((fun x => Write x) <$> BS.string_to_bytes str) s') := + \cancelx + \using{γ} AuthSet.frag γ {[s]} + \proving{K : mpredI} ostream.bs_dos (OS:=OS ⊤ γ) str K + \through (AuthSet.frag γ s' -∗ K) + \end@{mpredI}. + Next Obligation. + simpl. + intros. + iIntros "F" (?) "K". + rewrite /Step.requester. + Admitted. + Hint Resolve bs_dos_steps_C : sl_opacity. 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) - ). + \prepost{γ osM} _global "std::cout" |-> ostream.R (OS ⊤ γ) osM 1$m + \pre AuthSet.frag γ {[ ostream.format_int 20 ]} + \post[Vint 0] AuthSet.frag γ {[ ""%bs ]}). + Lemma main_ok : verify[source] main_spec. Proof. 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 index c9177ba..c145388 100644 --- a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap.v +++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap.v @@ -1,40 +1,139 @@ -Require Import skylabs.auto.cpp.prelude.proof. -Require Import skylabs.brick.libstdcpp.iostream.spec. - +Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.prelude. Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.N5_swap_cpp. Import linearity. +Definition output_app (init : bs -> Prop) : LTS output_event := + {| Sts._state := bs + ; Sts._init_state := init + ; Sts._step := only_output |}. + +Definition behavior (a b : Z) : bs := + "Before swapping a = " ++ + ostream.format_int a ++ " , b = " ++ ostream.format_int b ++ "\n" ++ + "After swapping a = " ++ ostream.format_int b ++ " , b = " ++ ostream.format_int a ++ "\n". + + Section with_cpp. Context `{Σ : cpp_logic, σ : genv}. + Context `{SPECTRA : !appG (output_app (eq $ behavior 2 3)) _Σ}. + + #[program] + Instance Swap : App.app := + {| App.evt := output_event + ; App.lts := output_app (eq $ behavior 2 3) + ; App.inG := _ + |}. + Next Obligation. + unshelve eapply mpred_prop.mpred_has_usual_own. apply SPECTRA. + Defined. + + #[program] + Definition OS (E : coPset) γ : Ostream := + {| do evt K := Step.requester Swap E γ evt K |}%I. + Next Obligation. repeat intro. apply requester_ne; done. Qed. - Inductive only_output : bs -> output_event -> bs -> Prop := - | output_char c {b : bs} : only_output (BS.String c b) (Write c) b. - Require Import skylabs.iris.extra.base_logic.lib.spectra. + Definition X := Step.requester Swap. + #[local] Hint Resolve X : sl_opacity. - Definition behavior (a b : Z) : bs := - "Before swapping a = " ++ - Z_to_string a ++ " , b = " ++ Z_to_string b ++ "\n" ++ - "After swapping a = " ++ Z_to_string b ++ " , b = " ++ Z_to_string a ++ "\n". + #[program] + Definition bs_dos_steps_C (s : bs) (s' : propset (Sts._state (App.lts Swap))) str + (ANY_STEPS : AnySteps only_output {[s]} ((fun x => Write x) <$> BS.string_to_bytes str) s') := + \cancelx + \using{γ} AuthSet.frag γ {[s]} + \proving{K : mpredI} ostream.bs_dos (OS:=OS ⊤ γ) str K + \through (AuthSet.frag γ s' -∗ K) + \end@{mpredI}. + Next Obligation. + simpl. + intros. + iIntros "F" (?) "K". + rewrite /Step.requester. + Admitted. + Hint Resolve bs_dos_steps_C : sl_opacity. cpp.spec "main()" from source as main_spec with ( - \prepost{osM} _global "std::cout" |-> ostream.R 1$m osM - \pre AuthSet.frag γ {[ behavior 3 2 ]} - \pre{str} _global "std::cout" |-> ostream_contentR 1$m str - \post[Vint 0] - _global "std::cout" |-> ostream_contentR 1$m ** - AuthSet.frag γ {[ ""%bs ]} - ). + \prepost{γ osM} _global "std::cout" |-> ostream.R (OS ⊤ γ) osM 1$m + \pre AuthSet.frag γ {[ behavior 2 3 ]} + \post[Vint 0] AuthSet.frag γ {[ ""%bs ]}). + + #[program] + Definition pick_ex {PROP:bi}:= + \cancelx + \bound_existential Q + \proving{P} (P -∗ Q) + \instantiate Q := P + \end@{PROP}. + Next Obligation. + intros. + iIntros "_" (??? ->). iIntros "$". + Qed. + #[local] Hint Resolve pick_ex : sl_opacity. + + #[global] + Instance as_sep_L_proper_frame {TT : tele} {P Q} + : kont.AsSep P -> + kont.ProperFrame (fun K : TT -t> mpred => P K ∗ Q)%I. + Proof. + destruct 1. constructor. + iIntros (??) "K [P $]". + rewrite !_as_sep. + iDestruct "P" as (?) "[A B]". + iExists _; iFrame "B". iApply "K"; iApply "A". + Qed. + + #[global] + Instance as_sep_R_proper_frame {TT : tele} {P Q} + : kont.AsSep Q -> + kont.ProperFrame (fun K : TT -t> mpred => P ∗ Q K)%I. + Proof. + destruct 1. constructor. + iIntros (??) "K [P $]". + rewrite !_as_sep. + iDestruct "P" as (?) "[A B]". + iExists _; iFrame "B". iApply "K"; iApply "A". + Admitted. + + #[global] + Instance hack_proper_frame {PROP:bi} {P} + : kont.ProperFrame (PROP:=PROP) (T:=[tele]) (bi_sep P)%I. + Proof. + clear. + constructor; simpl. + iIntros (??) "K [$ P]". + iApply ("K" $! ()). done. + Qed. + + #[program] + Definition spec_lookup_c {fn iSpec} := + \cancelx + \preserving{P (_ : find_spec.FindSpec _ false (_global fn) P iSpec)} □ P + \proving{spec} _global fn |-> cptrR spec + \through [| spec = iSpec |] + \end. + Next Obligation. + intros. + iIntros "#P" (??); subst. + destruct H. + iDestruct (_spec_ok with "P") as "#$". + Qed. + Hint Resolve spec_lookup_c : sl_opacity. + + (* TODO: upstream *) + #[global] + Instance of_unmaterialized_refine1 {ty s s'}: + Refine1 false true (unmaterialized_fspec ty s = unmaterialized_fspec ty s') + [ s = s' ]. + Proof. + constructor; simpl; auto. + inversion 1; subst; done. + Qed. Lemma main_ok : verify[source] "main()". Proof. + #[local] Opaque ostream.bs_dos. 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). + iModIntro; go. Qed. End with_cpp. 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 index 8c9e44c..97edad0 100644 --- 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 @@ -1,6 +1,5 @@ -Require Import skylabs.auto.cpp.prelude.proof. -Require Import skylabs.brick.libstdcpp.iostream.spec. - +Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.prelude. +Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.N5_swap. Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.N5_swap_a_cpp. Import linearity. From aad71cec7c775e066b77f9f9fe4ad8e6a348ba20 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Fri, 1 May 2026 14:19:06 -0400 Subject: [PATCH 11/13] Ported all of the examples --- .../test/geeks_for_geeks_examples/N12_area.v | 63 +++++++--- .../geeks_for_geeks_examples/N1_hello_world.v | 27 ++-- .../test/geeks_for_geeks_examples/N4_sum.v | 50 ++++---- .../test/geeks_for_geeks_examples/N5_swap.v | 104 ++-------------- .../test/geeks_for_geeks_examples/N5_swap_a.v | 50 +++++--- .../N6_print_sizeof.v | 59 ++++++--- .../test/geeks_for_geeks_examples/prelude.v | 117 +++++++++++++++++- 7 files changed, 283 insertions(+), 187 deletions(-) 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 index b1b7dc5..2719d49 100644 --- a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N12_area.v +++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N12_area.v @@ -1,37 +1,72 @@ -Require Import skylabs.auto.cpp.prelude.proof. -Require Import skylabs.brick.libstdcpp.iostream.spec. - +Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.prelude. Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.N12_area_cpp. Import linearity. +#[local] Open Scope Z_scope. + +Definition area_of_rectangle (side1 side2 : Z) := side1 * side2. +Definition perimeter_of_rectangle (side1 side2 : Z) := 2 * (side1 + side2). + +Definition behavior (side1 side2 : Z) : bs := + let newline : bs := " +"%bs in + "Area = " ++ ostream.format_int (area_of_rectangle side1 side2) ++ newline ++ "Perimeter = " ++ ostream.format_int (perimeter_of_rectangle side1 side2). + 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. + #[local] Notation APP := (output_app (eq $ behavior side1 side2)). + + Context `{SPECTRA : !appG APP _Σ}. + + #[local] Instance Area : App.app := mkApp APP. + (* NOTE: Specializing this hint is necessary due to + the current Spectra packaging *) + Definition X := Step.requester Area. + #[local] Hint Resolve X : sl_opacity. + + (* NOTE: generalizing this over an [App.app] is difficult because [App.app] hides + the event signature. *) + #[program] + Definition OS (E : coPset) γ : Ostream := + {| do evt K := Step.requester Area E γ evt K |}%I. + Next Obligation. intros. repeat intro. by apply requester_ne. Qed. + + #[program] + Definition bs_dos_steps_C (s : bs) (s' : propset (Sts._state (App.lts Area))) str + (ANY_STEPS : AnySteps only_output {[s]} ((fun x => Write x) <$> BS.string_to_bytes str) s') := + \cancelx + \using{γ} AuthSet.frag γ {[s]} + \proving{K : mpredI} ostream.bs_dos (OS:=OS ⊤ γ) str K + \through (AuthSet.frag γ s' -∗ K) + \end@{mpredI}. + Next Obligation. + simpl. + intros. + iIntros "F" (?) "K". + rewrite /Step.requester. + Admitted. + Hint Resolve bs_dos_steps_C : sl_opacity. + + 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)) - ). + \prepost{γ osM} _global "std::cout" |-> ostream.R (OS ⊤ γ) osM 1$m + \pre AuthSet.frag γ {[ behavior side1 side2 ]} + \post[Vint 0] AuthSet.frag γ {[ ""%bs ]}). cpp.spec "areaRectangle(int, int)" from source inline. cpp.spec "perimeterRectangle(int, int)" from source inline. Lemma main_ok : verify[source] "main()". Proof. + #[local] Opaque ostream.bs_dos. 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.v b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N1_hello_world.v index fb0a7f2..f1638e3 100644 --- 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 @@ -9,28 +9,19 @@ Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.N1_hello_wo Import linearity. -Definition output_app (init : bs -> Prop) : LTS output_event := - {| Sts._state := bs - ; Sts._init_state := init - ; Sts._step := only_output |}. - Section with_cpp. Context `{Σ : cpp_logic, σ : genv}. - (* TODO: upstream this *) + #[local] Notation APP := (output_app (eq "Hello World"%bs)). - Context `{SPECTRA : !appG (output_app (eq "Hello World"%bs)) _Σ}. + Context `{SPECTRA : !appG APP _Σ}. - #[program] - Instance HelloWorld : App.app := - {| App.evt := output_event - ; App.lts := output_app (eq "Hello World"%bs) - ; App.inG := _ - |}. - Next Obligation. - unshelve eapply mpred_prop.mpred_has_usual_own. apply SPECTRA. - Defined. + #[local] Instance HelloWorld : App.app := mkApp APP. + Definition X := requester_C HelloWorld. + Hint Resolve X : sl_opacity. + (* NOTE: generalizing this over an [App.app] is difficult because [App.app] hides + the event signature. *) #[program] Definition OS (E : coPset) γ : Ostream := {| do evt K := Step.requester HelloWorld E γ evt K |}%I. @@ -41,10 +32,6 @@ Section with_cpp. \pre AuthSet.frag γ {[ "Hello World"%bs ]} \post[Vint 0] AuthSet.frag γ {[ ""%bs ]}). - Import kont. - - Definition X := requester_C HelloWorld. - Hint Resolve X : sl_opacity. Lemma main_ok : verify[source] "main()". Proof. verify_shift; go. banish_string_literals. iModIntro; go. Qed. 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 index 6b651e1..8330a35 100644 --- a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N4_sum.v +++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N4_sum.v @@ -3,47 +3,45 @@ Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.N4_sum_cpp. Import linearity. -Definition output_app (init : bs -> Prop) : LTS output_event := - {| Sts._state := bs - ; Sts._init_state := init - ; Sts._step := only_output |}. - - Section with_cpp. Context `{Σ : cpp_logic, σ : genv}. - Context `{SPECTRA : !appG (output_app (eq $ ostream.format_int 20)) _Σ}. - #[program] - Instance Sum : App.app := - {| App.evt := output_event - ; App.lts := output_app (eq $ ostream.format_int 20) - ; App.inG := _ - |}. - Next Obligation. - unshelve eapply mpred_prop.mpred_has_usual_own. apply SPECTRA. - Defined. + #[local] Notation APP := (output_app (eq $ ostream.format_int 20)). + + Context `{SPECTRA : !appG APP _Σ}. + + #[local] Instance Sum : App.app := mkApp APP. + (* NOTE: Specializing this hint is necessary due to + the current Spectra packaging *) + Definition X := Step.requester Sum. + #[local] Hint Resolve X : sl_opacity. + #[program] Definition OS (E : coPset) γ : Ostream := {| do evt K := Step.requester Sum E γ evt K |}%I. Next Obligation. repeat intro. apply requester_ne; done. Qed. - Definition X := Step.requester Sum. - #[local] Hint Resolve X : sl_opacity. - #[program] - Definition bs_dos_steps_C (s : bs) (s' : propset (Sts._state (App.lts Sum))) str - (ANY_STEPS : AnySteps only_output {[s]} ((fun x => Write x) <$> BS.string_to_bytes str) s') := + Definition bs_dos_steps_C str (s s' : propset (Sts._state (App.lts Sum))) + (ANY_STEPS : AnySteps only_output s ((fun x => Write x) <$> BS.string_to_bytes str) s') := \cancelx - \using{γ} AuthSet.frag γ {[s]} + \using{γ} AuthSet.frag γ s \proving{K : mpredI} ostream.bs_dos (OS:=OS ⊤ γ) str K \through (AuthSet.frag γ s' -∗ K) \end@{mpredI}. Next Obligation. - simpl. - intros. - iIntros "F" (?) "K". - rewrite /Step.requester. + simpl. clear. + intros str s s' ANY_STEP. + remember ((fun x => Write x) <$> BS.string_to_bytes str) as X. + generalize dependent str. + induction ANY_STEP; simpl. + { destruct str; simpl; try congruence. + intros. admit. } + { destruct str; simpl; try congruence. + inversion 1; subst; intros. admit. + } + { admit. } Admitted. Hint Resolve bs_dos_steps_C : sl_opacity. 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 index c145388..33d19b5 100644 --- a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap.v +++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N5_swap.v @@ -3,39 +3,29 @@ Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.N5_swap_cpp Import linearity. -Definition output_app (init : bs -> Prop) : LTS output_event := - {| Sts._state := bs - ; Sts._init_state := init - ; Sts._step := only_output |}. - Definition behavior (a b : Z) : bs := + let newline : bs := " +"%bs in "Before swapping a = " ++ - ostream.format_int a ++ " , b = " ++ ostream.format_int b ++ "\n" ++ - "After swapping a = " ++ ostream.format_int b ++ " , b = " ++ ostream.format_int a ++ "\n". - + ostream.format_int a ++ " , b = " ++ ostream.format_int b ++ newline ++ + "After swapping a = " ++ ostream.format_int b ++ " , b = " ++ ostream.format_int a ++ newline. Section with_cpp. Context `{Σ : cpp_logic, σ : genv}. - Context `{SPECTRA : !appG (output_app (eq $ behavior 2 3)) _Σ}. - #[program] - Instance Swap : App.app := - {| App.evt := output_event - ; App.lts := output_app (eq $ behavior 2 3) - ; App.inG := _ - |}. - Next Obligation. - unshelve eapply mpred_prop.mpred_has_usual_own. apply SPECTRA. - Defined. + #[local] Notation APP := (output_app (eq $ behavior 2 3)). + + Context `{SPECTRA : !appG APP _Σ}. + + #[local] Instance Swap : App.app := mkApp APP. + Definition X := requester_C Swap. + Hint Resolve X : sl_opacity. #[program] Definition OS (E : coPset) γ : Ostream := {| do evt K := Step.requester Swap E γ evt K |}%I. Next Obligation. repeat intro. apply requester_ne; done. Qed. - Definition X := Step.requester Swap. - #[local] Hint Resolve X : sl_opacity. - #[program] Definition bs_dos_steps_C (s : bs) (s' : propset (Sts._state (App.lts Swap))) str (ANY_STEPS : AnySteps only_output {[s]} ((fun x => Write x) <$> BS.string_to_bytes str) s') := @@ -57,78 +47,6 @@ Section with_cpp. \pre AuthSet.frag γ {[ behavior 2 3 ]} \post[Vint 0] AuthSet.frag γ {[ ""%bs ]}). - #[program] - Definition pick_ex {PROP:bi}:= - \cancelx - \bound_existential Q - \proving{P} (P -∗ Q) - \instantiate Q := P - \end@{PROP}. - Next Obligation. - intros. - iIntros "_" (??? ->). iIntros "$". - Qed. - #[local] Hint Resolve pick_ex : sl_opacity. - - #[global] - Instance as_sep_L_proper_frame {TT : tele} {P Q} - : kont.AsSep P -> - kont.ProperFrame (fun K : TT -t> mpred => P K ∗ Q)%I. - Proof. - destruct 1. constructor. - iIntros (??) "K [P $]". - rewrite !_as_sep. - iDestruct "P" as (?) "[A B]". - iExists _; iFrame "B". iApply "K"; iApply "A". - Qed. - - #[global] - Instance as_sep_R_proper_frame {TT : tele} {P Q} - : kont.AsSep Q -> - kont.ProperFrame (fun K : TT -t> mpred => P ∗ Q K)%I. - Proof. - destruct 1. constructor. - iIntros (??) "K [P $]". - rewrite !_as_sep. - iDestruct "P" as (?) "[A B]". - iExists _; iFrame "B". iApply "K"; iApply "A". - Admitted. - - #[global] - Instance hack_proper_frame {PROP:bi} {P} - : kont.ProperFrame (PROP:=PROP) (T:=[tele]) (bi_sep P)%I. - Proof. - clear. - constructor; simpl. - iIntros (??) "K [$ P]". - iApply ("K" $! ()). done. - Qed. - - #[program] - Definition spec_lookup_c {fn iSpec} := - \cancelx - \preserving{P (_ : find_spec.FindSpec _ false (_global fn) P iSpec)} □ P - \proving{spec} _global fn |-> cptrR spec - \through [| spec = iSpec |] - \end. - Next Obligation. - intros. - iIntros "#P" (??); subst. - destruct H. - iDestruct (_spec_ok with "P") as "#$". - Qed. - Hint Resolve spec_lookup_c : sl_opacity. - - (* TODO: upstream *) - #[global] - Instance of_unmaterialized_refine1 {ty s s'}: - Refine1 false true (unmaterialized_fspec ty s = unmaterialized_fspec ty s') - [ s = s' ]. - Proof. - constructor; simpl; auto. - inversion 1; subst; done. - Qed. - Lemma main_ok : verify[source] "main()". Proof. #[local] Opaque ostream.bs_dos. 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 index 97edad0..e0b13c5 100644 --- 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 @@ -7,28 +7,50 @@ Import linearity. Section with_cpp. Context `{Σ : cpp_logic, σ : genv}. + #[local] Notation APP := (output_app (eq $ behavior 2 3)). + + Context `{SPECTRA : !appG APP _Σ}. + + #[local] Instance Swap : App.app := mkApp APP. + Definition X := requester_C Swap. + Hint Resolve X : sl_opacity. + + #[program] + Definition OS (E : coPset) γ : Ostream := + {| do evt K := Step.requester Swap E γ evt K |}%I. + Next Obligation. repeat intro. apply requester_ne; done. Qed. + + 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" - ) - ). + \prepost{γ osM} _global "std::cout" |-> ostream.R (OS ⊤ γ) osM 1$m + \pre AuthSet.frag γ {[ behavior 2 3 ]} + \post[Vint 0] AuthSet.frag γ {[ ""%bs ]}). + + #[program] + Definition bs_dos_steps_C (s : bs) (s' : propset (Sts._state (App.lts Swap))) str + (ANY_STEPS : AnySteps only_output {[s]} ((fun x => Write x) <$> BS.string_to_bytes str) s') := + \cancelx + \using{γ} AuthSet.frag γ {[s]} + \proving{K : mpredI} ostream.bs_dos (OS:=OS ⊤ γ) str K + \through (AuthSet.frag γ s' -∗ K) + \end@{mpredI}. + Next Obligation. + simpl. + intros. + iIntros "F" (?) "K". + rewrite /Step.requester. + Admitted. + Hint Resolve bs_dos_steps_C : sl_opacity. + Lemma main_ok : verify[source] "main()". Proof. + (* TODO: this should be made more robust to not require this annotation *) + #[local] Opaque ostream.bs_dos. 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.v b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N6_print_sizeof.v index e4b6f57..3448b6f 100644 --- 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 @@ -1,35 +1,60 @@ -Require Import skylabs.auto.cpp.prelude.proof. -Require Import skylabs.brick.libstdcpp.iostream.spec. - +Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.prelude. Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.N6_print_sizeof_cpp. Import linearity. +Definition newline := " +"%bs. + +Definition behavior : bs := + "Size of int is: " ++ ostream.format_int 4 ++ newline ++ + "Size of char is: " ++ ostream.format_int 1 ++ newline ++ + "Size of float is: " ++ ostream.format_int 4 ++ newline ++ + "Size of double is: " ++ ostream.format_int 8 ++ newline. + Section with_cpp. Context `{Σ : cpp_logic, σ : genv}. - Definition newline := " -"%bs. + #[local] Notation APP := (output_app (eq behavior)). + + Context `{SPECTRA : !appG APP _Σ}. + + #[local] Instance SizeOf : App.app := mkApp APP. + Definition X := requester_C SizeOf. + Hint Resolve X : sl_opacity. + + #[program] + Definition OS (E : coPset) γ : Ostream := + {| do evt K := Step.requester SizeOf E γ evt K |}%I. + Next Obligation. repeat intro. apply requester_ne; done. Qed. + + #[program] + Definition bs_dos_steps_C (s : bs) (s' : propset (Sts._state (App.lts SizeOf))) str + (ANY_STEPS : AnySteps only_output {[s]} ((fun x => Write x) <$> BS.string_to_bytes str) s') := + \cancelx + \using{γ} AuthSet.frag γ {[s]} + \proving{K : mpredI} ostream.bs_dos (OS:=OS ⊤ γ) str K + \through (AuthSet.frag γ s' -∗ K) + \end@{mpredI}. + Next Obligation. + simpl. + intros. + iIntros "F" (?) "K". + rewrite /Step.requester. + Admitted. + Hint Resolve bs_dos_steps_C : sl_opacity. 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) - ). + \prepost{γ osM} _global "std::cout" |-> ostream.R (OS ⊤ γ) osM 1$m + \pre AuthSet.frag γ {[ behavior ]} + \post[Vint 0] AuthSet.frag γ {[ ""%bs ]}). Lemma main_ok : verify[source] "main()". Proof. + #[local] Opaque ostream.bs_dos. 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/prelude.v b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/prelude.v index 01d578f..c0274ef 100644 --- a/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/prelude.v +++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/prelude.v @@ -4,8 +4,24 @@ Require Export skylabs.brick.libstdcpp.iostream.spec. Require Export skylabs.iris.extra.base_logic.lib.spectra. (* BEGIN UPSTREAM *) -Definition appG {evt : Type} (lts : LTS evt) (Σ : gFunctors) : Type := - inG Σ (auth_setR (lts_state lts)). + +(* FOR SPECTRA definition *) +Class appG {evt : Type} (lts : LTS evt) (Σ : gFunctors) : Type := +{ _has_auth_set_state : inG Σ (auth_setR (lts_state lts)) }. + +Section to_spectra. + Context `{Σ : cpp_logic}. + + #[program] + Definition mkApp {event} (APP : LTS event) {SPECTRA : appG APP _Σ} : App.app := + {| App.evt := event + ; App.lts := APP + ; App.inG := _ + |}. + Next Obligation. + intros. unshelve eapply mpred_prop.mpred_has_usual_own. apply SPECTRA. + Defined. +End to_spectra. Section to_tele. Lemma tele_snoc_arg_snoc {TT T} (x : tele_snoc TT T) : exists ys y, @@ -27,7 +43,41 @@ Section to_tele. Qed. End to_tele. -(* FOR SPECTRA *) +Section to_auto. + Context {PROP : bi}. + #[program] + Definition pick_ex_C {PROP:bi}:= + \cancelx + \bound_existential Q + \proving{P} (P -∗ Q) + \instantiate Q := P + \end@{PROP}. + Next Obligation. + intros. + iIntros "_" (??? ->). iIntros "$". + Qed. +End to_auto. +#[global] Hint Resolve pick_ex_C | 200 : sl_opacity. + +Section to_cpp_auto. + Context `{Σ : cpp_logic} {σ : genv}. + #[program] + Definition spec_lookup_C {fn iSpec} := + \cancelx + \preserving{P (_ : find_spec.FindSpec _ false (_global fn) P iSpec)} □ P + \proving{spec} _global fn |-> cptrR spec + \through [| spec = iSpec |] + \end. + Next Obligation. + intros. + iIntros "#P" (??); subst. + destruct H. + iDestruct (_spec_ok with "P") as "#$". + Qed. +End to_cpp_auto. +#[global] Hint Resolve spec_lookup_C | 200 : sl_opacity. + +(* FOR SPECTRA automation *) Section operational. Context {T E} (step : T -> option E -> T -> Prop). @@ -146,8 +196,64 @@ Section to_spectra. by setoid_rewrite H. Qed. + (* NOTE: generalizing this over an [App.app] is difficult because [App.app] hides + the event signature. *) + #[program] + Definition OS (APP: App.app) (E : coPset) γ : SepHandler PROP (App.evt APP) := + {| do evt K := Step.requester APP E γ evt K |}%I. + End to_spectra. #[global] Hint Resolve frag_frag_exact_B frag_frag_exact_F : sl_opacity. + +#[global] +Instance of_unmaterialized_refine1 `{Σ : cpp_logic} {σ : genv} {ty s s'}: + Refine1 false true (unmaterialized_fspec ty s = unmaterialized_fspec ty s') + [ s = s' ]. +Proof. + constructor; simpl; auto. + inversion 1; subst; done. +Qed. + +Section to_kont. + Context {PROP : bi}. + #[global] + Instance as_sep_L_proper_frame {TT : tele} {P Q} + : kont.AsSep P -> + kont.ProperFrame (fun K : TT -t> PROP => P K ∗ Q)%I. + Proof. + destruct 1. constructor. + iIntros (??) "K [P $]". + rewrite !_as_sep. + iDestruct "P" as (?) "[A B]". + iExists _; iFrame "B". iApply "K"; iApply "A". + Qed. + + #[global] + Instance as_sep_R_proper_frame {TT : tele} {P Q} + : kont.AsSep Q -> + kont.ProperFrame (fun K : TT -t> PROP => P ∗ Q K)%I. + Proof. + destruct 1. constructor. + iIntros (??) "K [$ P]". + rewrite !_as_sep. + iDestruct "P" as (?) "[A B]". + iExists _; iFrame "B". iApply "K"; iApply "A". + Qed. + + (* this instance is a bit of a bug when happen to end up + finding [fun K => P ∗ K], then this can be eta-contracted to + [bi_sep P]. + *) + #[global] + Instance hack_proper_frame {P} + : kont.ProperFrame (PROP:=PROP) (T:=[tele]) (bi_sep P)%I. + Proof. + clear. + constructor; simpl. + iIntros (??) "K [$ P]". + iApply ("K" $! ()). done. + Qed. +End to_kont. (* END UPSTREAM *) @@ -211,3 +317,8 @@ Proof. eexists _; split. set_solver. constructor. } } } Qed. + +Definition output_app (init : bs -> Prop) : LTS output_event := + {| Sts._state := bs + ; Sts._init_state := init + ; Sts._step := only_output |}. From 0308df52c23e8300167241f4a888d4ac38ddfc04 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Fri, 1 May 2026 14:26:42 -0400 Subject: [PATCH 12/13] Re-organization --- rocq-brick-libstdcpp/proof/iostream/itree.v | 68 --------------------- rocq-brick-libstdcpp/proof/iostream/spec.v | 62 +++++++++++++++++++ 2 files changed, 62 insertions(+), 68 deletions(-) diff --git a/rocq-brick-libstdcpp/proof/iostream/itree.v b/rocq-brick-libstdcpp/proof/iostream/itree.v index e0e4b77..3c69324 100644 --- a/rocq-brick-libstdcpp/proof/iostream/itree.v +++ b/rocq-brick-libstdcpp/proof/iostream/itree.v @@ -16,74 +16,7 @@ Section with_E. End with_E. -Require Import stdpp.numbers. - -Variant input_char : Type -> Type := - | read : input_char N. - Require Import stdpp.base. -Require Import stdpp.numbers. - -(** [is_ws] returns true if the character is a standard whitespace. - Uses stdpp's bool_decide to evaluate the logical disjunction. *) -Definition is_ws (c : N) : bool := - bool_decide (c = 32 \/ c = 10 \/ c = 13 \/ c = 9)%N. - -(** [as_digit] returns [Some d] if the character is between '0' and '9'. - Uses stdpp's bool_decide to evaluate the logical conjunction. *) -Definition as_digit (c : N) : option N := - if bool_decide (48 <= c /\ c <= 57)%N then - Some (c - 48)%N - else - None. - -(** [read_int] reads characters using [Do read] and parses - the string as an integer. For example, the characters - <1>, <2>, <\n> would return <('\n', 12)>. - - The function accepts both positive and negative integers. - - The first component is the "overread", the first byte read that - is not part of the number. - *) -CoFixpoint read_int : itree input_char (N * Z) := - (* Internal state machine to accumulate parsed digits *) - let cofix loop (sign : Z) (acc : Z) : itree input_char (N * Z) := - Do read (fun c => - match as_digit c with - | Some digit => - loop sign (acc * 10 + Z.of_N digit)%Z - | None => - (* Not a digit: return the delimiter character and the final signed integer *) - Ret (c, (sign * acc)%Z) - end - ) - in - - Do read (fun c => - if (c =? 45)%N then - (* Encountered '-' (ASCII 45) -> Start reading negative number *) - loop (-1)%Z 0%Z - - else if (c =? 43)%N then - (* Encountered '+' (ASCII 43) -> Start reading positive number *) - loop 1%Z 0%Z - - else if is_ws c then - (* Whitespace (space, \n, \r, \t) -> Co-recursively skip *) - read_int - - else match as_digit c with - | Some digit => - (* Encountered a digit -> Start accumulating a positive number *) - loop 1%Z (Z.of_N digit) - | None => - (* Unexpected character before any digits -> Abort and return 0 *) - Ret (c, 0%Z) - end - ). - - Require Import skylabs.prelude.sts. Section as_lts. @@ -92,7 +25,6 @@ Section as_lts. Context {as_evt : forall {T}, E T -> T -> Evt}. - Variant itree_step : itree E unit -> option Evt -> itree E unit -> Prop := | step_do {T} {act : E T} (r : T) k : itree_step (Do act k) (Some $ as_evt _ act r) (k r) diff --git a/rocq-brick-libstdcpp/proof/iostream/spec.v b/rocq-brick-libstdcpp/proof/iostream/spec.v index e0228f5..f59399e 100644 --- a/rocq-brick-libstdcpp/proof/iostream/spec.v +++ b/rocq-brick-libstdcpp/proof/iostream/spec.v @@ -130,11 +130,73 @@ Module istream. Section with_cpp. Context `{Σ : cpp_logic, σ : genv}. + Variant input_char : Type -> Type := + | read : input_char N. + Definition as_event (T : Type) (act : input_char T) : T -> input_event := match act in input_char T return T -> _ with | read => fun n => Read n end. + (** [is_ws] returns true if the character is a standard whitespace. + Uses stdpp's bool_decide to evaluate the logical disjunction. *) + Definition is_ws (c : N) : bool := + bool_decide (c = 32 \/ c = 10 \/ c = 13 \/ c = 9)%N. + + (** [as_digit] returns [Some d] if the character is between '0' and '9'. + Uses stdpp's bool_decide to evaluate the logical conjunction. *) + Definition as_digit (c : N) : option N := + if bool_decide (48 <= c /\ c <= 57)%N then + Some (c - 48)%N + else + None. + + (** [read_int] reads characters using [Do read] and parses + the string as an integer. For example, the characters + <1>, <2>, <\n> would return <('\n', 12)>. + + The function accepts both positive and negative integers. + + The first component is the "overread", the first byte read that + is not part of the number. + *) + CoFixpoint read_int : itree input_char (N * Z) := + (* Internal state machine to accumulate parsed digits *) + let cofix loop (sign : Z) (acc : Z) : itree input_char (N * Z) := + Do read (fun c => + match as_digit c with + | Some digit => + loop sign (acc * 10 + Z.of_N digit)%Z + | None => + (* Not a digit: return the delimiter character and the final signed integer *) + Ret (c, (sign * acc)%Z) + end + ) + in + + Do read (fun c => + if (c =? 45)%N then + (* Encountered '-' (ASCII 45) -> Start reading negative number *) + loop (-1)%Z 0%Z + + else if (c =? 43)%N then + (* Encountered '+' (ASCII 43) -> Start reading positive number *) + loop 1%Z 0%Z + + else if is_ws c then + (* Whitespace (space, \n, \r, \t) -> Co-recursively skip *) + read_int + + else match as_digit c with + | Some digit => + (* Encountered a digit -> Start accumulating a positive number *) + loop 1%Z (Z.of_N digit) + | None => + (* Unexpected character before any digits -> Abort and return 0 *) + Ret (c, 0%Z) + end + ). + cpp.spec "std::basic_istream>::operator>>(int&)" from source as istream_take_int_spec with ( \this this From 76074821ad3811d8781ab45e65c54dcc17e89106 Mon Sep 17 00:00:00 2001 From: Gregory Malecha Date: Fri, 1 May 2026 14:39:43 -0400 Subject: [PATCH 13/13] Some notes about refinement --- rocq-brick-libstdcpp/proof/iostream/README.md | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 rocq-brick-libstdcpp/proof/iostream/README.md diff --git a/rocq-brick-libstdcpp/proof/iostream/README.md b/rocq-brick-libstdcpp/proof/iostream/README.md new file mode 100644 index 0000000..3fa565f --- /dev/null +++ b/rocq-brick-libstdcpp/proof/iostream/README.md @@ -0,0 +1,18 @@ +# `` + +This directory captures the behavior of the `` library using the refinement methodology +developed in the [Spectra](https://github.com/SkyLabsAI/BRiCk/blob/main/rocq-skylabs-iris/theories/base_logic/lib/spectra.md) library. + +At the high level, the behavior of a program is described by a labled transition system (LTS** and the +*current state* of the LTS is embedded in separation logic (in Spectra this is done using `AuthSet.frag`). +Interactions with the outside world are captured via updating this state through the use of requesters +and committers which allow updating this state by emitting appropriate events. + +## Adequacy + +See the Spectra docs for more information about establishing a formal refinement with this setup. + +## References + +- [Spectra](https://github.com/SkyLabsAI/BRiCk/blob/main/rocq-skylabs-iris/theories/base_logic/lib/spectra.md) +- [A Separation Logic for Refining Concurrent Objects](https://dl.acm.org/doi/10.1145/1926385.1926415)