transScript.sml 16.1 KB
Newer Older
Magnus Myreen's avatar
Magnus Myreen committed
1
open preamble
2
open simpLib (* realTheory  *)realLib RealArith stringTheory
3

Heiko Becker's avatar
Heiko Becker committed
4
open ml_translatorTheory ml_translatorLib RatProgTheory cfTacticsLib basisProgTheory
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";

Heiko Becker's avatar
Heiko Becker committed
13
val _ = translation_extends "RatProg";
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

Magnus Myreen's avatar
Magnus Myreen committed
98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207
(* improve function definitions a little *)

val const_1_over_2_pow_11_def = Define `
  const_1_over_2_pow_11 = 1 / 2 pow 11`

val const_1_over_2_pow_24_def = Define `
  const_1_over_2_pow_24 = 1 / 2 pow 24`

val const_1_over_2_pow_53_def = Define `
  const_1_over_2_pow_53 = 1 / 2 pow 53`

val const_1_over_2_pow_11_eq = EVAL ``const_1_over_2_pow_11``;
val const_1_over_2_pow_24_eq = EVAL ``const_1_over_2_pow_24``;
val const_1_over_2_pow_53_eq = EVAL ``const_1_over_2_pow_53``;

val _ = translate const_1_over_2_pow_11_eq;
val _ = translate const_1_over_2_pow_24_eq;
val _ = translate const_1_over_2_pow_53_eq;

val _ = translate (MachineTypeTheory.mTypeToQ_def
  |> REWRITE_RULE [GSYM const_1_over_2_pow_11_def,
                   GSYM const_1_over_2_pow_24_def,
                   GSYM const_1_over_2_pow_53_def]);

val isMorePrecise_eq = prove(
  ``isMorePrecise m1 m2 =
    case m1 of
    | M0 => T
    | M64 => (case m2 of M0 => F | _ => T)
    | M32 => (case m2 of M0 => F | M64 => F | _ => T)
    | M16 => (case m2 of M16 => T | _ => F)``,
  Cases_on `m1` \\ Cases_on `m2` \\ EVAL_TAC);

val _ = translate isMorePrecise_eq;

fun LET_CONV var_name body =
  (UNBETA_CONV body THENC
   RATOR_CONV (ALPHA_CONV (mk_var(var_name, type_of body))) THENC
   REWR_CONV (GSYM LET_THM));

val absIntvUpd_eq =
  IntervalArithTheory.absIntvUpd_def
  |> SPEC_ALL
  |> CONV_RULE (RAND_CONV (LET_CONV "lo1" ``IVlo iv1`` THENC
                           LET_CONV "lo2" ``IVlo iv2`` THENC
                           LET_CONV "hi1" ``IVhi iv1`` THENC
                           LET_CONV "hi2" ``IVhi iv2``));

val addInterval_eq =
  IntervalArithTheory.addInterval_def
  |> REWRITE_RULE [absIntvUpd_eq]
val _ = translate addInterval_eq

val multInterval_eq =
  IntervalArithTheory.multInterval_def
  |> REWRITE_RULE [absIntvUpd_eq]
val _ = translate multInterval_eq

val maxValueM0_def =
  let val tm = EVAL ``maxValue M0`` |> concl |> rand in
  Define `maxValueM0 = ^tm` end |> translate;

val maxValueM16_def =
  let val tm = EVAL ``maxValue M16`` |> concl |> rand in
  Define `maxValueM16 = ^tm` end |> translate;

val maxValueM32_def =
  let val tm = EVAL ``maxValue M32`` |> concl |> rand in
  Define `maxValueM32 = ^tm` end |> translate;

val maxValueM64_def =
  let val tm = EVAL ``maxValue M64`` |> concl |> rand in
  Define `maxValueM64 = ^tm` end |> translate;

val maxValue_eq = prove(
  ``maxValue m =
    case m of
    | M0 => maxValueM0
    | M16 => maxValueM16
    | M32 => maxValueM32
    | M64 => maxValueM64``,
  Cases_on `m` \\ EVAL_TAC)
  |> translate;

val minValueM0_def =
  let val tm = EVAL ``minValue M0`` |> concl |> rand in
  Define `minValueM0 = ^tm` end |> translate;

val minValueM16_def =
  let val tm = EVAL ``minValue M16`` |> concl |> rand in
  Define `minValueM16 = ^tm` end |> translate;

val minValueM32_def =
  let val tm = EVAL ``minValue M32`` |> concl |> rand in
  Define `minValueM32 = ^tm` end |> translate;

