transScript.sml 12.9 KB
Newer Older
Magnus Myreen's avatar
Magnus Myreen committed
1
open preamble
2 3 4
open simpLib realTheory realLib RealArith stringTheory

open ml_translatorTheory ml_translatorLib realProgTheory cfTacticsLib ioProgLib
Magnus Myreen's avatar
Magnus Myreen committed
5

6 7 8 9
open AbbrevsTheory ExpressionsTheory RealSimpsTheory ExpressionAbbrevsTheory
     ErrorBoundsTheory IntervalArithTheory DaisyTactics IntervalValidationTheory
     EnvironmentsTheory CommandsTheory ssaPrgsTheory ErrorValidationTheory
     CertificateCheckerTheory daisyParserTheory
Magnus Myreen's avatar
Magnus Myreen committed
10 11 12

val _ = new_theory "trans";

13
val _ = translation_extends "realProg";
Magnus Myreen's avatar
Magnus Myreen committed
14

15 16 17 18
val _ = temp_overload_on("abs",``real$abs``);
val _ = temp_overload_on("max",``real$max``);
val _ = temp_overload_on("min",``real$min``);

19 20 21 22
val check_rec_def = Define `
  check_rec (input:Token list) (num_fun:num)=
  case num_fun of
    | SUC n' =>
23
      (case dParse input of
24 25
         | SOME ((dCmd, P, A, Gamma),NIL) =>
           if CertificateCheckerCmd dCmd A P Gamma
26 27
           then "True\n"
           else "False\n"
28 29
         | SOME ((dCmd, P, A, Gamma), residual) =>
           if CertificateCheckerCmd dCmd A P Gamma
30 31 32 33 34
           then check_rec residual n'
           else "False\n"
         | NONE => pp input(*"parse failure\n"*))
    | _ => "failure num of functions"`;

35
val check_def = Define `
36
check (f:real cmd) (P:precond) (A:analysisResult) Gamma (n:num) =
37
case n of
38
 | SUC n' => (CertificateCheckerCmd f A P Gamma /\ check f P A Gamma n')
39 40 41 42 43 44 45
 | _ => T`

val check_all_def = Define `
  check_all (num_fun:num) (iters:num) (input:Token list) =
    case num_fun of
      | SUC n =>
        (case (dParse input) of
46 47
          | SOME ((f,P,A, Gamma), residual) =>
            if (check f P A Gamma iters)
48 49 50 51 52 53 54
                then case residual of
                      | a:: b => check_all n iters residual
                      | NIL => "True\n"
                else "False\n"
          | NONE => "Failure: Parse\n")
      | _ => "Failure: Number of Functions in certificate\n"`;

55 56
val runChecker_def = Define `
  runChecker (input:tvarN) =
57
    let tokList = lex input in
58
        case tokList of
59 60
            (* FIRST: number of iterations, SECOND: number of functions *)
          | DCONST n :: DCONST m :: tokRest => check_all m n tokRest
61
          | _ => "failure no num of functions"`;
62

Magnus Myreen's avatar
Magnus Myreen committed
63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83
(* for recursive translation *)

