tie some global things together

_CoqProject

@@ -33,6 +33,7 @@ theories/sim/refl_step.v
 theories/sim/left_step.v
 theories/sim/right_step.v
 theories/sim/simple.v
+theories/sim/refl.v
 
 theories/opt/ex1.v
 theories/opt/ex1_down.v

theories/opt/ex1.v

-From stbor.sim Require Import local invariant refl_step tactics body simple program.
+From stbor.sim Require Import local invariant refl tactics simple program.
 
 Set Default Proof Using "Type".
 
@@ -26,12 +26,10 @@ Definition ex1_opt : function :=
     "v"
   .
 
-Lemma ex1_sim_body fs ft :
-  sim_local_funs_lookup fs ft →
-  ⊨ᶠ{fs,ft} ex1_unopt ≥ ex1_opt.
+Lemma ex1_sim_body :
+  ⊨ᶠ ex1_unopt ≥ ex1_opt.
 Proof.
-  intros Hfst.
-  apply (sim_fun_simple1 10)=>// rarg es css et cs args argt AREL ??.
+  apply (sim_fun_simple1 10)=>// fs ft rarg es css et cs args argt LOOK AREL ??.
   simplify_eq/=.
   (* InitCall *)
   apply sim_simple_init_call=> c /= {css}.
@@ -71,10 +69,10 @@ Proof.
   intros Hdec Hmain. apply sim_prog_sim_classical.
   { apply Hdec. }
   { apply has_main_insert; done. }
-  apply sim_local_funs_insert; first done.
-  - admit.
+  apply sim_mod_funs_local.
+  apply sim_mod_funs_insert; first done.
   - exact: ex1_sim_body.
-  - (* FIXME: Needs reflexivity. *)
-Admitted.
+  - exact: sim_mod_funs_refl.
+Qed.
 
 Print Assumptions ex1.

theories/sim/body.v

@@ -3,6 +3,22 @@ From stbor.sim Require Export instance.
 
 Set Default Proof Using "Type".
 
+Lemma sim_body_result fs ft r n es et σs σt Φ :
+  (✓ r → Φ r n es σs et σt : Prop) →
+  r ⊨{S n,fs,ft} (of_result es, σs) ≥ (of_result et, σt) : Φ.
+Proof.
+  intros POST. pfold.  split; last first.
+  { constructor 1. intros vt' ? STEPT'. exfalso.
+    apply result_tstep_stuck in STEPT'. by rewrite to_of_result in STEPT'. }
+  { move => ? /= Eqvt'. symmetry in Eqvt'. simplify_eq.
+    exists es, σs, r, n. split; last split.
+    - right. split; [lia|]. eauto.
+    - eauto.
+    - rewrite to_of_result in Eqvt'. simplify_eq.
+      apply POST. by destruct WSAT as (?&?&?%cmra_valid_op_r &?). }
+  { left. rewrite to_of_result. by eexists. }
+Qed.
+
 Lemma sim_body_res_proper fs ft n es σs et σt Φ r1 r2:
   r1 ≡ r2 →
   r1 ⊨{n,fs,ft} (es, σs) ≥ (et, σt) : Φ →

theories/sim/instance.v

@@ -5,26 +5,27 @@ 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 ) ']'  '/' :  Φ ']'").
 
