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 @@
+# `<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)
diff --git a/rocq-brick-libstdcpp/proof/iostream/itree.v b/rocq-brick-libstdcpp/proof/iostream/itree.v
new file mode 100644
index 0000000..3c69324
--- /dev/null
+++ b/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.
diff --git a/rocq-brick-libstdcpp/proof/iostream/pred.v b/rocq-brick-libstdcpp/proof/iostream/pred.v
index 3f86ebf..de4cf94 100644
--- a/rocq-brick-libstdcpp/proof/iostream/pred.v
+++ b/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.
diff --git a/rocq-brick-libstdcpp/proof/iostream/spec.v b/rocq-brick-libstdcpp/proof/iostream/spec.v
index 3851fd6..f59399e 100644
--- a/rocq-brick-libstdcpp/proof/iostream/spec.v
+++ b/rocq-brick-libstdcpp/proof/iostream/spec.v
@@ -8,88 +8,208 @@ 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.
 
-Section with_cpp.
-  Context `{Σ : cpp_logic, σ : genv}.
-
-  cpp.spec "std::operator<<<std::char_traits<char>>(std::basic_ostream<char, std::char_traits<char>>&, const char*)" from source as ostream_insert_spec with (
-    \arg{osP} "" (Vptr osP)
-    \prepost{osM} osP |-> ostreamR 1$m osM
-    \pre{str} osP |-> ostream_contentR 1$m str
-    \arg{strP} "" (Vptr strP)
-    \prepost{q__s strM} strP |-> cstring.R q__s strM
-    \post[Vptr osP]
-      osP |-> ostream_contentR 1$m (str ++ strM)).
-
-  Parameter Z_to_string : Z -> cstring.t.
-  #[global] Declare Instance Z_to_string_inj : Inj eq eq Z_to_string.
-  (** TODO: find an implementation!*)
-
-  cpp.spec "std::basic_ostream<char, std::char_traits<char>>::operator<<(int)" from source as ostream_print_int_spec with (
-    \this this
-    \prepost{osM} this |-> ostreamR 1$m osM
-    \pre{str} this |-> ostream_contentR 1$m str
-    \arg{n} "" (Vint n)
-    \post[Vptr this]
-        this |-> ostream_contentR 1$m (str ++ Z_to_string n)
-  ).
-
-  cpp.spec "std::basic_ostream<char, std::char_traits<char>>::operator<<(unsigned long)" from source as ostream_print_ulong_spec with (
-    \this this
-    \prepost{osM} this |-> ostreamR 1$m osM
-    \pre{str} this |-> ostream_contentR 1$m str
-    \arg{n} "" (Vint n)
-    \post[Vptr this]
-        this |-> ostream_contentR 1$m (str ++ Z_to_string n)
-  ).
-
-  Definition iostream_manip_spec state_f contents_f : WpSpec_cpp_val := (
-    \arg{osP : ptr} "" (Vptr osP)
-    (* XXX: manipulators can modify [osM]! *)
-    \pre{osM} osP |-> ostreamR 1$m osM
-    \post* osP |-> ostreamR 1$m (state_f osM)
-    \pre{str} osP |-> ostream_contentR 1$m str
-    \post[Vptr osP] osP |-> ostream_contentR 1$m (contents_f str)).
-
-  Definition ostream_cpp_type : type :=
-    "std::basic_ostream<char, std::char_traits<char>>&".
-  Definition iostream_manip_kind : okind :=
-    tFunction ostream_cpp_type [ostream_cpp_type].
-
-  cpp.spec "std::endl<char, std::char_traits<char>>(std::basic_ostream<char, std::char_traits<char>>&)" from source as endl_spec with (
-    \exact Reduce iostream_manip_spec (fun osM => osM) (fun str => str ++ "\n")%bs
-  ).
-
-  (* This is the overload taking the endl manipulator. *)
-  (* https://eel.is/c++draft/output.streams#ostream.inserters *)
-  cpp.spec "std::basic_ostream<char, std::char_traits<char>>::operator<<(std::basic_ostream<char, std::char_traits<char>>&(*)(std::basic_ostream<char, std::char_traits<char>>&))"
-    from source as ostream_insert_string_spec with (
-    \this this
-    \arg{os_f} "" (Vptr os_f)
-    \pre{state_f stream_f}
-      os_f |-> unmaterialized_specR
-        iostream_manip_kind
-        (iostream_manip_spec state_f stream_f)
-    \pre{osM} this |-> ostreamR 1$m osM
-    \post* this |-> ostreamR 1$m (state_f osM)
-    \pre{str} this |-> ostream_contentR 1$m str
-    \post[Vptr this]
-      this |-> ostream_contentR 1$m (stream_f str)
-  ).
-
-  (** NOTE: this specification is weak because it does not connect to the
-      actual stream "contents". *)
-  cpp.spec "std::basic_istream<char, std::char_traits<char>>::operator>>(int&)"
-    from source as istream_take_int_spec with (
-    \this this
-    \pre{isM} this |-> istreamR 1$m isM
-    \arg{nP} "" (Vptr nP)
-    \pre nP |-> anyR "int" 1$m
-    \post[Vptr this] Exists isM' n,
-        this |-> istreamR 1$m isM' **
-          nP |-> intR 1$m n
-  ).
-
-End with_cpp.
+(*
+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 *)
+
+
+Module ostream.
+  Section with_cpp.
+    Context `{Σ : cpp_logic, σ : genv}.
+
+    Fixpoint bs_dos {OS : Ostream} (bs : bs) (K : mpred) : mpred :=
+      match bs with
+      | BS.EmptyString => 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_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 $ 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::char_traits<char>>(std::basic_ostream<char, std::char_traits<char>>&, const char*)"
+      from source as ostream_insert_spec with (
+      \arg{osP} "" (Vptr osP)
+      \prepost{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
+      \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<char, std::char_traits<char>>::operator<<(int)"
+      from source as ostream_print_int_spec with (
+      \this this
+      \arg{n} "" (Vint n)
+      \prepost{OS γ} this |-> ostream.R OS γ 1$m
+      \pre{Q} bs_dos (format_int n) Q
+      \post[Vptr this] Q
+    ).
+
+    cpp.spec "std::basic_ostream<char, std::char_traits<char>>::operator<<(unsigned long)"
+      from source as ostream_print_ulong_spec with (
+      \this this
+      \arg{n} "" (Vint n)
+      \prepost{OS γ} this |-> ostream.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 |-> ostream.R OS γ 1$m
+      \pre{Q} bs_dos contents_f Q
+      \post[Vptr osP] Q).
+
+    Definition ostream_cpp_type : type :=
+      "std::basic_ostream<char, std::char_traits<char>>&".
+    Definition iostream_manip_kind : okind :=
+      tFunction ostream_cpp_type [ostream_cpp_type].
+
+    cpp.spec "std::endl<char, std::char_traits<char>>(std::basic_ostream<char, std::char_traits<char>>&)"
+      from source as endl_spec with (
+      \exact Reduce iostream_manip_spec "
+"%bs
+    ).
+
+    (* This is the overload taking the endl manipulator. *)
+    (* https://eel.is/c++draft/output.streams#ostream.inserters *)
+    cpp.spec "std::basic_ostream<char, std::char_traits<char>>::operator<<(std::basic_ostream<char, std::char_traits<char>>&(*)(std::basic_ostream<char, std::char_traits<char>>&))"
+      from source as ostream_insert_string_spec with (
+      \this this
+      \arg{os_f} "" (Vptr os_f)
+      \pre{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 = Vptr this |] ** Q))
+      \post[Vptr this] Q
+    ).
+
+
+  End with_cpp.
+End ostream.
+
+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<char, std::char_traits<char>>::operator>>(int&)"
+      from source as istream_take_int_spec with (
+          \this this
+          \pre{IS isM} this |-> istream.R IS isM 1$m
+          \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 **
+              K n
+        ).
+
+  End with_cpp.
+
+End istream.
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 329fc3f..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
@@ -1,6 +1,10 @@
 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.prelude.
+
 Require Import skylabs.brick.libstdcpp.test.geeks_for_geeks_examples.N1_hello_world_cpp.
 
 Import linearity.
@@ -8,18 +12,28 @@ Import linearity.
 Section with_cpp.
   Context `{Σ : cpp_logic, σ : genv}.
 
+  #[local] Notation APP := (output_app (eq "Hello World"%bs)).
+
+  Context `{SPECTRA : !appG APP _Σ}.
+
+  #[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.
+  Next Obligation. intros. repeat intro. by apply requester_ne. 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 ++ "Hello World")).
+    \prepost{γ osM} _global "std::cout" |-> ostream.R (OS ⊤ γ) osM 1$m
+    \pre AuthSet.frag γ {[ "Hello World"%bs ]}
+    \post[Vint 0]  AuthSet.frag γ {[ ""%bs ]}).
+
 
   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/N4_sum.v b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/N4_sum.v
