Prove soundness of command intevrals in HOL4

hol4/CommandsScript.sml

+(**
+ Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework
+ **)
+open preamble
+open simpLib realTheory realLib RealArith
+open abbrevsTheory ExpressionAbbrevsTheory
+
+val _ = new_theory "Commands";
+
+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))`;
+
+val (bstep_rules, bstep_ind, bstep_cases) = Hol_reln `
+  (! x e s s' VarEnv ParamEnv P v eps VarEnv2.
+    eval_exp eps VarEnv ParamEnv P e v /\
+    bstep s (updEnv x v VarEnv) ParamEnv P eps s' VarEnv2 ==>
+    bstep (Let x e s) VarEnv ParamEnv P eps s' VarEnv2) /\
+  (! e VarEnv ParamEnv P v eps.
+    eval_exp eps VarEnv ParamEnv P e v ==>
+    bstep (Ret e) VarEnv ParamEnv P eps Nop (updEnv 0 v VarEnv))`;
+
+val bstep_cases =
+  map (GEN_ALL o SIMP_CONV (srw_ss()) [Once bstep_cases])
+    [``bstep (Let x e s) VarEnv ParamEnv P eps s' VarEnv2``,
+     ``bstep (Ret e) VarEnv ParamEnv P eps Nop VarEnv2``]
+  |> LIST_CONJ |> curry save_thm "bstep_cases";
+
+val _ = export_theory ();

hol4/EnvironmentsScript.sml

+open preamble
+open simpLib realTheory realLib RealArith
+open abbrevsTheory ExpressionAbbrevsTheory CommandsTheory
+
+val (approxEnv_rules, approxEnv_ind, approxEnv_cases) = Hol_reln `
+  (!(E:env) (A:analysisResult). approxEnv E A E) /\
+  (!(E1:env) (E2:env) (A:analysisResult) v1 v2 x.
+    approxEnv E1 A E2 /\
+    (abs (v1 - v2) <= SND (A (Var x))) ==>
+    approxEnv (updEnv x v1 E1) A (updEnv x v2 E2))`;

hol4/ErrorBoundsScript.sml

@@ -6,7 +6,7 @@ Bounds are explained in section 5, Deriving Computable Error Bounds
 open preamble
 open simpLib realTheory realLib RealArith
 open abbrevsTheory expressionsTheory RealSimpsTheory
-open ExpressionAbbrevsTheory
+open ExpressionAbbrevsTheory EnvironmentsTheory
 
 val _ = new_theory "ErrorBounds";
 

hol4/expressionsScript.sml

@@ -64,36 +64,38 @@ perturb (r:real) (e:real) = r * (1 + e)`
   using a perturbation of the real valued computation by (1 + d)
 **)
 val (eval_exp_rules, eval_exp_ind, eval_exp_cases) = Hol_reln `
-   (!eps E (P:num->(real # real)) x.
-         eval_exp eps E P (Var x) (E x)) /\
-   (!eps E P x delta.
+   (!eps VarEnv ParamEnv P x.
+         eval_exp eps VarEnv ParamEnv P (Var x) (VarEnv x)) /\
+   (!eps VarEnv ParamEnv P x delta delta_lo delta_hi.
          abs delta <= eps /\
-         FST (P x) <= perturb (E x) delta /\
-         perturb (E x) delta <= SND (P x) ==>
-         eval_exp eps E P (Param x) (perturb (E x) delta)) /\
-   (!eps E P delta.
+         abs delta_lo <= eps /\
+         abs delta_hi <= eps /\
+         perturb (FST (P x)) delta_lo  <= perturb (ParamEnv x) delta /\
+         perturb (ParamEnv x) delta <= perturb (SND (P x)) delta_hi ==>
+         eval_exp eps VarEnv ParamEnv P (Param x) (perturb (ParamEnv x) delta)) /\
+   (!eps VarEnv ParamEnv P n delta.
          abs delta <= eps ==>
-         eval_exp eps E P (Const n) (perturb n delta)) /\
-    (!eps E P f1 v1.
-          eval_exp eps E P f1 v1 ==>
-          eval_exp eps E P (Unop Neg f1) (evalUnop Neg v1)) /\
-    (!eps E P f1 v1 delta.
+         eval_exp eps VarEnv ParamEnv P (Const n) (perturb n delta)) /\
+    (!eps VarEnv ParamEnv P f1 v1.
+          eval_exp eps VarEnv ParamEnv P f1 v1 ==>
+          eval_exp eps VarEnv ParamEnv P (Unop Neg f1) (evalUnop Neg v1)) /\
+    (!eps VarEnv ParamEnv P f1 v1 delta.
           abs delta <= eps /\
-          eval_exp eps E P f1 v1 ==>
-          eval_exp eps E P (Unop Inv f1) (perturb (evalUnop Inv v1) delta)) /\
-    (!eps E P b f1 f2 v1 v2 delta.
+          eval_exp eps VarEnv ParamEnv P f1 v1 ==>
+          eval_exp eps VarEnv ParamEnv P (Unop Inv f1) (perturb (evalUnop Inv v1) delta)) /\
+    (!eps VarEnv ParamEnv P b f1 f2 v1 v2 delta.
           abs delta <= eps /\
-          eval_exp eps E P f1 v1 /\
-          eval_exp eps E P f2 v2 ==>
-          eval_exp eps E P (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta))`;
+          eval_exp eps VarEnv ParamEnv P f1 v1 /\
+          eval_exp eps VarEnv ParamEnv P f2 v2 ==>
+          eval_exp eps VarEnv ParamEnv P (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta))`;
 
 val eval_exp_cases =
   map (GEN_ALL o SIMP_CONV (srw_ss()) [Once eval_exp_cases])
-    [``eval_exp eps E P (Var v) res``,
-     ``eval_exp eps E P (Param v) res``,
-     ``eval_exp eps E P (Const n) res``,
-     ``eval_exp eps E P (Unop u e) res``,
-     ``eval_exp eps E P (Binop n e1 e2) res``]
+    [``eval_exp eps VarEnv ParamEnv P (Var v) res``,
+     ``eval_exp eps VarEnv ParamEnv P (Param v) res``,
+     ``eval_exp eps VarEnv ParamEnv P (Const n) res``,
+     ``eval_exp eps VarEnv ParamEnv P (Unop u e) res``,
+     ``eval_exp eps VarEnv ParamEnv P (Binop n e1 e2) res``]
   |> LIST_CONJ |> curry save_thm "eval_exp_cases";
 
 val delta_0_deterministic = store_thm("delta_0_deterministic",
@@ -101,8 +103,8 @@ val delta_0_deterministic = store_thm("delta_0_deterministic",
   fs [perturb_def,ABS_BOUNDS,REAL_LE_ANTISYM]);
 
 val meps_0_deterministic = store_thm("meps_0_deterministic",
-  ``!(e: real exp) v1:real v2:real E P.
-      eval_exp (&0) E P e v1 /\ eval_exp (&0) E P e v2 ==> v1 = v2``,
+  ``!(e: real exp) v1:real v2:real VarEnv ParamEnv P.
+      eval_exp (&0) VarEnv ParamEnv P e v1 /\ eval_exp (&0) VarEnv ParamEnv P e v2 ==> v1 = v2``,
   Induct \\ fs [eval_exp_cases]
   \\ rw [] \\ fs [delta_0_deterministic]
   \\ res_tac \\ fs []);
@@ -118,19 +120,19 @@ val _ = Datatype `
   Define evaluation of boolean expressions
 *)
 val (bval_exp_rules, bval_exp_ind, bval_exp_cases) = Hol_reln `
-  (!eps E P e1 e2 v1 v2.
-      eval_exp eps E P e1 v1 /\
-      eval_exp eps E P e2 v2 ==>
-      bval eps E P (Leq e1 e2) (v1 <= v2))/\
-  (!eps E P e1 e2 v1 v2.
-      eval_exp eps E P e1 v1 /\
-      eval_exp eps E P e2 v2 ==>
-      bval eps E P (Less e1 e2) (v1 < v2))`;
+  (!eps VarEnv ParamEnv P e1 e2 v1 v2.
+      eval_exp eps VarEnv ParamEnv P e1 v1 /\
+      eval_exp eps VarEnv ParamEnv P e2 v2 ==>
+      bval eps VarEnv ParamEnv P (Leq e1 e2) (v1 <= v2))/\
+  (!eps VarEnv ParamEnv P e1 e2 v1 v2.
+      eval_exp eps VarEnv ParamEnv P e1 v1 /\
+      eval_exp eps VarEnv ParamEnv P e2 v2 ==>
+      bval eps VarEnv ParamEnv P (Less e1 e2) (v1 < v2))`;
 
 val bval_exp_cases =
   map (GEN_ALL o SIMP_CONV (srw_ss()) [Once bval_exp_cases])
-    [``bval eps E P (Leq e1 e2) res``,
-     ``bval eps E P (Less e1 e2) res``]
+    [``bval eps VarEnv ParamEnv P (Leq e1 e2) res``,
+     ``bval eps VarEnv ParamEnv P (Less e1 e2) res``]
   |> LIST_CONJ |> curry save_thm "bval_exp_cases";
 
 (* Simplify arithmetic later by making > >= only abbreviations *)
@@ -145,12 +147,12 @@ variables in the Eironment.
 This relies on the property that variables are not perturbed as opposed to parameters
 **)
 val binary_unfolding = store_thm("binary_unfolding",
-``!(b:binop) (e1:(real)exp) (e2:(real)exp) (eps:real) (cenv:env) (P:precond) (v:real).
-      (eval_exp eps cenv P (Binop b e1 e2) v <=>
+``!(b:binop) (e1:(real)exp) (e2:(real)exp) (eps:real) VarEnv ParamEnv (P:precond) (v:real).
+      (eval_exp eps VarEnv ParamEnv P (Binop b e1 e2) v <=>
         (?(v1:real) (v2:real).
-           eval_exp eps cenv P e1 v1 /\
-           eval_exp eps cenv P e2 v2 /\
-           eval_exp eps (updEnv 2 v2 (updEnv 1 v1 cenv)) P (Binop b (Var 1) (Var 2)) v))``,
+           eval_exp eps VarEnv ParamEnv P e1 v1 /\
+           eval_exp eps VarEnv ParamEnv P e2 v2 /\
+           eval_exp eps (updEnv 2 v2 (updEnv 1 v1 VarEnv)) ParamEnv P (Binop b (Var 1) (Var 2)) v))``,
   fs [updEnv_def, eval_exp_cases,APPLY_UPDATE_THM,PULL_EXISTS]
   \\ metis_tac []);
 

hol4/ssaPrgsScript.sml

+open preamble
+open CommandsTheory
+
+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)`;
+
+(* TODO: This still allows overwriting of return value *)
+val (ssaPrg_rules, ssaPrg_ind, ssaPrg_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) /\
+  (!e inVars Vterm.
+    (inVars = Vterm) ==>
+    ssaPrg (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``]
+  |> LIST_CONJ |> curry save_thm "ssaPrg_cases";
+
+
+val _ = export_theory ();