-Notation "⊨ᶠ{ fs , ft } f1 ≥ f2" :=
-  (sim_local_fun wsat vrel fs ft end_call_sat 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) →
-  r ⊨{S n,fs,ft} (of_result es, σs) ≥ (of_result et, σt) : Φ.
-Proof.
-  intros POST. pfold.  split; last first.
-  { constructor 1. intros vt' ? STEPT'. exfalso.
-    apply result_tstep_stuck in STEPT'. by rewrite to_of_result in STEPT'. }
-  { move => ? /= Eqvt'. symmetry in Eqvt'. simplify_eq.
-    exists es, σs, r, n. split; last split.
-    - right. split; [lia|]. eauto.
-    - eauto.
-    - rewrite to_of_result in Eqvt'. simplify_eq.
-      apply POST. by destruct WSAT as (?&?&?%cmra_valid_op_r &?). }
-  { left. rewrite to_of_result. by eexists. }
-Qed.
+(** "modular" simulation relations dont make assumptions
+about the global fn table.
+This is very weak! A stronger version would, instead of universally quantifying the
+fn table, allow giving a lower bound. But this is good enough for now.
+
+This could be done in general, but we just do it for the instance. *)
+Definition sim_mod_fun f1 f2 :=
+  ∀ fs ft, sim_local_funs_lookup fs ft → sim_local_fun wsat vrel fs ft end_call_sat f1 f2.
+
+Definition sim_mod_funs (fns fnt: fn_env) :=
+  ∀ name fn_src, fns !! name = Some fn_src → ∃ fn_tgt,
+    fnt !! name = Some fn_tgt ∧
+    length fn_src.(fun_b) = length fn_tgt.(fun_b) ∧
+    sim_mod_fun fn_src fn_tgt.
 
+Notation "⊨ᶠ f1 ≥ f2" :=
+  (sim_mod_fun f1 f2)
+  (at level 70, f1, f2 at next level, format "⊨ᶠ  f1  ≥  f2").
+
+(** The modular version permits insertion. *)
 Lemma sim_local_funs_lookup_insert fns fnt x fs ft :
   length fns.(fun_b) = length fnt.(fun_b) →
   sim_local_funs_lookup fs ft →
@@ -39,58 +40,35 @@ Proof.
     rewrite lookup_insert_ne //.
 Qed.
 
