Alpha renaming, coherent doc and port expressions to new semantics

coq/Expressions.v

 (**
-Formalization of the base expression language for the daisy framework
-Required in all files, since we will always reason about expressions.
+  Formalization of the base expression language for the daisy framework
  **)
 Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals.
-Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet Daisy.IntervalArithQ Daisy.IntervalArith.
+Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet.
 
 (**
   Expressions will use binary operators.
@@ -99,12 +98,9 @@ Definition perturb (r:R) (e:R) :=
 
 (**
 Define expression evaluation relation parametric by an "error" epsilon.
-This value will be used later to express float computations using a perturbation
-of the real valued computation by (1 + delta), where |delta| <= machine epsilon.
-
-It is important that variables are not perturbed when loading from an environment.
-This is the case, since loading a float value should not increase an additional error.
-Unary negation is special! We do not have a new error here since IEE 754 gives us a sign bit
+The result value expresses float computations according to the IEEE standard,
+using a perturbation of the real valued computation by (1 + delta), where
+|delta| <= machine epsilon.
 **)
 Inductive eval_exp (eps:R) (E:env) :(exp R) -> R -> Prop :=
 | Var_load x v:
@@ -126,7 +122,11 @@ Inductive eval_exp (eps:R) (E:env) :(exp R) -> R -> Prop :=
     eval_exp eps E f2 v2 ->
     eval_exp eps E (Binop op f1 f2) (perturb (evalBinop op v1 v2) delta).
 
-Fixpoint freeVars (V:Type) (e:exp V) :NatSet.t :=
+(**
+  Define the set of "used" variables of an expression to be the set of variables
+  occuring in it
+**)
+Fixpoint usedVars (V:Type) (e:exp V) :NatSet.t :=
   match e with
   | Var _ x => NatSet.singleton x
   | Unop u e1 => freeVars e1
@@ -135,7 +135,7 @@ Fixpoint freeVars (V:Type) (e:exp V) :NatSet.t :=
   end.
 
 (**
-If |delta| <= 0 then perturb v delta is exactly v.
+  If |delta| <= 0 then perturb v delta is exactly v.
 **)
 Lemma delta_0_deterministic (v:R) (delta:R):
   (Rabs delta <= 0)%R ->
@@ -172,8 +172,7 @@ Qed.
 Helping lemma. Needed in soundness proof.
 For each evaluation of using an arbitrary epsilon, we can replace it by
 evaluating the subexpressions and then binding the result values to different
-variables in the Eironment.
-This relies on the property that variables are not perturbed as opposed to parameters
+variables in the Environment.
 **)
 Lemma binary_unfolding b f1 f2 eps E vF:
   eval_exp eps E (Binop b f1 f2) vF ->
@@ -218,15 +217,15 @@ Proof.
     inversion H2; subst; auto.
 Qed.
 
-
 (**
   Using the parametric expressions, define boolean expressions for conditionals
 **)
 Inductive bexp (V:Type) : Type :=
   leq: exp V -> exp V -> bexp V
 | less: exp V -> exp V -> bexp V.
+
 (**
-  Define evaluation of booleans for reals
+  Define evaluation of boolean expressions
  **)
 Inductive bval (eps:R) (E:env): (bexp R) -> Prop -> Prop :=
   leq_eval (f1:exp R) (f2:exp R) (v1:R) (v2:R):

coq/Infra/Abbrevs.v

@@ -16,7 +16,6 @@ define them to automatically unfold upon simplification.
  **)
 Definition interval:Type := R * R.
 Definition err:Type := R.
-Definition ann:Type := interval * err.
 Definition mkInterval (ivlo:R) (ivhi:R) := (ivlo,ivhi).
 Definition IVlo (intv:interval) := fst intv.
 Definition IVhi (intv:interval) := snd intv.
@@ -36,9 +35,6 @@ Arguments mkIntv _ _/.
 Arguments ivlo _ /.
 Arguments ivhi _ /.
 
-Ltac iv_assert iv name:=
-  assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
-
 (**
 Later we will argue about program preconditions.
 Define a precondition to be a function mapping numbers (resp. variables) to intervals.
@@ -50,10 +46,15 @@ Definition precond :Type := nat -> intv.
  **)
 Definition env := nat -> option R.
 
+(**
+  The empty environment must return NONE for every variable
+**)
 Definition emptyEnv:env := fun _ => None.
+
 (**
   Define environment update function as abbreviation, for variable environments
 **)
+
 Definition updEnv (x:nat) (v: R) (E:env) (y:nat) :=
   if y =? x
   then Some v

coq/Infra/Ltacs.v

