Start working on HOL4 port of new semantics and add some documentation

hol4/CommandsScript.sml

@@ -7,34 +7,54 @@ open AbbrevsTheory ExpressionAbbrevsTheory
 
 val _ = new_theory "Commands";
 
+(**
+  Next define what a program is.
+  Currently no loops, or conditionals.
+  Only assignments and return statement
+**)
 val _ = Datatype `
   cmd = Let num ('v exp) cmd
-       | Ret ('v exp)
-       | Nop`;
-
-(*
-val (sstep_rules, sstep_ind, sstep_cases) = Hol_reln `
-  (! x e s VarEnv ParamEnv P v eps.
-    eval_exp eps VarEnv ParamEnv P e v ==>
-    sstep (Let x e s) VarEnv ParamEnv P eps s (updEnv x v VarEnv)) /\
-  (! e VarEnv ParamEnv P v eps.
-    eval_exp eps VarEnv ParamEnv P e v ==>
-    sstep (Ret e) VarEnv ParamEnv P eps Nop (updEnv 0 v VarEnv))`;
-*)
+       | Ret ('v exp)`;
 
+(**
+  Define big step semantics for the Daisy language, terminating on a "returned"
+  result value
+ **)
 val (bstep_rules, bstep_ind, bstep_cases) = Hol_reln `
-  (! x e s s' E v eps VarEnv2.
-    eval_exp eps E e v /\
-    bstep s (updEnv x v E) eps s' VarEnv2 ==>
-    bstep (Let x e s) E eps s' VarEnv2) /\
-  (! e E v eps.
-    eval_exp eps E e v ==>
-    bstep (Ret e) E eps Nop (updEnv 0 v VarEnv))`;
+  (!x e s s' E v eps vR.
+      eval_exp eps E e v /\
+      bstep s (updEnv x v E) eps s' vR ==>
+      bstep (Let x e s) E eps s' vR) /\
+  (!e E v eps.
+      eval_exp eps E e v ==>
+      bstep (Ret e) E eps Nop v)`;
 
+(**
+  Generate a better case lemma again
+**)
 val bstep_cases =
   map (GEN_ALL o SIMP_CONV (srw_ss()) [Once bstep_cases])
     [``bstep (Let x e s) E eps s' VarEnv2``,
      ``bstep (Ret e) E eps Nop VarEnv2``]
   |> LIST_CONJ |> curry save_thm "bstep_cases";
 
+(**
+  The free variables of a command are all used variables of expressions
+  without the let bound variables
+**)
+val freeVars_def = Define `
+  freeVars (f: 'a cmd) :num_set =
+    case f of
+      |Let x e g => delete x (union (usedVars e) (freeVars g))
+      |Ret e => usedVars e`;
+
+(**
+  The defined variables of a command are all let bound variables
+**)
+val definedVars_def = Define `
+  definedVars (f:'a cmd) :num_set =
+    case f of
+      |Let x e g => Insert x (definedVars g)
+      |Ret e => LN`;
+
 val _ = export_theory ();

hol4/ExpressionAbbrevsScript.sml

-
+(**
+  Some abbreviations that require having defined expressions beforehand
+  If we would put them in the Abbrevs file, this would create a circular dependency which Coq cannot resolve.
+**)
 open preamble
 open ExpressionsTheory
 
 val _ = new_theory "ExpressionAbbrevs"
 
+(**
+We treat a function mapping an expression arguing on fractions as value type
+to pairs of intervals on rationals and rational errors as the analysis result
+**)
 val _ = type_abbrev("analysisResult", ``:real exp->(interval # real)``);
 
 val _ = export_theory()

hol4/Infra/DaisyTactics.sml

+(*
+  Some tactics which ease proving goals
+*)
+
+structure DaisyTactics =
+struct
+
+local open intLib wordsLib in end;
+open set_relationTheory;
+open BasicProvers Defn HolKernel Parse Tactic monadsyntax
+     alistTheory arithmeticTheory bagTheory boolLib boolSimps bossLib
+     combinTheory dep_rewrite finite_mapTheory indexedListsTheory lcsymtacs
+     listTheory llistTheory markerLib miscTheory
+     optionTheory pairLib pairTheory pred_setTheory
+     quantHeuristicsLib relationTheory res_quanTheory rich_listTheory
+     sortingTheory sptreeTheory stringTheory sumTheory wordsTheory;
+
+fun elim_conj thm =
+  let val (hypl, concl) = dest_thm thm in
+      if is_conj concl
+      then
+          let val (thm1, thm2) = CONJ_PAIR thm in
+              elim_conj thm1 \\ elim_conj thm2
+          end
+      else
+          ASSUME_TAC thm
+  end;
+
+fun elim_exist1 thm =
+  let val (hypl, concl) = dest_thm thm in
+      if is_exists concl
+      then
+              CHOOSE_THEN elim_exist thm
+      else
+          elim_conj thm
+  end
+and elim_exist thm =
+  let val (hypl, concl) = dest_thm thm in
+      if is_exists concl
+      then
+              CHOOSE_THEN elim_exist1 thm
+      else
+          elim_conj thm
+  end;
+
+fun inversion pattern cases_thm =
+  qpat_x_assum pattern
+               (fn thm => elim_exist (ONCE_REWRITE_RULE [cases_thm] thm));
+
+fun qexistsl_tac termlist =
+	case termlist of
+	 [] => ALL_TAC
+     | t::tel => qexists_tac t \\ qexistsl_tac tel;
+
+end

hol4/Infra/preamble.sml

@@ -23,43 +23,6 @@ fun asm_match q = Q.MATCH_ASSUM_RENAME_TAC q
 val match_exists_tac = part_match_exists_tac (hd o strip_conj)
 val asm_exists_tac = first_assum(match_exists_tac o concl)
 val has_pair_type = can dest_prod o type_of
-
-fun elim_conj thm =
-  let val (hypl, concl) = dest_thm thm in
-      if is_conj concl
-      then
-          let val (thm1, thm2) = CONJ_PAIR thm in
-              elim_conj thm1 \\ elim_conj thm2
-          end
-      else
-          ASSUME_TAC thm
-  end;
-
-fun elim_exist1 thm =
-  let val (hypl, concl) = dest_thm thm in
-      if is_exists concl
-      then
-              CHOOSE_THEN elim_exist thm
-      else
-          elim_conj thm
-  end
-and elim_exist thm =
-  let val (hypl, concl) = dest_thm thm in
-      if is_exists concl
-      then
-              CHOOSE_THEN elim_exist1 thm
-      else
-          elim_conj thm
-  end;
-
-fun inversion pattern cases_thm =
-  qpat_x_assum pattern
-               (fn thm => elim_exist (ONCE_REWRITE_RULE [cases_thm] thm));
-
-fun qexistsl_tac termlist =
-	case termlist of
-	 [] => ALL_TAC
-     | t::tel => qexists_tac t \\ qexistsl_tac tel;
 (* -- *)
 
 val _ = set_trace"Goalstack.print_goal_at_top"0 handle HOL_ERR _ => set_trace"goalstack print goal at top"0

hol4/ssaPrgsScript.sml

+(**
+  We define a pseudo SSA predicate.
+  The formalization is similar to the renamedApart property in the LVC framework by Schneider, Smolka and Hack
+  http://dblp.org/rec/conf/itp/SchneiderSH15
+  Our predicate is not as fully fledged as theirs, but we especially borrow the idea of annotating
+  the program with the predicate with the set of free and defined variables
+**)
 open preamble
-open CommandsTheory
+open pred_setSyntax pred_setTheory
+open AbbrevsTheory ExpressionsTheory CommandsTheory DaisyTactics
 
 val _ = new_theory "ssaPrgs";
 
-val validVars_def = Define `
-  validVars (f:'a exp) (Vs:num set) =
-    case f of
-     | Const n => T
-     | Var v  => v IN Vs
-     | Param v  => T
-     | Unop op f1  => validVars f1 Vs
-     | Binop op f1 f2  => (validVars f1 Vs /\ validVars f2 Vs)`;
+val validVars_add = store_thm("validVars_add",
+``!(e:'a exp) Vs n.
+     domain (usedVars e) ⊆ domain Vs ==>
+     domain (usedVars e) ⊆ domain (Insert n Vs)``,
+fs [Insert_def, domain_insert, SUBSET_DEF]);
 
-(* TODO: This still allows overwriting of return value *)
-val (ssaPrg_rules, ssaPrg_ind, ssaPrg_cases) = Hol_reln `
+val validVars_non_stuck = store_thm ("validVars_non_stuck",
+  ``!(e:real exp) inVars E.
+      domain (usedVars e) ⊆ inVars /\
+      (!v. v IN (domain (usedVars e)) ==>
+         ?r. E v = SOME r) ==>
+        ? vR. eval_exp 0 E e vR``,
+  Induct_on `e` \\ once_rewrite_tac[usedVars_def]
+  \\ rpt strip_tac \\ fs []
+  >- (qexists_tac `r` \\ fs[eval_exp_cases])
+  >- (qexists_tac `v` \\ fs[eval_exp_cases]
+      \\ qexists_tac `0`
+      \\ fs[perturb_def])
+  >- (`?vR. eval_exp 0 E e vR`
+        by (first_x_assum match_mp_tac
+            \\ qexists_tac `inVars`
+            \\ fs [])
+      \\ qexists_tac `evalUnop u vR`
+      \\ fs[eval_exp_cases]
+      \\ Cases_on `u`
+      >- (disj1_tac \\ qexists_tac `vR`
+          \\ fs [])
+      >- (disj2_tac \\ qexistsl_tac [`vR`, `0`]
+          \\ fs [perturb_def]))
+  >- (`?vR1. eval_exp 0 E e vR1`
+       by (first_x_assum match_mp_tac
+           \\ qexists_tac `inVars`
+           \\ fs [domain_union])
+       \\ `?vR2. eval_exp 0 E e' vR2`
+         by (first_x_assum match_mp_tac
+           \\ qexists_tac `inVars`
+           \\ fs [domain_union])
+      \\ qexists_tac `evalBinop b vR1 vR2`
+      \\ Cases_on `b` \\ fs[eval_exp_cases]
+      \\ qexistsl_tac [`vR1`, `vR2`, `0`]
+      \\ fs[perturb_def]));
+
+(**
+  Inductive ssa predicate, following the definitions from the LVC framework,
+  see top of file for citation
+  We maintain as an invariant that if we have
+  ssa f
+**)
+val (ssa_rules, ssa_ind, ssa_cases) = Hol_reln `
   (!x e s inVars Vterm.
-    validVars e inVars /\
-    (x IN inVars = F)  /\
-    ssaPrg s (x INSERT inVars) Vterm ==>
-    ssaPrg (Let x e s) inVars Vterm) /\
+     (domain (usedVars e)) SUBSET (domain inVars) /\
+     (~ (x IN (domain inVars)))  /\
+     ssa s (Insert x inVars) Vterm ==>
+     ssa (Let x e s) inVars Vterm) /\
   (!e inVars Vterm.
-    (inVars = Vterm) ==>
-    ssaPrg (Ret e) inVars Vterm)`;
+     (domain (usedVars e))SUBSET  (domain inVars) /\
+     (inVars = Vterm) ==>
+     ssa (Ret e) inVars Vterm)`;
 
-val ssaPrg_cases =
-  map (GEN_ALL o SIMP_CONV (srw_ss()) [Once ssaPrg_cases])
-    [``ssaPrg (Let x e s) inVars Vterm``,
-     ``ssaPrg (Ret e) inVars Vterm``]
+(*
+  As usual
+*)
+val ssa_cases =
+  map (GEN_ALL o SIMP_CONV (srw_ss()) [Once ssa_cases])
+    [``ssa (Let x e s) inVars Vterm``,
+     ``ssa (Ret e) inVars Vterm``]
   |> LIST_CONJ |> curry save_thm "ssaPrg_cases";
 
+val ssa_subset_freeVars = store_thm ("ssa_subset_freeVars",
+  ``!(f:'a cmd) inVars outVars inVars'.
+      (domain inVars' = domain inVars) /\
+      ssa f inVars outVars ==>
+      ssa f inVars' outVars``,
+  once_rewrite_tac[CONJ_SYM]
+  \\ once_rewrite_tac [GSYM AND_IMP_INTRO]
+  (* THIS DOES NOT WORK *)
+  \\ recInduct ssa_ind
+  metis_tac[]);
 
 val _ = export_theory ();