-Lemma sim_local_body_insert fs ft fns fnt x r n es et σs σt Φ 
-  (FRESH : fs !! x = None)
-  (HOLD: sim_local_funs_lookup fs ft) :
-  ⊨ᶠ{fs,ft} fns ≥ fnt →
-  r ⊨{n,fs,ft} (es, σs) ≥ (et, σt) : Φ →
-  r ⊨{n,<[x:=fns]> fs,<[x:=fnt]> ft} (es, σs) ≥ (et, σt) : Φ.
-Proof.
-  intros FUN. revert r n es et σs σt Φ. pcofix CIH.
-  intros r1 n es et σs σt Φ SIM. punfold SIM. pfold.
-  intros NT r_f WSAT.
-  have NT2: never_stuck fs es σs. { admit. }
-  specialize (SIM NT2 r_f WSAT) as [NS TE ST]. split.
-  - destruct NS as [|RED]; [by left|]. right. admit.
-  - intros vt Eqvt.
-    specialize (TE _ Eqvt) as (vs' & σs' & r' & n' & STEPS' & WSAT' & HΦ).
-    exists vs', σs', r', n'. split; last split; [|done..].
-    { destruct STEPS' as [STEPS'|]; [|by right]. left. admit. }
-  - inversion ST.
-    + constructor 1.
-      intros et' σt' STEPT.
-      have STEPT2: (et, σt) ~{ft}~> (et', σt'). { admit. }
-      specialize (STEP _ _ STEPT2) as (vs' & σs' & r' & n' & STEPS' & WSAT' & CONT).
-      exists vs', σs', r', n'. split; last split; [|done|].
-      { admit. }
-      pclearbot. right. by apply CIH.
-    + econstructor 2; eauto.
-      { instantiate (1:= Ks). admit. }
-      intros r' vs vt σs' σt' VREL' WSAT' STACK'.
-      specialize (CONT r' vs vt σs' σt' VREL' WSAT' STACK') as [n' CONT].
-      exists n'. pclearbot. right. by apply CIH.
-Admitted.
-
-Lemma sim_local_funs_insert fns fnt x fs ft :
+Lemma sim_mod_funs_insert fs ft x fns fnt :
   length fns.(fun_b) = length fnt.(fun_b) →
-  fs !! x = None →
-  (* FIXME: add notation for this. Probably replacing ⊨ᶠ. *)
-  (∀ fs ft, sim_local_funs_lookup fs ft → ⊨ᶠ{ fs , ft } fns ≥ fnt) →
-  sim_local_funs wsat vrel fs ft end_call_sat →
-  sim_local_funs wsat vrel (<[x:=fns]>fs) (<[x:=fnt]>ft) end_call_sat.
+  (⊨ᶠ fns ≥ fnt) →
+  sim_mod_funs fs ft →
+  sim_mod_funs (<[x:=fns]>fs) (<[x:=fnt]>ft).
 Proof.
-  intros ?? Hnew Hold. intros f fn_src.
+  intros ? Hnew Hold. intros f fn_src.
   destruct (decide (x=f)) as [->|Hne].
   - rewrite lookup_insert=>[=?]. subst. exists fnt. rewrite lookup_insert.
     split; first done. split; first done. apply Hnew.
-    apply sim_local_funs_lookup_insert; first done.
-    exact: sim_local_funs_to_lookup.
   - rewrite lookup_insert_ne // =>Hlk.
     destruct (Hold _ _ Hlk) as (f_tgt & ? & ? & Hf). exists f_tgt.
-    rewrite lookup_insert_ne //. split; first done.
-    split; first done.
-    have ? : sim_local_funs_lookup fs ft by eapply sim_local_funs_to_lookup.
-    intros r es et vs vt σs σt VREL SUBS SUBT.
-    specialize (Hf r es et vs vt σs σt VREL SUBS SUBT) as [n Hf].
-    exists n. apply sim_local_body_insert; [done..|by apply Hnew|done].
+    rewrite lookup_insert_ne //.
+Qed.
+
+Lemma sim_mod_funs_to_lookup fs ft:
+  sim_mod_funs fs ft → sim_local_funs_lookup fs ft.
+Proof.
+  intros Hlf name fns Hlk. destruct (Hlf _ _ Hlk) as (fnt & ? & ? & ?).
+  eauto.
+Qed.
+
+(** Once we got all things together, we can get the whole-program
+assumption. *)
+Lemma sim_mod_funs_local fs ft :
+  sim_mod_funs fs ft →
+  sim_local_funs wsat vrel fs ft end_call_sat.
+Proof.
+  intros Hmod. intros f fn_src Hlk.
+  destruct (Hmod _ _ Hlk) as (fn_tgt & ? & ? & ?). exists fn_tgt.
+  eauto using sim_mod_funs_to_lookup.
 Qed.

theories/sim/local.v

@@ -10,7 +10,7 @@ Section local.
 Context {A: ucmraT}.
 Variable (wsat: A → state → state → Prop).
 Variable (vrel: A → value → value → Prop).
-Variable (fns fnt: fn_env).
+Variable (fs ft: fn_env).
 
 Notation PRED := (A → nat → result → state → result → state → Prop)%type.
 Notation SIM := (A → nat → expr → state → expr → state → PRED → Prop)%type.
@@ -21,25 +21,25 @@ Inductive _sim_local_body_step (r_f : A) (sim_local_body : SIM)
   (r: A) (idx: nat) es σs et σt Φ : Prop :=
 (* If tgt makes 1 step, src can make some step *)
 | sim_local_body_step_next
-    (STEP: ∀ et' σt' (STEPT: (et, σt) ~{fnt}~> (et', σt')),
+    (STEP: ∀ et' σt' (STEPT: (et, σt) ~{ft}~> (et', σt')),
       (* then we locally can makes some step and pick a new resource r' *)
       ∃ es' σs' r' idx',
-        ((es, σs) ~{fns}~>+ (es', σs') ∨
+        ((es, σs) ~{fs}~>+ (es', σs') ∨
          ((idx' < idx)%nat ∧ (es', σs') = (es, σs))) ∧
         wsat (r_f ⋅ r') σs' σt' ∧
         sim_local_body r' idx' es' σs' et' σt' Φ)
 (* If tgt prepares to make a call to [name], src should be able to make the same
   call. Here we do not want to step into the call of [name], but to step over it. *)
 | sim_local_body_step_over_call
-    (Ks: list (ectxi_language.ectx_item (bor_ectxi_lang fns)))
-    (Kt: list (ectxi_language.ectx_item (bor_ectxi_lang fnt)))
+    (Ks: list (ectxi_language.ectx_item (bor_ectxi_lang fs)))
+    (Kt: list (ectxi_language.ectx_item (bor_ectxi_lang ft)))
     fid (vl_tgt: list value)
     (vl_src: list value) σ1_src
     rc rv
     (* tgt is ready to make a call of [name] *)
     (CALLTGT: et = fill Kt (Call #[ScFnPtr fid] (Val <$> vl_tgt)))
     (* src is ready to make a call of [name] *)
-    (CALLSRC: (es, σs) ~{fns}~>* (fill Ks (Call #[ScFnPtr fid] (Val <$> vl_src)), σ1_src))
+    (CALLSRC: (es, σs) ~{fs}~>* (fill Ks (Call #[ScFnPtr fid] (Val <$> vl_src)), σ1_src))
     (* and we can pick a resource [rv] for the arguments *)
     (WSAT: wsat (r_f ⋅ (rc ⋅ rv)) σ1_src σt)
     (* [rv] justifies the arguments *)
@@ -58,13 +58,13 @@ Inductive _sim_local_body_step (r_f : A) (sim_local_body : SIM)
 Record sim_local_body_base (r_f: A) (sim_local_body : SIM)
   (r: A) (idx: nat) es σs et σt Φ : Prop := {
   sim_local_body_stuck :
-    (terminal et ∨ reducible fnt et σt) ;
+    (terminal et ∨ reducible ft et σt) ;
   sim_local_body_terminal :
     (* if tgt is terminal *)
     ∀ vt (TERM: to_result et = Some vt),
       (* then src can get terminal *)
       ∃ vs' σs' r' idx',
-        sflib.__guard__ ((es, σs) ~{fns}~>+ (of_result vs', σs') ∨
+        sflib.__guard__ ((es, σs) ~{fs}~>+ (of_result vs', σs') ∨
                          ((idx' < idx)%nat ∧ (es, σs) = (of_result vs', σs'))) ∧
         (* and re-establish wsat *)
         wsat (r_f ⋅ r') σs' σt ∧ Φ r' idx' vs' σs' vt σt ;
@@ -75,7 +75,7 @@ Record sim_local_body_base (r_f: A) (sim_local_body : SIM)
 Definition _sim_local_body (sim_local_body : SIM)
   (r: A) (idx: nat) es σs et σt Φ : Prop :=
   (* assuming that src cannot get stuck *)
-  ∀ (NEVER_STUCK: never_stuck fns es σs)
+  ∀ (NEVER_STUCK: never_stuck fs es σs)
     (* for any frame r_f that is compatible with our resource r has world satisfaction *)
     r_f (WSAT: wsat (r_f ⋅ r) σs σt),
     sim_local_body_base r_f sim_local_body r idx es σs et σt Φ.
@@ -112,10 +112,12 @@ Proof.
     exists idx'. pclearbot. right. eapply CIH; eauto.
 Qed.
 
-(* Simulating functions:
+(** Simulating functions:
   - We start after the substitution.
   - We assume the arguments are values related by [r]
-  - The returned result must also be values and related by [vrel]. *)
+  - The returned result must also be values and related by [vrel].
+This is called "local" because it considers one function at a time.
+However, it does assume full knowledge about the GLOBAL function table! *)
 Definition fun_post (esat: A → call_id → Prop) initial_call_id_stack
   (r: A) (n: nat) rs (σs: state) rt σt :=
   (∃ c, σt.(scs) = c :: initial_call_id_stack ∧ esat r c) ∧
@@ -131,21 +133,21 @@ Definition sim_local_fun
                           (fun_post esat σt.(scs)).
 
 Definition sim_local_funs (esat: A → call_id → Prop) : Prop :=
-  ∀ name fn_src, fns !! name = Some fn_src → ∃ fn_tgt,
-    fnt !! name = Some fn_tgt ∧
+  ∀ name fn_src, fs !! name = Some fn_src → ∃ fn_tgt,
+    ft !! name = Some fn_tgt ∧
     length fn_src.(fun_b) = length fn_tgt.(fun_b) ∧
     sim_local_fun esat fn_src fn_tgt.
 
 Definition sim_local_funs_lookup : Prop :=
-  ∀ name fn_src, fns !! name = Some fn_src → ∃ fn_tgt,
-    fnt !! name = Some fn_tgt ∧
+  ∀ name fn_src, fs !! name = Some fn_src → ∃ fn_tgt,
+    ft !! name = Some fn_tgt ∧
     length fn_src.(fun_b) = length fn_tgt.(fun_b).
 
 Lemma sim_local_funs_to_lookup esat :
   sim_local_funs esat → sim_local_funs_lookup.
 Proof.
-  intros Hlf name fs Hlk. destruct (Hlf _ _ Hlk) as (ft & ? & ? & ?).
-  exists ft. auto.
+  intros Hlf name fns Hlk. destruct (Hlf _ _ Hlk) as (fnt & ? & ? & ?).
+  eauto.
 Qed.
 
 (* Viewshift *)
@@ -176,7 +178,5 @@ Proof.
 Qed.
 
 End local.
-(*
-Definition sim_mod_fun 
-*)
+
 Hint Resolve sim_local_body_mono : paco.

theories/sim/refl.v

+From stbor.lang Require Import lang.
+From stbor.sim Require Import refl_step.
+
+Set Default Proof Using "Type".
+
+Lemma sim_mod_funs_refl prog :
+  sim_mod_funs prog prog.
+Proof.
+Admitted.

theories/sim/refl_step.v

 From iris.algebra Require Import local_updates.
 
 From stbor.lang Require Import steps_progress steps_inversion steps_retag.
-From stbor.sim Require Export instance.
+From stbor.sim Require Export instance body.
 
 Set Default Proof Using "Type".
 

theories/sim/simple.v

@@ -7,7 +7,8 @@ To go the other direction, [apply sim_simplify NEW_POST]. Then you will likely
 want to clean some stuff from your context.
 *)
 
-From stbor.sim Require Import body instance refl_step.
+From stbor.sim Require Export body instance.
+From stbor.sim Require Import refl_step.
 
 Definition fun_post_simple
   initial_call_id_stack (r: resUR) (n: nat) vs (css: call_id_stack) vt cst :=
@@ -43,17 +44,18 @@ Qed.
 
 (** Simple proof for a function taking one argument. *)
 (* TODO: make the two call stacks the same. *)
-Lemma sim_fun_simple1 n fs ft (esf etf: function) :
+Lemma sim_fun_simple1 n (esf etf: function) :
   length (esf.(fun_b)) = 1%nat →
   length (etf.(fun_b)) = 1%nat →
-  (∀ rf es css et cst vs vt,
+  (∀ fs ft rf es css et cst vs vt,
+    sim_local_funs_lookup fs ft →
     vrel rf 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 →
     rf ⊨ˢ{n,fs,ft} (InitCall es, css) ≥ (InitCall et, cst) : fun_post_simple cst) →
-  ⊨ᶠ{fs,ft} esf ≥ etf.
+  ⊨ᶠ esf ≥ etf.
 Proof.
-  intros Hls Hlt HH rf es et vls vlt σs σt FREL SUBSTs SUBSTt. exists n.
+  intros Hls Hlt HH fs ft Hlook rf es et vls vlt σs σt FREL SUBSTs SUBSTt. exists n.
   move:(subst_l_is_Some_length _ _ _ _ SUBSTs) (subst_l_is_Some_length _ _ _ _ SUBSTt).
   rewrite Hls Hlt.
   destruct vls as [|vs []]; [done| |done].