some global glue

theories/opt/ex1.v

-From stbor.sim Require Import local invariant refl_step tactics body simple.
+From stbor.sim Require Import local invariant refl_step tactics body simple program.
 
 Set Default Proof Using "Type".
 
@@ -57,4 +57,19 @@ Proof.
   intros rf frs frt FREL.
   apply sim_simple_val.
 
-Abort.
+Admitted.
+
+Lemma ex1_sim (prog: fn_env) :
+  stuck_decidable →
+  has_main prog →
+  let prog_src := <["ex1":=ex1]> prog in
+  let prog_tgt := <["ex1":=ex1_opt]> prog in
+  behave_prog prog_tgt <1= behave_prog prog_src.
+Proof.
+  intros Hdec Hmain. apply sim_prog_sim_classical.
+  { apply Hdec. }
+  { apply has_main_insert; done. }
+  apply sim_local_funs_insert; first done.
+  - exact: ex1_sim_body.
+  - (* FIXME: Needs reflexivity. *)
+Admitted.

theories/sim/global_adequacy.v

@@ -30,14 +30,15 @@ Proof.
 Qed.
 
 (** A classically provable assumption: each program is either never-stuck or it can get stuck. *)
-Definition stuck_decidable prog: Prop :=
+Definition stuck_decidable_1 prog: Prop :=
   ∀ e σ, never_stuck prog e σ \/
                     exists e' σ', (e, σ) ~{prog}~>* (e', σ') /\
                              ~ terminal e' /\
                              ~ reducible prog e' σ'.
+Definition stuck_decidable: Prop := ∀ prog, stuck_decidable_1 prog.
 
 Lemma classically_stuck_decidable :
-  (∀ P, P ∨ ¬P) → ∀ prog, stuck_decidable prog.
+  (∀ P, P ∨ ¬P) → stuck_decidable.
 Proof.
   intros EM prog e σ.
   set RHS := exists _, _. destruct (EM RHS) as [POS|NEG]; first by right.
@@ -112,7 +113,7 @@ Qed.
 Lemma adequacy_classical
       prog_src
       prog_tgt idx conf_src conf_tgt
-      `{NSD: stuck_decidable prog_src}
+      `{NSD: stuck_decidable_1 prog_src}
       (SIM: sim prog_src prog_tgt idx conf_src conf_tgt)
       (WFS: Wf conf_src.2)
       (WFT: Wf conf_tgt.2)

theories/sim/instance.v

@@ -24,3 +24,36 @@ Proof.
       apply POST. by destruct WSAT as (?&?&?%cmra_valid_op_r &?). }
   { left. rewrite to_of_result. by eexists. }
 Qed.
+
+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 →
+  sim_local_funs_lookup (<[x:=fns]>fs) (<[x:=fnt]>ft).
+Proof.
+  intros Hnew Hold f f_src.
+  destruct (decide (x=f)) as [->|Hne].
+  - rewrite lookup_insert=>[=?]. subst. exists fnt. rewrite lookup_insert.
+    auto.
+  - rewrite lookup_insert_ne // =>Hlk.
+    destruct (Hold _ _ Hlk) as (f_tgt & ? & ?). exists f_tgt.
+    rewrite lookup_insert_ne //.
+Qed.
+
+Lemma sim_local_funs_insert fns fnt x fs ft :
+  length fns.(fun_b) = length fnt.(fun_b) →
+  (* 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.
+Proof.
+  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 & ? & ? & ?). exists f_tgt.
+    rewrite lookup_insert_ne //. split; first done.
+    split; first done.
+Admitted.

theories/sim/local.v

@@ -141,6 +141,13 @@ Definition sim_local_funs_lookup : Prop :=
     fnt !! 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.
+Qed.
+
 End local.
 
 Hint Resolve sim_local_body_mono : paco.

theories/sim/program.v

 From stbor.lang Require Import steps_wf steps_inversion.
-From stbor.sim Require Import sflib behavior global local invariant.
-From stbor.sim Require Import global_adequacy local_adequacy refl_step.
+From stbor.sim Require Import sflib global local invariant.
+From stbor.sim Require Import local_adequacy refl_step.
+From stbor.sim Require Export global_adequacy behavior.
 
 Set Default Proof Using "Type".
 
+Definition has_main (prog: fn_env) : Prop :=
+  ∃ ebs HCs, prog !! "main" = Some (@FunV [] ebs HCs).
+
+Lemma has_main_insert (prog: fn_env) (x: string) (f: function) :
+  x ≠ "main" → has_main prog → has_main (<[x:=f]> prog).
+Proof.
+  intros Hne (ebs & HCs & EQ). exists ebs, HCs.
+  rewrite lookup_insert_ne //.
+Qed.
+
 Lemma sim_prog_sim_classical
       prog_src
       prog_tgt
-      `{NSD: stuck_decidable prog_src}
+      `{NSD: stuck_decidable_1 prog_src}
+      (MAINT: has_main prog_src)
       (FUNS: sim_local_funs wsat vrel prog_src prog_tgt end_call_sat)
-      (MAINT: ∃ ebs HCs, prog_src !! "main" = Some (@FunV [] ebs HCs))
   : behave_prog prog_tgt <1= behave_prog prog_src.
 Proof.
   destruct MAINT as (ebs & HCs & Eqs).