fun def_of_const tm = let
  val res = dest_thy_const tm handle HOL_ERR _ =>
              failwith ("Unable to translate: " ^ term_to_string tm)
  val name = (#Name res)
  fun def_from_thy thy name =
    DB.fetch thy (name ^ "_pmatch") handle HOL_ERR _ =>
    DB.fetch thy (name ^ "_def") handle HOL_ERR _ =>
    DB.fetch thy (name ^ "_DEF") handle HOL_ERR _ =>
    DB.fetch thy name
  val def = def_from_thy "termination" name handle HOL_ERR _ =>
            def_from_thy (#Thy res) name handle HOL_ERR _ =>
            failwith ("Unable to find definition of " ^ name)
  val def = def |> CONV_RULE (DEPTH_CONV BETA_CONV)
  in def end

val _ = (find_def_for_const := def_of_const);

(* / for recursive translation *)

84
val _ = translate lookup_def;
85

86
val _ = translate subspt_eq;
Heiko Becker's avatar
Heiko Becker committed
87

88
val res = translate parseExp_def;
Heiko Becker's avatar
Heiko Becker committed
89

90 91 92 93 94
val parseexp_side_true = prove(
  ``!x. parseexp_side x = T``,
  recInduct parseExp_ind \\ rw []
  \\ once_rewrite_tac [fetch "-" "parseexp_side_def"] \\ rw [])
  |> update_precondition;
Heiko Becker's avatar
Heiko Becker committed
95

96
val res = translate dParse_def;
97

Heiko Becker's avatar
Heiko Becker committed
98
val res = translate CertificateCheckerCmd_def;
99

100 101 102 103 104 105
val invertinterval_side_def = fetch "-" "invertinterval_side_def";

val divideinterval_side_def = fetch "-" "divideinterval_side_def";

val validintervalbounds_side_def = fetch "-" "validintervalbounds_side_def";

Heiko Becker's avatar
Heiko Becker committed
106 107 108 109 110 111 112 113 114
val validintervalboundscmd_side_def = fetch "-" "validintervalboundscmd_side_def";

val validerrorbound_side_def = fetch "-" "validerrorbound_side_def";

val validerrorboundcmd_side_def = fetch "-" "validerrorboundcmd_side_def";

val certificatecheckercmd_side_def = fetch "-" "certificatecheckercmd_side_def";

val precond_validIntervalbounds_true = prove (
115
  ``!e absenv P (dVars:num_set).
116
      (!v. v IN (domain dVars) ==> valid (FST (absenv (Var v)))) ==>
117
      validintervalbounds_side e absenv P dVars``,
118 119 120
  recInduct validIntervalbounds_ind
  \\ rw[]
  \\ once_rewrite_tac [validintervalbounds_side_def]
121 122 123
  \\ Cases_on `f` \\ fs []
  \\ rpt (qpat_x_assum `T` kall_tac)
  >- (once_rewrite_tac [GSYM noDivzero_def]
124 125
      \\ rpt strip_tac
      \\ rveq
126 127 128
      \\ `valid (FST(absenv e))`
           by (irule validIntervalbounds_validates_iv
               \\ qexistsl_tac [`P`, `validVars`]
129 130
               \\ fs[])
      \\ once_rewrite_tac [invertinterval_side_def]
131 132
      \\ rw_asm `absenv e = _`
      \\ Cases_on `x2` \\ rename1 `absenv e = ((elo,ehi),err)`
133 134 135 136
      \\ qpat_x_assum `!v. _` kall_tac
      \\ qpat_x_assum `!intv. _` kall_tac
      \\ fs [IVlo_def, IVhi_def, valid_def, noDivzero_def]
      \\ REAL_ASM_ARITH_TAC)
137
  >- (once_rewrite_tac [GSYM noDivzero_def]
138 139
      \\ rpt strip_tac
      \\ rveq
140 141
      \\ once_rewrite_tac [divideinterval_side_def]
      \\ once_rewrite_tac [invertinterval_side_def]
142
      \\ `valid (FST(absenv e0))`
143 144
           by (irule validIntervalbounds_validates_iv
               \\ qexistsl_tac [`P`, `validVars`]
145
               \\ fs[])
146 147 148 149 150 151
      \\ Cases_on `x4` \\ rename1 `absenv e0 = ((elo,ehi),err)`
      \\ qpat_x_assum `!v. _` kall_tac
      \\ rpt (qpat_x_assum `!intv. _` kall_tac)
      \\ qpat_x_assum `absenv e0 = _` (fn thm => fs [thm])
      \\ fs [IVlo_def, IVhi_def, valid_def, noDivzero_def]
      \\ REAL_ASM_ARITH_TAC));
152

Heiko Becker's avatar
Heiko Becker committed
153 154
val precond_validIntervalboundsCmd_true = prove (
  ``!f absenv P (dVars:num_set).
155
      (!v. v IN (domain dVars) ==> valid (FST (absenv (Var v)))) ==>
156 157 158
      validintervalboundscmd_side f absenv P dVars``,
  recInduct validIntervalboundsCmd_ind
  \\ rpt strip_tac
159 160
  \\ once_rewrite_tac [validintervalboundscmd_side_def]
  \\ rpt strip_tac \\ fs []
161 162
  >- (irule precond_validIntervalbounds_true \\ fs [])
  >- (first_x_assum irule
163 164 165
      \\ rw []
      >- (imp_res_tac validIntervalbounds_validates_iv \\ fs [] \\ rfs [])
      >- (first_x_assum match_mp_tac \\ fs []))
166
  >- (irule precond_validIntervalbounds_true
167
      \\ fs []));
168

169
val precond_validErrorbound_true = prove (``
170
  !P f expTypes absenv (dVars:num_set).
171
    (!v. v IN (domain dVars) ==> valid (FST (absenv (Var v)))) /\
172
    validIntervalbounds f absenv P dVars ==>
173
    validerrorbound_side f expTypes absenv dVars ``,
174 175 176 177 178 179
  gen_tac
  \\ recInduct validErrorbound_ind
  \\ rpt gen_tac
  \\ fs[AND_IMP_INTRO]
  \\ disch_then ASSUME_TAC
  \\ once_rewrite_tac [validerrorbound_side_def]
180
  \\ once_rewrite_tac [GSYM noDivzero_def]
181
  \\ rpt gen_tac \\ disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
182 183
  \\ rpt gen_tac
  \\ ntac 2 (disch_then ASSUME_TAC)
184 185
  \\ rpt gen_tac
  \\ conj_tac
186
  >- (rpt strip_tac
187 188 189 190 191
      \\ rveq
      \\ fs[]
      \\ first_x_assum irule
      \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
      \\ rw_asm_star `absenv _ = _`
Nikita Zyuzin's avatar
Nikita Zyuzin committed
192
      \\ Cases_on `absenv x15`
193 194
      \\ fs [])
  \\ conj_tac
195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226
  >- (disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
      \\ conj_tac
      >- (conj_tac \\ first_x_assum match_mp_tac
          \\ fs [Once validIntervalbounds_def])
      >- (disch_then ASSUME_TAC
          \\ rpt gen_tac
          \\ disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
          \\ rpt gen_tac
          \\ disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
          \\ rpt (disch_then ASSUME_TAC)
          \\ rveq
          \\ rename1 `absenv (Binop Div e1 e2) = (ivDiv, errDiv)`
          \\ rename1 `absenv e1 = (ive1,err1)`
          \\ Cases_on `ive1` \\ rename1 `absenv e1 = ((e1lo,e1hi), err1)`
          \\ rename1 `absenv e2 = (ive2,err2)`
          \\ Cases_on `ive2` \\ rename1 `absenv e2 = ((e2lo,e2hi), err2)`
          \\ rewrite_tac [divideinterval_side_def, widenInterval_def, minAbsFun_def, invertinterval_side_def, IVlo_def, IVhi_def]
          \\ `valid (FST(absenv e1)) /\ valid (FST(absenv e2))`
               by (conj_tac \\ drule validIntervalbounds_validates_iv
                   >- (disch_then match_mp_tac
                       \\ qexists_tac `P`
                       \\ fs [Once validIntervalbounds_def])
                   >- (disch_then match_mp_tac
                       \\ qexists_tac `P`
                       \\ fs [Once validIntervalbounds_def]))
          \\ rw_asm `absenv e1 = _`
          \\ rw_asm `absenv e2 = _`
          \\ qpat_x_assum `!v. _` kall_tac
          \\ `0 <= err2`
               by (drule err_always_positive
                 \\ disch_then (fn thm => qspecl_then [`e2lo,e2hi`, `err2`] match_mp_tac thm)
                 \\ fs [])
227
        \\ `e2lo - err2 <> 0 /\ e2hi + err2 <> 0`
228 229 230 231 232
             by (fs [noDivzero_def, IVlo_def, IVhi_def, widenInterval_def, valid_def]
                 \\ conj_tac \\ REAL_ASM_ARITH_TAC)
        \\ `noDivzero (SND (FST (absenv e2))) (FST (FST (absenv e2)))`
             by (drule validIntervalbounds_noDivzero_real
                 \\ fs [])
233
        \\ `abs (e2lo - err2) <> 0 /\ abs (e2hi + err2) <> 0`
234
             by (REAL_ASM_ARITH_TAC)
235
        \\ `min (abs (e2lo - err2)) (abs (e2hi + err2)) <> 0`
236 237 238 239 240
             by (fs [min_def]
                 \\ Cases_on `abs (e2lo - err2) <= abs (e2hi + err2)`
                 \\ fs [] \\ REAL_ASM_ARITH_TAC)
        \\ qpat_x_assum `absenv e2 = _` (fn thm => fs [thm])
        \\ fs [noDivzero_def, valid_def, IVhi_def, IVlo_def]
241
        \\ REAL_ASM_ARITH_TAC))
Nikita Zyuzin's avatar
Nikita Zyuzin committed
242 243 244 245
  \\ conj_tac
  >- (disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
      \\ rpt conj_tac \\ first_x_assum match_mp_tac
          \\ fs [Once validIntervalbounds_def])
246 247 248 249 250 251 252
  \\ rpt strip_tac
  \\ rveq
  \\ fs[]
  \\ first_x_assum irule
  \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
  \\ rw_asm_star `absenv _ = _`
  \\ rw_asm_star `absenv (Downcast _ _) = _`);
253 254

val precond_errorbounds_true = prove (``
255
  !P f expTypes absenv dVars.
256
    (!v. v IN domain dVars ==> valid (FST (absenv (Var v)))) /\
257
    validIntervalboundsCmd f absenv P dVars ==>
258
    validerrorboundcmd_side f expTypes absenv dVars``,
259 260 261 262
  gen_tac
  \\ recInduct validErrorboundCmd_ind
  \\ rpt strip_tac
  \\ once_rewrite_tac [validerrorboundcmd_side_def]
263
  \\ Cases_on `f` \\ fs [Once validIntervalboundsCmd_def]
264
  >- (rpt strip_tac
265 266 267
      >- (irule precond_validErrorbound_true \\ fs[]
          \\ qexists_tac `P` \\ fs [])
      >- (first_x_assum irule
268
          \\ rpt (conj_tac)
269
          \\ fs[]
270
          >- (gen_tac
271 272 273
              \\ Cases_on `v = n` \\ fs[]
              \\ rveq
              \\ rw_sym_asm `env e = _`
274
              \\ drule validIntervalbounds_validates_iv
275 276 277 278
              \\ disch_then drule \\ fs[])
          >- (Cases_on `c` \\ fs [Once validIntervalboundsCmd_def])))
  >- (irule precond_validErrorbound_true \\ fs[]
      \\ qexists_tac `P` \\ fs []));
279

280
val precond_is_true = prove (
281 282
  ``!f absenv P expTypes.
      certificatecheckercmd_side f absenv P expTypes``,
283
   once_rewrite_tac [certificatecheckercmd_side_def]
284
   \\ rpt gen_tac
285
   \\ strip_tac
286
   \\ conj_tac
287
   >- (irule precond_validIntervalboundsCmd_true
288
       \\ fs [])
289
   >- (strip_tac \\ irule precond_errorbounds_true \\ fs[]
290 291
       \\ qexists_tac `P` \\ fs []))
  |> update_precondition;
Heiko Becker's avatar
Heiko Becker committed
292

293 294 295
val res = translate str_of_num_def;

val str_of_num_side_def = fetch "-" "str_of_num_side_def";
296

297 298 299 300 301 302 303 304 305
val str_of_num_side_true = prove (``!a. str_of_num_side a``,
recInduct str_of_num_ind
\\ rpt strip_tac \\ simp [str_of_num_side_def]
\\ rpt strip_tac
\\ `n MOD 10 < 10` by (match_mp_tac MOD_LESS \\ fs [])
\\ match_mp_tac LESS_TRANS
\\ qexists_tac `10 + 48` \\ fs []) |> update_precondition;

val res = translate runChecker_def;
306

307
(* -- I/O routines from here onwards -- *)
308 309 310 311 312 313 314 315 316 317

val main = process_topdecs`
  fun main u =
    write_list (runchecker (read_all []))`;

val res = ml_prog_update(ml_progLib.add_prog main I)
val st = get_ml_prog_state()

val main_spec = Q.store_thm("main_spec",
  `app (p:'ffi ffi_proj) ^(fetch_v "main" st)
318
     [Conv NONE []] (STDOUT out * STDERR err * STDIN inp F)
319
     (POSTv uv. &UNIT_TYPE () uv *
320 321 322
                STDOUT (out ++ runChecker inp) *
                STDERR err *
                STDIN "" T)`,
323 324 325 326 327
  xcf "main" st
  \\ qmatch_abbrev_tac`_ frame _`
  \\ xlet`POSTv uv. &(LIST_TYPE CHAR [] uv) * frame`
  >- (xcon \\ xsimpl \\ EVAL_TAC)
  \\ qunabbrev_tac`frame`
328
  \\ xlet`POSTv cv. &LIST_TYPE CHAR inp cv * STDERR err * STDIN "" T * STDOUT out`
329
  >- (xapp \\ instantiate \\ xsimpl
330
      \\ map_every qexists_tac[`STDERR err * STDOUT out`,`F`,`inp`]
331 332 333 334 335 336 337
      \\ xsimpl)
  \\ qmatch_abbrev_tac`_ frame _`
  \\ qmatch_goalsub_abbrev_tac`STRCAT _ res`
  \\ xlet`POSTv xv. &LIST_TYPE CHAR res xv * frame`
  >- (xapp \\ instantiate \\ xsimpl)
  \\ xapp \\ instantiate
  \\ simp[Abbr`frame`]
338
  \\ map_every qexists_tac[`STDERR err * STDIN "" T`,`out`]
339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354
  \\ xsimpl);

val spec = main_spec |> UNDISCH_ALL |> add_basis_proj;
val name = "main"
val (semantics_thm,prog_tm) = call_thm st name spec;

val entire_program_def = Define`entire_program = ^prog_tm`;

val semantics_entire_program =
  semantics_thm
  |> PURE_ONCE_REWRITE_RULE[GSYM entire_program_def]
  |> REWRITE_RULE [APPEND]
  |> CONV_RULE(RENAME_VARS_CONV["io_events"])
  |> DISCH_ALL |> GEN_ALL
  |> CONV_RULE(RENAME_VARS_CONV["inp","cls"])
  |> curry save_thm "semantics_entire_program";
355

Magnus Myreen's avatar
Magnus Myreen committed
356
val _ = export_theory();