index ebed51a..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
@@ -1,6 +1,4 @@
-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.
@@ -8,13 +6,51 @@ Import linearity.
 Section with_cpp.
   Context `{Σ : cpp_logic, σ : genv}.
 
+  #[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.
+
+  #[program]
+  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
+    \proving{K : mpredI} ostream.bs_dos (OS:=OS ⊤ γ) str K
+    \through (AuthSet.frag γ s' -∗ K)
+    \end@{mpredI}.
+  Next Obligation.
+    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.
+
   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/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 e82bfcb..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
@@ -1,34 +1,57 @@
-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 behavior (a b : Z) : bs :=
+  let newline : bs := "
+"%bs in
+  "Before swapping a = " ++
+    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}.
 
+  #[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.
+
+  #[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" |-> 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 ]}).
 
   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..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
@@ -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.
@@ -8,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
new file mode 100644
index 0000000..c0274ef
--- /dev/null
+++ b/rocq-brick-libstdcpp/test/geeks_for_geeks_examples/prelude.v
@@ -0,0 +1,324 @@
+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 *)
+
+(* 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,
+      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.
+
+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).
+
+  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
+  | 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.
+
+End operational.
+Existing Class AnySteps.
+#[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.
+
+  #[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.
+
+  (* 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 *)
+
+
+(** 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 $ 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 $ 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.
+
+Definition output_app (init : bs -> Prop) : LTS output_event :=
+  {| Sts._state := bs
+   ; Sts._init_state := init
+   ; Sts._step := only_output |}.