val minValueM64_def =
  let val tm = EVAL ``minValue M64`` |> concl |> rand in
  Define `minValueM64 = ^tm` end |> translate;

val minValue_eq = prove(
  ``minValue m =
    case m of
    | M0 => minValueM0
    | M16 => minValueM16
    | M32 => minValueM32
    | M64 => minValueM64``,
  Cases_on `m` \\ EVAL_TAC)
  |> translate;

Heiko Becker's avatar
Heiko Becker committed
208
val res = translate CertificateCheckerCmd_def;
209

210 211 212 213 214 215
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
216 217 218 219 220 221 222 223 224
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 (
225
  ``!e absenv P (dVars:num_set).
226
      (!v. v IN (domain dVars) ==> valid (FST (absenv (Var v)))) ==>
227
      validintervalbounds_side e absenv P dVars``,
228 229 230
  recInduct validIntervalbounds_ind
  \\ rw[]
  \\ once_rewrite_tac [validintervalbounds_side_def]
231 232 233
  \\ Cases_on `f` \\ fs []
  \\ rpt (qpat_x_assum `T` kall_tac)
  >- (once_rewrite_tac [GSYM noDivzero_def]
234 235
      \\ rpt strip_tac
      \\ rveq
236 237 238
      \\ `valid (FST(absenv e))`
           by (irule validIntervalbounds_validates_iv
               \\ qexistsl_tac [`P`, `validVars`]
239 240
               \\ fs[])
      \\ once_rewrite_tac [invertinterval_side_def]
241 242
      \\ rw_asm `absenv e = _`
      \\ Cases_on `x2` \\ rename1 `absenv e = ((elo,ehi),err)`
243 244 245 246
      \\ 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)
247
  >- (once_rewrite_tac [GSYM noDivzero_def]
248 249
      \\ rpt strip_tac
      \\ rveq
250 251
      \\ once_rewrite_tac [divideinterval_side_def]
      \\ once_rewrite_tac [invertinterval_side_def]
252
      \\ `valid (FST(absenv e0))`
253 254
           by (irule validIntervalbounds_validates_iv
               \\ qexistsl_tac [`P`, `validVars`]
255
               \\ fs[])
256 257 258 259 260 261
      \\ 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));
262

Heiko Becker's avatar
Heiko Becker committed
263 264
val precond_validIntervalboundsCmd_true = prove (
  ``!f absenv P (dVars:num_set).
265
      (!v. v IN (domain dVars) ==> valid (FST (absenv (Var v)))) ==>
266 267 268
      validintervalboundscmd_side f absenv P dVars``,
  recInduct validIntervalboundsCmd_ind
  \\ rpt strip_tac
269 270
  \\ once_rewrite_tac [validintervalboundscmd_side_def]
  \\ rpt strip_tac \\ fs []
271 272
  >- (irule precond_validIntervalbounds_true \\ fs [])
  >- (first_x_assum irule
273 274 275
      \\ rw []
      >- (imp_res_tac validIntervalbounds_validates_iv \\ fs [] \\ rfs [])
      >- (first_x_assum match_mp_tac \\ fs []))
276
  >- (irule precond_validIntervalbounds_true
277
      \\ fs []));
278

279
val precond_validErrorbound_true = prove (``
280
  !P f expTypes absenv (dVars:num_set).
281
    (!v. v IN (domain dVars) ==> valid (FST (absenv (Var v)))) /\
282
    validIntervalbounds f absenv P dVars ==>
283
    validerrorbound_side f expTypes absenv dVars ``,
284 285 286 287 288 289
  gen_tac
  \\ recInduct validErrorbound_ind
  \\ rpt gen_tac
  \\ fs[AND_IMP_INTRO]
  \\ disch_then ASSUME_TAC
  \\ once_rewrite_tac [validerrorbound_side_def]
290
  \\ once_rewrite_tac [GSYM noDivzero_def]
291
  \\ rpt gen_tac \\ disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
292 293
  \\ rpt gen_tac
  \\ ntac 2 (disch_then ASSUME_TAC)
294 295
  \\ rpt gen_tac
  \\ conj_tac
296
  >- (rpt strip_tac
297 298 299 300 301
      \\ rveq
      \\ fs[]
      \\ first_x_assum irule
      \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
      \\ rw_asm_star `absenv _ = _`
Nikita Zyuzin's avatar
Nikita Zyuzin committed
302
      \\ Cases_on `absenv x15`
303 304
      \\ fs [])
  \\ conj_tac
305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336
  >- (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 [])
337
        \\ `e2lo - err2 <> 0 /\ e2hi + err2 <> 0`
338 339 340 341 342
             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 [])
