A sketch of a refinement-based setup.

rocq-brick-libstdcpp/proof/iostream/README.md

@@ -0,0 +1,18 @@
+# `<iostream>`
+
+This directory captures the behavior of the `<iostream>` 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)

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

@@ -0,0 +1,38 @@
+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.base.
+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.

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

@@ -8,6 +8,10 @@ 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.itree.
+
 Require Import skylabs.brick.libstdcpp.iostream.inc_iostream_cpp.
 
 (** TODO upstream START *)
@@ -18,31 +22,101 @@ 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}.
+(** A handler for events as a predicate transformer.
+
+    Generally, this will be an <AU> that proves that <evt> is a valid next event.
+ *)
+Class SepHandler (PROP : bi) (evt : Type) : Type :=
+{ do : propset evt -> (evt -> PROP) -> PROP
+  (** This is effectively an <<AU>> 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
+    to be sent to the consumer on a [Flush].
+ *)
+Variant output_event : Set :=
+  | Write (_ : N).
+
+Variant input_event : Set :=
+  | Read (_ : N).
+
+(** 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 <iomanip> *)
+  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.
 
-  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.
+  End with_cpp.
+End ostream.
 
-  #[global] Instance: LearnEqF1 ostreamR := ltac:(solve_learnable).
-  #[global] Instance: LearnEqF1 ostream_contentR := ltac:(solve_learnable).
+Module istream.
+  Parameter gname : Set.
+  Parameter R : forall `{Σ : cpp_logic} {σ : genv}, Istream -> gname -> cQp.t -> Rep.
+  #[only(cfracsplittable)] derive R.
 
-  Parameter istreamT : Type.
-  Parameter istreamR : cQp.t -> istreamT -> Rep.
-  #[only(cfracsplittable)] derive istreamR.
-  #[global] Instance: LearnEqF1 istreamR := ltac:(solve_learnable).
+  Section with_cpp.
+    Context `{Σ : cpp_logic, σ : genv}.
 
-  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.
+    #[global] Instance: Cbn (Learn (learn_eq ==> learn_eq ==> any ==> learn_hints.fin) R).
+    Proof. solve_learnable. Qed.
 
-End with_cpp.
+  End with_cpp.
 
-#[export] Hint Resolve ostream_contentR_aggressiveC : br_hints.
+End istream.