make function a record so we can have projections; tweak notations

theories/lang/lang_base.v

@@ -285,8 +285,12 @@ Proof.
 Qed.
 
 (** Global static function table *)
-Inductive function :=
-| FunV (xl : list binder) (e : expr) `{Closed (xl +b+ []) e}.
+Record function := FunV {
+  fun_b: list binder;
+  fun_e: expr;
+  fun_closed: Closed (fun_b +b+ []) fun_e
+}.
+Arguments FunV _ _ {_}.
 Definition fn_env := gmap fn_id function.
 
 (** Main state: a heap of scalars. *)

theories/opt/ex1.v

-From stbor.sim Require Import local invariant refl_step tactics body.
+From stbor.sim Require Import local invariant refl_step tactics body simple.
 
 Set Default Proof Using "Type".
 
@@ -26,7 +26,7 @@ Definition ex1_opt : function :=
     "v"
   .
 
-Lemma ex1_sim_body fs ft : ⊨{fs,ft} ex1 ≥ᶠ ex1_opt.
+Lemma ex1_sim_body fs ft : ⊨ᶠ{fs,ft} ex1 ≥ ex1_opt.
 Proof.
   intros rf es et vls vlt σs σt FREL SUBSTs SUBSTt.
   destruct vls as [|vs []]; [done| |done].  simpl in SUBSTs.

theories/opt/ex1_down.v

@@ -23,7 +23,7 @@ Definition ex1_down_opt : function :=
     .
 
 
-Lemma ex1_down_sim_fun fs ft : ⊨{fs,ft} ex1_down ≥ᶠ ex1_down_opt.
+Lemma ex1_down_sim_fun fs ft : ⊨ᶠ{fs,ft} ex1_down ≥ ex1_down_opt.
 Proof.
   intros r es et vls vlt σs σt FREL SUBSTs SUBSTt.
   destruct vls as [|vs []]; [done| |done].  simpl in SUBSTs.

theories/opt/ex2.v

@@ -24,6 +24,6 @@ Definition ex2_opt : function :=
     "v"
   .
 
-Lemma ex2_sim_body fs ft : ⊨{fs,ft} ex2 ≥ᶠ ex2_opt.
+Lemma ex2_sim_body fs ft : ⊨ᶠ{fs,ft} ex2 ≥ ex2_opt.
 Proof.
 Abort.

theories/opt/ex2_down.v

@@ -23,7 +23,7 @@ Definition ex2_down_opt : function :=
     .
 
 
-Lemma ex2_down_sim_fun fs ft : ⊨{fs,ft} ex2_down ≥ᶠ ex2_down_opt.
+Lemma ex2_down_sim_fun fs ft : ⊨ᶠ{fs,ft} ex2_down ≥ ex2_down_opt.
 Proof.
   intros r es et vls vlt σs σt FREL SUBSTs SUBSTt.
   destruct vls as [|vs []]; [done| |done].  simpl in SUBSTs.

theories/opt/ex3.v

@@ -32,7 +32,7 @@ Definition ex3_opt_2 : function :=
     Call #[ScFnPtr "f"] []
   .
 
-Lemma ex3_sim_fun fs ft : ⊨{fs,ft} ex3 ≥ᶠ ex3_opt_1.
+Lemma ex3_sim_fun fs ft : ⊨ᶠ{fs,ft} ex3 ≥ ex3_opt_1.
 Proof.
   intros r es et vls vlt σs σt FREL SUBSTs SUBSTt.
   destruct vls as [|vs []]; [done| |done].  simpl in SUBSTs.

theories/opt/ex3_down.v

@@ -34,7 +34,7 @@ Definition ex3_down_opt_2 : function :=
     "v"
   .
 
-Lemma ex3_down_sim_fun fs ft : ⊨{fs,ft} ex3_down ≥ᶠ ex3_down_opt_1.
+Lemma ex3_down_sim_fun fs ft : ⊨ᶠ{fs,ft} ex3_down ≥ ex3_down_opt_1.
 Proof.
   intros r es et vls vlt σs σt FREL SUBSTs SUBSTt.
   destruct vls as [|vs []]; [done| |done].  simpl in SUBSTs.

theories/sim/instance.v

@@ -3,11 +3,11 @@ From stbor.sim Require Export local invariant.
 
 Notation "r ⊨{ n , fs , ft } ( es , σs ) ≥ ( et , σt ) : Φ" :=
   (sim_local_body wsat vrel fs ft r n%nat es%E σs et%E σt Φ)
-  (at level 70, format "'[hv' r  '/' ⊨{ n , fs , ft } '/  ' '[ ' ( es ,  '/' σs ) ']' '/' ≥  '/  ' '[ ' ( et ,  '/' σt ) ']'  '/' :  Φ ']'").
+  (at level 70, format "'[hv' r  '/' ⊨{ n , fs , ft }  '/  ' '[ ' ( es ,  '/' σs ) ']'  '/' ≥  '/  ' '[ ' ( et ,  '/' σt ) ']'  '/' :  Φ ']'").
 
-Notation "⊨{ fs , ft } f1 ≥ᶠ f2" :=
+Notation "⊨ᶠ{ fs , ft } f1 ≥ f2" :=
   (sim_local_fun wsat vrel fs ft end_call_sat f1 f2)
-  (at level 70, format "⊨{ fs , ft }  f1  ≥ᶠ  f2").
+  (at level 70, f1, f2 at next level, format "⊨ᶠ{ fs , ft }  f1  ≥  f2").
 
 Lemma sim_body_result fs ft r n es et σs σt Φ :
   (✓ r → Φ r n es σs et σt : Prop) →

theories/sim/local.v

@@ -119,12 +119,8 @@ Definition sim_local_fun
   (esat: A → state → state → Prop) (fn_src fn_tgt : function) : Prop :=
   ∀ r es et (vl_src vl_tgt: list value) σs σt
     (VALEQ: Forall2 (vrel r) vl_src vl_tgt)
-    (EQS: match fn_src with
-          | FunV xl e => subst_l xl (Val <$> vl_src) e = Some es
-          end)
-    (EQT: match fn_tgt with
-          | FunV xl e => subst_l xl (Val <$> vl_tgt) e = Some et
-          end),
+    (EQS: subst_l fn_src.(fun_b) (Val <$> vl_src) fn_src.(fun_e) = Some es)
+    (EQT: subst_l fn_tgt.(fun_b) (Val <$> vl_tgt) fn_tgt.(fun_e) = Some et),
     ∃ idx, sim_local_body r idx
                           (InitCall es) σs (InitCall et) σt
                           (λ r' _ rs' σs' rt' σt',
@@ -136,9 +132,7 @@ Definition sim_local_fun
 Definition sim_local_funs (esat: A → state → state → Prop) : Prop :=
   ∀ name fn_tgt, fnt !! name = Some fn_tgt → ∃ fn_src,
     fns !! name = Some fn_src ∧
-    match fn_src, fn_tgt with
-    | FunV xls _, FunV xlt _ => length xls = length xlt
-    end ∧
+    length (fn_src.(fun_b)) = length (fn_tgt.(fun_b)) ∧
     sim_local_fun esat fn_src fn_tgt.
 
 End local.

theories/sim/program.v

@@ -17,7 +17,7 @@ Lemma sim_prog_sim_classical
 Proof.
   destruct MAINT as (ebt & HCt & Eqt).
   destruct (FUNS _ _ Eqt) as ([xls ebs HCs] & Eqs & Eql & SIMf).
-  apply nil_length_inv in Eql. subst xls.
+  apply nil_length_inv in Eql. simplify_eq/=.
   specialize (SIMf ε ebs ebt [] [] init_state init_state) as [idx SIM]; [simpl; done..|].
   unfold behave_prog.
   eapply (adequacy_classical _ _ idx); [apply NSD| |by apply wf_init_state..].

theories/sim/simple.v

+(** A simpler simulation relation that hides the physical state.
+Useful whenever the resources we own are strong enough to carry us from step to step.
+
+When your goal is simple, to make it stateful just do [intros σs σt].
+To go the other direction, [apply sim_simplify]. Then you will likely
+want to clean some stuff from your context.
+*)
+
+From stbor.sim Require Export instance.
+
+Definition sim_simple fs ft r n es et Φ : Prop :=
+  ∀ σs σt, r ⊨{ n , fs , ft } ( es , σs ) ≥ ( et , σt ) : Φ.
+
+Notation "r ⊨ˢ{ n , fs , ft } es '≥' et : Φ" :=
+  (sim_simple fs ft r n%nat es%E et%E Φ)
+  (at level 70, es, et at next level,
+   format "'[hv' r  '/' ⊨ˢ{ n , fs , ft }  '/  ' '[ ' es ']'  '/' ≥  '/  ' '[ ' et ']'  '/' :  Φ ']'").
+
+Lemma sim_fun_simple1 n fs ft (esf etf: function) Φ :
+  length (esf.(fun_b)) = 1%nat →
+  length (etf.(fun_b)) = 1%nat →
+  (∀ es et vs vt r, vrel r vs vt →
+   subst_l (esf.(fun_b)) [Val vs] (esf.(fun_e)) = Some es →
+   subst_l (etf.(fun_b)) [Val vt] (etf.(fun_e)) = Some et →
+   r ⊨ˢ{n,fs,ft} es ≥ et : Φ) →
+  ⊨ᶠ{fs,ft} esf ≥ etf.
+Abort.