From 3e046357e7e42d92c93b3d9eb33ca4ea323ed044 Mon Sep 17 00:00:00 2001 From: Heiko Becker Date: Wed, 29 Jun 2016 16:33:17 +0200 Subject: [PATCH] Start working on toy example proof, add coq definitions --- coq/exps.v | 85 ++++++++++++++++++++++++++++++++++++++++++++++ hol/exps.hl | 53 ++++++++++++++--------------- hol/toy_example.hl | 26 +++++++++++--- 3 files changed, 132 insertions(+), 32 deletions(-) create mode 100644 coq/exps.v diff --git a/coq/exps.v b/coq/exps.v new file mode 100644 index 0000000..b6b0fc9 --- /dev/null +++ b/coq/exps.v @@ -0,0 +1,85 @@ +(** +Formalization of the base expression language for the daisy framework + **) +Require Import Coq.Reals.Reals. +Set Implicit Arguments. +(** + Expressions will use binary operators. + Define them first +**) +Inductive binop : Type := Plus | Sub | Mult | Div. +(** + Next define an evaluation function for binary operators on reals. + Errors are added on the expression evaluation level later. + **) +Fixpoint eval_binop (o:binop) (v1:R) (v2:R) := + match o with + | Plus => Rplus v1 v2 + | Sub => Rminus v1 v2 + | Mult => Rmult v1 v2 + | Div => Rdiv v1 v2 + end. +(* + Define expressions parametric over some value type V. + Will ease reasoning about different instantiations later. +*) +Inductive exp (V:Type): Type := + Var: nat -> exp V +| Const: V -> exp V +| Binop: binop -> exp V -> exp V -> exp V. +(** + Define the machine epsilon for floating point operations. + FIXME: Currently set to 1.0 instead of the concrete value! +**) +Definition m_eps:R := 1. +(** + Define a perturbation function to ease writing of basic definitions +**) +Definition perturb (r:R) (e:R) := + Rmult r (Rplus 1 e). +(** + Define expression evaluation parametric by an "error function". + This function will be used later to express float computations using a perturbation + of the real valued computation by (1 + d) + Additionally we need an "error id" function which uniquely numbers an expression. +**) +Fixpoint eval_err (e:exp R) (err_fun:exp R-> R) (env:nat -> R) := + match e with + |Var _ n => perturb (env n) (err_fun (Var _ n)) + |Const v => perturb v (err_fun (Const v)) + |Binop op e1 e2 => let v1 := eval_err e1 err_fun env in + let v2 := eval_err e2 err_fun env in + perturb (eval_binop op v1 v2) (err_fun (Binop op e1 e2)) + end. +(** + Define real evaluation as stated above: +**) +Definition eval_real (e:exp R) (env:nat -> R) := eval_err e (fun x => R0) env. +(** + float evaluation is non-deterministic, since the perturbation is existencially quantified + --> state as predicate when float evaluation using errors is valid, related to errors +**) +Definition is_valid_err_float (err_fun: nat -> R) : Prop := + forall id, exists n:R, + (n = err_fun id \/ (Ropp n) = err_fun id) /\ + Rle (Rabs n) m_eps. +(** + 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 +**) +Fixpoint bval_SIMPS (b:bexp R) (env:nat -> R) (eval: exp R -> (nat -> R) -> R) := + match b with + |leq e1 e2 => Rle (eval e1 env) (eval e2 env) + |less e1 e2 => Rlt (eval e1 env) (eval e2 env) +end. + +(** + Simplify arithmetic later by making > >= only abbreviations +**) +Definition gr := fun (V:Type) (e1: exp V) (e2: exp V) => less e2 e1. +Definition greq := fun (V:Type) (e1:exp V) (e2: exp V) => leq e2 e1. \ No newline at end of file diff --git a/hol/exps.hl b/hol/exps.hl index 561563f..7688c66 100644 --- a/hol/exps.hl +++ b/hol/exps.hl @@ -5,6 +5,21 @@ needs "Infra/tactics.hl";; (* needs "/home/heiko/Git_Repos/hol-light/IEEE/make.ml";; *) +(* + Expressions will use binary operators. + Define them first +*) +let binop_INDUCT, binop_REC = define_type + "binop = Plus | Sub | Mult | Div ";; +(* + Define an evaluation function for binary operators. + Errors are added on the expression evaluation level later +*) +let eval_binop = new_recursive_definition binop_REC + `(eval_binop Plus v1 v2 = v1 + v2) /\ + (eval_binop Sub v1 v2 = v1 - v2) /\ + (eval_binop Mult v1 v2 = v1 * v2) /\ + (eval_binop Div v1 v2 = v1 / v2)`;; (* Define expressions parametric over some value type V. Will ease reasoning about different instantiations later. @@ -12,21 +27,16 @@ needs "Infra/tactics.hl";; let exp_INDUCT, exp_REC= define_type "exp = Var num | Const V - | Plus exp exp - | Sub exp exp - | Mult exp exp - | Div exp exp";; - + | Binop binop exp exp";; (* Define the machine epsilon for floating point operations. FIXME: Currently set to 1.0 instead of the concrete value! *) let m_eps = define `m_eps:real = (&1)`;; - (* Define a perturbation function to ease writing of basic definitions *) -let perturb_def = define `(perturb:real->real->real) = \r e. e * ((&1) + e)`;; +let perturb = define `(perturb:real->real->real) = \r e. r * ((&1) + e)`;; (* Define expression evaluation parametric by an "error function". This function will be used later to express float computations using a perturbation @@ -34,32 +44,19 @@ let perturb_def = define `(perturb:real->real->real) = \r e. e * ((&1) + e)`;; Additionally we need an "error id" function which uniquely numbers an expression. *) let eval_err = new_recursive_definition exp_REC - `(eval_err (Var name) err_fun err_id_fun env - = perturb (env name) (err_fun (err_id_fun (Var name)))) /\ - (eval_err (Const v) err_fun err_id_fun env - = perturb v (err_fun (err_id_fun (Const v)))) /\ - (eval_err (Plus e1 e2) err_fun err_id_fun env - = perturb ( - (eval_err e1 err_fun err_id_fun env) + (eval_err e2 err_fun err_id_fun env)) - (err_fun (err_id_fun (Plus e1 e2)))) /\ - (eval_err (Sub e1 e2) err_fun err_id_fun env - = perturb ( - (eval_err e1 err_fun err_id_fun env) - (eval_err e2 err_fun err_id_fun env)) - (err_fun (err_id_fun (Sub e1 e2)))) /\ - (eval_err (Mult e1 e2)err_fun err_id_fun env - = perturb ( - (eval_err e1 err_fun err_id_fun env) * (eval_err e2 err_fun err_id_fun env)) - (err_fun (err_id_fun (Mult e1 e2)))) /\ - (eval_err (Div e1 e2) err_fun err_id_fun env - = perturb ( - (eval_err e1 err_fun err_id_fun env) / (eval_err e2 err_fun err_id_fun env)) - (err_fun (err_id_fun (Div e1 e2))))`;; + `(eval_err (Var name) err_fun env + = perturb (env name) (err_fun (Var name))) /\ + (eval_err (Const v) err_fun env + = perturb v (err_fun (Const v))) /\ + (eval_err (Binop binop e1 e2) err_fun env + = perturb (eval_binop binop (eval_err e1 err_fun env) (eval_err e2 err_fun env)) + (err_fun (Binop binop e1 e2)))`;; (* Define real evaluation as stated above: *) let eval_real = define - `eval_real (e:(real)exp) (env:num->real) = eval_err e (\x. &0) (\x. &0) env`;; + `eval_real (e:(real)exp) (env:num->real) = eval_err e (\x. &0) env`;; (* float evaluation is non-deterministic, since the perturbation is existencially quantified diff --git a/hol/toy_example.hl b/hol/toy_example.hl index 7b7a997..9a60fa2 100644 --- a/hol/toy_example.hl +++ b/hol/toy_example.hl @@ -1,5 +1,5 @@ (* - + Toy Example to get a feeling for what needs to be done for certificate checking *) needs "daisy_lang.hl";; @@ -8,7 +8,25 @@ let prg = define Let 1 (Mult (Const (&2)) (Var 2)) (Ret (Mult (Const (&3)) (Var 1)))`;; -let prg_float = define - `prg_float:(float)cmd = +let abs_err = define `abs_err = &1`;; (* TODO: FIXME *) + +g `!fl_err_fun err_ids env env_final_real env_final_float. + is_valid_err_float fl_err_fun ==> + bstep prg env eval_real Nop env_final_real ==> + bstep prg env (\e. eval_err e fl_err_fun err_ids) Nop env_final_float ==> + abs (env_final_real 0 - env_final_float 0) <= abs_err`;; -g ` +e (REWRITE_TAC [prg]);; +e (INTRO_TAC + "!fl_err_fun err_ids env env_final_real env_final_float; + error_fl_valid; terminates_real; terminates_float");; +e (SUBGOAL_THEN `?v. eval_real (Mult (Const (&2)) (Var 2)) env = v` (LABEL_TAC "exists_val"));; +e (REWRITE_TAC[eval_real;eval_err]);; +e (REWRITE_TAC[perturb]);; +e (EXISTS_TAC `&0`);; +e (REAL_ARITH_TAC);; +e (REMOVE_THEN "exists_val" (DESTRUCT_TAC "@v. val_def"));; +e (SUBGOAL_THEN `bstep (Ret (Mult (Const (&3)) (Var 1))) (upd_env 1 v env) eval_real Nop env_final_real` ASSUME_TAC);; +e (ASM_MESON_TAC[bstep_CASES]);; +e (REWRITE_TAC[bstep_CASES]);; +b();; -- GitLab