@@ -2,6 +2,10 @@
 Require Import Coq.Bool.Bool Coq.Reals.Reals.
 Require Import Daisy.Infra.RealSimps Daisy.Infra.NatSet.
 
+
+Ltac iv_assert iv name:=
+  assert (exists ivlo ivhi, iv = (ivlo, ivhi)) as name by (destruct iv; repeat eexists; auto).
+
 (** Automatic translation and destruction of conjuctinos with andb into Props **)
 Ltac andb_to_prop H :=
   apply Is_true_eq_left in H;

hol4/abbrevsScript.sml → hol4/AbbrevsScript.sml

+(**
+  This file contains some type abbreviations, to ease writing.
+ **)
 open preamble
-open realTheory realLib
+open realTheory realLib sptreeTheory
 
-val _ = new_theory "abbrevs";
+val _ = new_theory "Abbrevs";
 (**
 For the moment we need only one interval type in HOL, since we do not have the
 problem of computability as we have it in Coq
@@ -10,8 +13,6 @@ val _ = type_abbrev("interval", ``:real#real``);
 val IVlo_def = Define `IVlo (iv:interval) = FST iv`;
 val IVhi_def = Define `IVhi (iv:interval) = SND iv`;
 
-val _ = type_abbrev("ann", ``:interval#real``);
-
 (**
 Later we will argue about program preconditions.
 Define a precondition to be a function mapping numbers (resp. variables) to intervals.
@@ -19,15 +20,25 @@ Define a precondition to be a function mapping numbers (resp. variables) to inte
 val _ = type_abbrev ("precond", ``:num->interval``);
 
 (**
-  Abbreviations for the environment types
+  Abbreviation for the type of a variable environment, which should be a partial function
 **)
 val _ = type_abbrev("env",``:num->real option``);
 
 (**
-  Define environment update function as abbreviation.
+  The empty environment must return NONE for every variable
+**)
+val emptyEnv_def = Define `
+  emptyEnv (x:num) = NONE`;
+
+(**
+  Define environment update function as abbreviation, for variable environments
 **)
 val updEnv_def = Define `
 updEnv (x:num) (v:real) (E:env) (y:num) :real option = if y = x then SOME v else E y`;
 
+(**
+  Abbreviation for insertion into "num_set" type
+**)
+val Insert_def = Define `Insert x V  = insert x () V`;
 
 val - = export_theory();

hol4/CertificateCheckerScript.sml

@@ -6,7 +6,7 @@
 **)
 open preamble
 open simpLib realTheory realLib RealArith
-open abbrevsTheory expressionsTheory RealSimpsTheory
+open AbbrevsTheory ExpressionsTheory RealSimpsTheory
 open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
 open IntervalValidationTheory ErrorValidationTheory
 

hol4/CommandsScript.sml

@@ -3,7 +3,7 @@
  **)
 open preamble
 open simpLib realTheory realLib RealArith
-open abbrevsTheory ExpressionAbbrevsTheory
+open AbbrevsTheory ExpressionAbbrevsTheory
 
 val _ = new_theory "Commands";
 

hol4/EnvironmentsScript.sml

 open preamble
 open simpLib realTheory realLib RealArith
-open abbrevsTheory ExpressionAbbrevsTheory CommandsTheory
+open AbbrevsTheory ExpressionAbbrevsTheory CommandsTheory
 
 val _ = new_theory "Environments";
 

hol4/ErrorBoundsScript.sml

 (**
-Proofs of general bounds on the error of arithmetic expressions.
+Proofs of general bounds on the error of arithmetic Expressions.
 This shortens soundness proofs later.
 Bounds are explained in section 5, Deriving Computable Error Bounds
 **)
 open preamble
 open simpLib realTheory realLib RealArith
-open abbrevsTheory expressionsTheory RealSimpsTheory
+open AbbrevsTheory ExpressionsTheory RealSimpsTheory
 open ExpressionAbbrevsTheory EnvironmentsTheory
 
 val _ = new_theory "ErrorBounds";

hol4/ErrorValidationScript.sml

@@ -8,7 +8,7 @@
  **)
 open preamble
 open simpLib realTheory realLib RealArith
-open abbrevsTheory expressionsTheory RealSimpsTheory
+open AbbrevsTheory ExpressionsTheory RealSimpsTheory
 open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
 open IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory
 

hol4/ExpressionsScript.sml

-open preamble
-open realTheory realLib
-open abbrevsTheory
+(**
+  Formalization of the base expression language for the daisy framework
+ **)
+open preamble miscTheory
+open realTheory realLib sptreeTheory
+open AbbrevsTheory
+
 val _ = ParseExtras.temp_tight_equality()
 
-val _ = new_theory "expressions";
+val _ = new_theory "Expressions";
 
 (**
   Expressions will use binary operators.
@@ -36,14 +40,10 @@ Errors are added in the expression evaluation level later
 val evalUnop_def = Define `
   evalUnop Neg v = - v /\
   evalUnop Inv v = inv(v:real)`
+
 (**
-  Define expressions parametric over some value type 'v.  Will ease
-  reasoning about different instantiations later.  Note that we
-  differentiate between whether we use a variable from the environment
-  or a parameter.  Parameters do not have error bounds in the
-  invariants, so they must be perturbed, but variables from the
-  program will be perturbed upon binding, so we do not need to perturb
-  them.
+  Define Expressions parametric over some value type 'v.
+  Will ease reasoning about different instantiations later.
 **)
 val _ = Datatype `
   exp = Var num
@@ -58,30 +58,34 @@ val perturb_def = Define `
   perturb (r:real) (e:real) = r * (1 + e)`
 
 (**
-  Define expression evaluation relation parametric by an "error"
-  delta.  This value will be used later to express float computations
-  using a perturbation of the real valued computation by (1 + d)
+Define expression evaluation relation parametric by an "error" epsilon.
+The result value expresses float computations according to the IEEE standard,
+using a perturbation of the real valued computation by (1 + delta), where
+|delta| <= machine epsilon.
 **)
 val (eval_exp_rules, eval_exp_ind, eval_exp_cases) = Hol_reln `
-   (!eps E x v.
-           E x = SOME v ==>
-           eval_exp eps E (Var x) v) /\
-   (!eps E n delta.
-         abs delta <= eps ==>
-         eval_exp eps E (Const n) (perturb n delta)) /\
-    (!eps E f1 v1.
-          eval_exp eps E f1 v1 ==>
-          eval_exp eps E (Unop Neg f1) (evalUnop Neg v1)) /\
-    (!eps E f1 v1 delta.
-          abs delta <= eps /\
-          eval_exp eps E f1 v1 ==>
-          eval_exp eps E (Unop Inv f1) (perturb (evalUnop Inv v1) delta)) /\
-    (!eps E b f1 f2 v1 v2 delta.
-          abs delta <= eps /\
-          eval_exp eps E f1 v1 /\
-          eval_exp eps E f2 v2 ==>
-          eval_exp eps E (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta))`;
+  (!eps E x v.
+     E x = SOME v ==>
+     eval_exp eps E (Var x) v) /\
+  (!eps E n delta.
+     abs delta <= eps ==>
+     eval_exp eps E (Const n) (perturb n delta)) /\
+  (!eps E f1 v1.
+     eval_exp eps E f1 v1 ==>
+     eval_exp eps E (Unop Neg f1) (evalUnop Neg v1)) /\
+  (!eps E f1 v1 delta.
+     abs delta <= eps /\
+     eval_exp eps E f1 v1 ==>
+     eval_exp eps E (Unop Inv f1) (perturb (evalUnop Inv v1) delta)) /\
+  (!eps E b f1 f2 v1 v2 delta.
+     abs delta <= eps /\
+     eval_exp eps E f1 v1 /\
+     eval_exp eps E f2 v2 ==>
+     eval_exp eps E (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta))`;
 
+(**
+  Generate a better case lemma
+**)
 val eval_exp_cases =
   map (GEN_ALL o SIMP_CONV (srw_ss()) [Once eval_exp_cases])
     [``eval_exp eps E (Var v) res``,
@@ -90,10 +94,28 @@ val eval_exp_cases =
      ``eval_exp eps E (Binop n e1 e2) res``]
   |> LIST_CONJ |> curry save_thm "eval_exp_cases";
 
+(**
+  Define the set of "used" variables of an expression to be the set of variables
+  occuring in it
+**)
+val usedVars_def = Define `
+  usedVars (e: 'a exp) :num_set =
+    case e of
+      | Var x => insert x () (LN)
+      | Unop u e1 => usedVars e1
+      | Binop b e1 e2 => union (usedVars e1) (usedVars e2)
+      | _ => LN`;
+
+(**
+  If |delta| <= 0 then perturb v delta is exactly v.
+**)
 val delta_0_deterministic = store_thm("delta_0_deterministic",
   ``!(v:real) (delta:real). abs delta <= 0 ==> perturb v delta = v``,
   fs [perturb_def,ABS_BOUNDS,REAL_LE_ANTISYM]);
 
+(**
+Evaluation with 0 as machine epsilon is deterministic
+**)
 val meps_0_deterministic = store_thm("meps_0_deterministic",
   ``!(e: real exp) v1:real v2:real E.
       eval_exp (&0) E e v1 /\ eval_exp (&0) E e v2 ==> v1 = v2``,
@@ -104,22 +126,33 @@ val meps_0_deterministic = store_thm("meps_0_deterministic",
 (**
 Helping lemma. Needed in soundness proof.
 For each evaluation of using an arbitrary epsilon, we can replace it by
-evaluating the subexpressions and then binding the result values to different
+evaluating the subExpressions and then binding the result values to different
 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) E (v:real).
+  ``!(b:binop) (e1:(real)exp) (e2:(real)exp) (eps:real) E (v:real).
       (eval_exp eps E (Binop b e1 e2) v <=>
-        (?(v1:real) (v2:real).
-           eval_exp eps E e1 v1 /\
-           eval_exp eps E e2 v2 /\
-           eval_exp eps (updEnv 2 v2 (updEnv 1 v1 E)) (Binop b (Var 1) (Var 2)) v))``,
+      (?(v1:real) (v2:real).
+         eval_exp eps E e1 v1 /\
+         eval_exp eps E e2 v2 /\
+         eval_exp eps (updEnv 2 v2 (updEnv 1 v1 emptyEnv)) (Binop b (Var 1) (Var 2)) v))``,
+  fs [updEnv_def, eval_exp_cases,APPLY_UPDATE_THM,PULL_EXISTS]
+  \\ metis_tac []);
+
+(**
+  Analogous lemma for unary expressions
+**)
+val unary_unfolding = store_thm("unary_unfolding",
+  ``!(u:unop) (e1:(real)exp) (eps:real) E (v:real).
+       (eval_exp eps E (Unop Inv e1) v <=>
+       (?(v1:real).
+          eval_exp eps E e1 v1 /\
+          eval_exp eps (updEnv 1 v1 emptyEnv) (Unop Inv (Var 1)) v))``,
   fs [updEnv_def, eval_exp_cases,APPLY_UPDATE_THM,PULL_EXISTS]
   \\ metis_tac []);
 
 (*
-  Using the parametric expressions, define boolean expressions for conditionals
+  Using the parametric Expressions, define boolean Expressions for conditionals
 *)
 val _ = Datatype `
   bexp = Leq ('v exp) ('v exp)
@@ -144,7 +177,9 @@ val bval_exp_cases =
      ``bval eps E (Less e1 e2) res``]
   |> LIST_CONJ |> curry save_thm "bval_exp_cases";
 
-(* Simplify arithmetic later by making > >= only abbreviations *)
+(**
+  Simplify arithmetic later by making > >= only abbreviations
+**)
 val _ = overload_on("Gr",``\(e1:('v)exp). \(e2:('v)exp). Less e2 e1``);
 val _ = overload_on("Greq",``\(e1:('v)exp). \(e2:('v)exp). Leq e2 e1``);
 

hol4/Holmakefile

-INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple common
+INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple Infra
 OPTIONS = QUIT_ON_FAILURE
 
 ifdef POLY
@@ -18,7 +18,7 @@ BARE_THYS = BasicProvers Defn HolKernel Parse Tactic monadsyntax \
      optionTheory pairLib pairTheory pred_setTheory \
      quantHeuristicsLib relationTheory res_quanTheory rich_listTheory \
      sortingTheory sptreeTheory stringTheory sumTheory wordsTheory \
-     simpLib realTheory realLib RealArith common/preamble
+     simpLib realTheory realLib RealArith Infra/preamble
 
 DEPS = $(patsubst %,%.uo,$(BARE_THYS1)) $(PARENTHEAP)
 

hol4/ExpressionAbbrevsScript.sml → hol4/Infra/ExpressionAbbrevsScript.sml

 
 open preamble
-open expressionsTheory
+open ExpressionsTheory
 
 val _ = new_theory "ExpressionAbbrevs"
 

hol4/IntervalArithScript.sml

@@ -4,7 +4,7 @@
 **)
 open preamble
 open realTheory realLib RealArith
-open abbrevsTheory expressionsTheory RealSimpsTheory;
+open AbbrevsTheory ExpressionsTheory RealSimpsTheory;
 
 val _ = new_theory "IntervalArith";
 

hol4/IntervalValidationScript.sml

@@ -7,7 +7,7 @@
 **)
 open preamble
 open simpLib realTheory realLib RealArith
-open abbrevsTheory expressionsTheory RealSimpsTheory
+open AbbrevsTheory ExpressionsTheory RealSimpsTheory
 open ExpressionAbbrevsTheory IntervalArithTheory CommandsTheory ssaPrgsTheory
 
 val _ = new_theory "IntervalValidation";