well-formedness

theories/lang/lang_base.v

@@ -286,9 +286,9 @@ Qed.
 
 (** Global static function table *)
 Record function := FunV {
-  fun_b: list binder;
-  fun_e: expr;
-  fun_closed: Closed (fun_b +b+ []) fun_e
+  fun_args: list binder;
+  fun_body: expr;
+  fun_closed: Closed (fun_args +b+ []) fun_body
 }.
 Arguments FunV _ _ {_}.
 Definition fn_env := gmap fn_id function.

theories/opt/ex1.v

@@ -59,7 +59,7 @@ Admitted.
 
 (** Top-level theorem: Two programs that only differ in the
 "ex1" function are related. *)
-Lemma ex1 (prog: fn_env) :
+Corollary ex1 (prog: fn_env) :
   stuck_decidable →
   has_main prog →
   let prog_src := <["ex1":=ex1_unopt]> prog in

theories/opt/ex1_down.v

@@ -23,13 +23,6 @@ Definition ex1_down_opt : function :=
     .
 
 
-Lemma ex1_down_sim_fun fs ft : ⊨ᶠ{fs,ft} ex1_down ≥ ex1_down_opt.
+Lemma ex1_down_sim_fun : ⊨ᶠ 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.
-  destruct vlt as [|vt []]; [done| |done].  simpl in SUBSTt. simplify_eq.
-
-  (* InitCall *)
-  exists 10%nat.
-  apply sim_body_init_call. simpl.
 Abort.

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 : ⊨ᶠ ex2 ≥ ex2_opt.
 Proof.
 Abort.

theories/opt/ex2_down.v

@@ -23,13 +23,6 @@ Definition ex2_down_opt : function :=
     .
 
 
-Lemma ex2_down_sim_fun fs ft : ⊨ᶠ{fs,ft} ex2_down ≥ ex2_down_opt.
+Lemma ex2_down_sim_fun : ⊨ᶠ 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.
-  destruct vlt as [|vt []]; [done| |done].  simpl in SUBSTt. simplify_eq.
-
-  (* InitCall *)
-  exists 10%nat.
-  apply sim_body_init_call. simpl.
 Abort.

theories/opt/ex3.v

@@ -32,13 +32,6 @@ Definition ex3_opt_2 : function :=
     Call #[ScFnPtr "f"] []
   .
 
-Lemma ex3_sim_fun fs ft : ⊨ᶠ{fs,ft} ex3 ≥ ex3_opt_1.
+Lemma ex3_sim_fun : ⊨ᶠ 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.
-  destruct vlt as [|vt []]; [done| |done].  simpl in SUBSTt. simplify_eq.
-
-  (* InitCall *)
-  exists 10%nat.
-  apply sim_body_init_call. simpl.
 Abort.

theories/opt/ex3_down.v

@@ -34,13 +34,6 @@ 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 : ⊨ᶠ 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.
-  destruct vlt as [|vt []]; [done| |done].  simpl in SUBSTt. simplify_eq.
-
-  (* InitCall *)
-  exists 10%nat.
-  apply sim_body_init_call. simpl.
 Abort.

theories/sim/instance.v

@@ -18,7 +18,7 @@ Definition sim_mod_fun 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) ∧
+    length fn_src.(fun_args) = length fn_tgt.(fun_args) ∧
     sim_mod_fun fn_src fn_tgt.
 
 Notation "⊨ᶠ f1 ≥ f2" :=
@@ -27,7 +27,7 @@ Notation "⊨ᶠ 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) →
+  length fns.(fun_args) = length fnt.(fun_args) →
   sim_local_funs_lookup fs ft →
   sim_local_funs_lookup (<[x:=fns]>fs) (<[x:=fnt]>ft).
 Proof.
@@ -41,7 +41,7 @@ Proof.
 Qed.
 
 Lemma sim_mod_funs_insert fs ft x fns fnt :
-  length fns.(fun_b) = length fnt.(fun_b) →
+  length fns.(fun_args) = length fnt.(fun_args) →
   (⊨ᶠ fns ≥ fnt) →
   sim_mod_funs fs ft →
   sim_mod_funs (<[x:=fns]>fs) (<[x:=fnt]>ft).

theories/sim/local.v

