program WF

theories/lang/defs.v

@@ -90,36 +90,6 @@ Definition never_stuck fs e σ :=
 Definition init_expr := (Call #["main"] []).
 Definition init_state := (mkState ∅ ∅ [O] O 1).
 
-Definition scalar_wf (s: scalar) : bool :=
-  match s with
-  | ScPtr _ _ => false
-  | _ => true
-  end.
-Definition value_wf (v: value) : bool := forallb scalar_wf v.
-
-Fixpoint expr_wf (e: expr) : bool :=
-  match e with
-  | Var y => true
-  | Val v => value_wf v
-  | Call e el => expr_wf e && forallb expr_wf el
-  | InitCall e => expr_wf e
-  | EndCall e => false
-  | Place l tag T => false
-  | BinOp op e1 e2 => expr_wf e1 && expr_wf e2
-  | Proj e1 e2 => expr_wf e1 && expr_wf e2
-  | Conc e1 e2 => expr_wf e1 && expr_wf e2
-  | Copy e => expr_wf e
-  | Write e1 e2 => expr_wf e1 && expr_wf e2
-  | Alloc T => true
-  | Free e => expr_wf e
-  | Deref e T => expr_wf e
-  | Ref e => expr_wf e
-  (* | Field e path => expr_wf e *)
-  | Retag e kind => expr_wf e
-  | Let x1 e1 e2 => expr_wf e1 && expr_wf e2
-  | Case e el => expr_wf e && forallb expr_wf el
-  end.
-
 (*=================================== UNUSED =================================*)
 (* Implicit Type (ρ: cfg bor_lang). *)
 

theories/opt/ex1.v

@@ -61,14 +61,14 @@ Admitted.
 "ex1" function are related. *)
 Corollary ex1 (prog: fn_env) :
   stuck_decidable →
-  has_main prog →
+  prog_wf prog →
   let prog_src := <["ex1":=ex1_unopt]> 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.
+  intros Hdec Hwf. apply sim_prog_sim_classical.
   { apply Hdec. }
-  { apply has_main_insert; done. }
+  { apply has_main_insert, Hwf; done. }
   apply sim_mod_funs_local.
   apply sim_mod_funs_insert; first done.
   - exact: ex1_sim_body.

theories/sim/instance.v

@@ -72,3 +72,14 @@ Proof.
   destruct (Hmod _ _ Hlk) as (fn_tgt & ? & ? & ?). exists fn_tgt.
   eauto using sim_mod_funs_to_lookup.
 Qed.
+
+(** Whole-programs need a "main". *)
+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.

theories/sim/program.v

@@ -5,16 +5,6 @@ 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.
-
 Theorem sim_prog_sim_classical
       prog_src
       prog_tgt

theories/sim/refl.v

@@ -14,7 +14,7 @@ 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 :=
+Definition scalar_wf (a: scalar) : Prop :=
   match a with
   | ScPoison | ScInt _ | ScFnPtr _ => True
   | ScnPtr => False
@@ -36,6 +36,9 @@ Fixpoint expr_wf (e: expr) : Prop :=
   | Place _ _ _ => False
   | Free _ => False (* TODO: We'd like to support deallocation! *)
   end.
+Definition prog_wf (prog: fn_env) :=
+  has_main prog ∧
+  map_Forall (λ _ f, expr_wf f.(fun_body)) prog.
 
 Theorem sim_mod_fun_refl f :
   expr_wf f.(fun_body) →
@@ -44,10 +47,12 @@ Proof.
 Admitted.
 
 Lemma sim_mod_funs_refl prog :
+  prog_wf prog →
   sim_mod_funs prog prog.
 Proof.
-  induction prog using map_ind.
+  intros [_ WF]. induction prog using map_ind.
   { intros ??. rewrite lookup_empty. done. }
-  apply sim_mod_funs_insert; try done.
-  apply sim_mod_fun_refl.
-Admitted.
+  apply sim_mod_funs_insert; first done.
+  - apply sim_mod_fun_refl. eapply WF. erewrite lookup_insert. done.
+  - apply IHprog. eapply map_Forall_insert_12; done.
+Qed.