343
        \\ `abs (e2lo - err2) <> 0 /\ abs (e2hi + err2) <> 0`
344
             by (REAL_ASM_ARITH_TAC)
345
        \\ `min (abs (e2lo - err2)) (abs (e2hi + err2)) <> 0`
346 347 348 349 350
             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]
351
        \\ REAL_ASM_ARITH_TAC))
Nikita Zyuzin's avatar
Nikita Zyuzin committed
352 353 354 355
  \\ conj_tac
  >- (disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
      \\ rpt conj_tac \\ first_x_assum match_mp_tac
          \\ fs [Once validIntervalbounds_def])
356 357 358 359 360 361 362
  \\ rpt strip_tac
  \\ rveq
  \\ fs[]
  \\ first_x_assum irule
  \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
  \\ rw_asm_star `absenv _ = _`
  \\ rw_asm_star `absenv (Downcast _ _) = _`);
363 364

val precond_errorbounds_true = prove (``
365
  !P f expTypes absenv dVars.
366
    (!v. v IN domain dVars ==> valid (FST (absenv (Var v)))) /\
367
    validIntervalboundsCmd f absenv P dVars ==>
368
    validerrorboundcmd_side f expTypes absenv dVars``,
369 370 371 372
  gen_tac
  \\ recInduct validErrorboundCmd_ind
  \\ rpt strip_tac
  \\ once_rewrite_tac [validerrorboundcmd_side_def]
373
  \\ Cases_on `f` \\ fs [Once validIntervalboundsCmd_def]
374
  >- (rpt strip_tac
375 376 377
      >- (irule precond_validErrorbound_true \\ fs[]
          \\ qexists_tac `P` \\ fs [])
      >- (first_x_assum irule
378
          \\ rpt (conj_tac)
379
          \\ fs[]
380
          >- (gen_tac
381 382 383
              \\ Cases_on `v = n` \\ fs[]
              \\ rveq
              \\ rw_sym_asm `env e = _`
384
              \\ drule validIntervalbounds_validates_iv
385 386 387 388
              \\ disch_then drule \\ fs[])
          >- (Cases_on `c` \\ fs [Once validIntervalboundsCmd_def])))
  >- (irule precond_validErrorbound_true \\ fs[]
      \\ qexists_tac `P` \\ fs []));
389

390
val precond_is_true = prove (
391 392
  ``!f absenv P expTypes.
      certificatecheckercmd_side f absenv P expTypes``,
393
   once_rewrite_tac [certificatecheckercmd_side_def]
394
   \\ rpt gen_tac
395
   \\ strip_tac
396
   \\ conj_tac
397
   >- (irule precond_validIntervalboundsCmd_true
398
       \\ fs [])
399
   >- (strip_tac \\ irule precond_errorbounds_true \\ fs[]
400 401
       \\ qexists_tac `P` \\ fs []))
  |> update_precondition;
Heiko Becker's avatar
Heiko Becker committed
402

403 404 405
val res = translate str_of_num_def;

val str_of_num_side_def = fetch "-" "str_of_num_side_def";
406

407 408 409 410 411 412 413 414 415
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;
416

417
(* -- I/O routines from here onwards -- *)
418 419 420 421 422 423 424 425 426 427

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)
428
     [Conv NONE []] (STDOUT out * STDERR err * STDIN inp F)
429
     (POSTv uv. &UNIT_TYPE () uv *
430 431 432
                STDOUT (out ++ runChecker inp) *
                STDERR err *
                STDIN "" T)`,
433 434 435 436 437
  xcf "main" st
  \\ qmatch_abbrev_tac`_ frame _`
  \\ xlet`POSTv uv. &(LIST_TYPE CHAR [] uv) * frame`
  >- (xcon \\ xsimpl \\ EVAL_TAC)
  \\ qunabbrev_tac`frame`
438
  \\ xlet`POSTv cv. &LIST_TYPE CHAR inp cv * STDERR err * STDIN "" T * STDOUT out`
439
  >- (xapp \\ instantiate \\ xsimpl
440
      \\ map_every qexists_tac[`STDERR err * STDOUT out`,`F`,`inp`]
441 442 443 444 445 446 447
      \\ 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`]
448
  \\ map_every qexists_tac[`STDERR err * STDIN "" T`,`out`]
449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464
  \\ 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";
465

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