@@ -126,8 +126,8 @@ Definition sim_local_fun
   (esat: A → call_id → 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: 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),
+    (EQS: subst_l fn_src.(fun_args) (Val <$> vl_src) fn_src.(fun_body) = Some es)
+    (EQT: subst_l fn_tgt.(fun_args) (Val <$> vl_tgt) fn_tgt.(fun_body) = Some et),
     ∃ idx, sim_local_body r idx
                           (InitCall es) σs (InitCall et) σt
                           (fun_post esat σt.(scs)).
@@ -135,13 +135,13 @@ Definition sim_local_fun
 Definition sim_local_funs (esat: A → call_id → Prop) : Prop :=
   ∀ 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) ∧
+    length fn_src.(fun_args) = length fn_tgt.(fun_args) ∧
     sim_local_fun esat fn_src fn_tgt.
 
 Definition sim_local_funs_lookup : Prop :=
   ∀ 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).
+    length fn_src.(fun_args) = length fn_tgt.(fun_args).
 
 Lemma sim_local_funs_to_lookup esat :
   sim_local_funs esat → sim_local_funs_lookup.

theories/sim/refl.v

@@ -3,7 +3,42 @@ From stbor.sim Require Import refl_step.
 
 Set Default Proof Using "Type".
 
+(** Enable use of [Forall] in recursion. *)
+Lemma Forall_id {A: Type} (P: A → Prop) (l: list A) :
+  Forall P l ↔ Forall id (map P l).
+Proof.
+  induction l; simpl; first by eauto using Forall_nil.
+  split; intros [??]%Forall_cons_1; apply Forall_cons; simpl; tauto.
+Qed.
+
+(** "Well-formed" code doen't contain literal
+pointers, places or administrative operations (init_call/end_call).
+Defined by recursion to make sure we don't miss a case. *)
+Fixpoint scalar_wf (a: scalar) : Prop :=
+  match a with
+  | ScPoison | ScInt _ | ScFnPtr _ => True
+  | ScnPtr => False
+  end.
+Definition value_wf (v: value) : Prop := Forall scalar_wf v.
+Fixpoint expr_wf (e: expr) : Prop :=
+  match e with
+  (* Structural cases. *)
+  | Val v => value_wf v
+  | Call f args => expr_wf f ∧ Forall id (map expr_wf args)
+  | Case e branches => expr_wf e ∧ Forall id (map expr_wf branches)
+  | Var _ | Alloc _ => True
+  | Deref e _ | Ref e  | Copy e | Retag e _ =>
+    expr_wf e
+  | Proj e1 e2 | Conc e1 e2 | BinOp _ e1 e2 | Let _ e1 e2 | Write e1 e2 =>
+    expr_wf e1 ∧ expr_wf e2
+  (* Forbidden cases. *)
+  | InitCall e | EndCall e => False
+  | Place _ _ _ => False
+  | Free _ => False (* TODO: We'd like to support deallocation! *)
+  end.
+
 Theorem sim_mod_fun_refl f :
+  expr_wf f.(fun_body) →
   ⊨ᶠ f ≥ f.
 Proof.
 Admitted.
@@ -15,4 +50,4 @@ Proof.
   { intros ??. rewrite lookup_empty. done. }
   apply sim_mod_funs_insert; try done.
   apply sim_mod_fun_refl.
-Qed.
+Admitted.

theories/sim/simple.v

@@ -45,13 +45,13 @@ Qed.
 (** Simple proof for a function taking one argument. *)
 (* TODO: make the two call stacks the same. *)
 Lemma sim_fun_simple1 n (esf etf: function) :
-  length (esf.(fun_b)) = 1%nat →
-  length (etf.(fun_b)) = 1%nat →
+  length (esf.(fun_args)) = 1%nat →
+  length (etf.(fun_args)) = 1%nat →
   (∀ 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 →
+    subst_l (esf.(fun_args)) [Val vs] (esf.(fun_body)) = Some es →
+    subst_l (etf.(fun_args)) [Val vt] (etf.(fun_body)) = Some et →
     rf ⊨ˢ{n,fs,ft} (InitCall es, css) ≥ (InitCall et, cst) : fun_post_simple cst) →
   ⊨ᶠ esf ≥ etf.
 Proof.