1 2 3(* 4quietdec := true; 5loadPath := 6 (concat Globals.HOLDIR "/examples/dev/sw") :: 7 (concat Globals.HOLDIR "/examples/elliptic/arm") :: 8 (concat Globals.HOLDIR "/examples/elliptic/spec") :: 9 (concat Globals.HOLDIR "/examples/elliptic/sep") :: 10 (concat Globals.HOLDIR "/examples/elliptic/swsep") :: 11 !loadPath; 12 13map load ["swsepLib", "elliptic_exampleTheory"]; 14show_assums := true; 15*) 16 17open swsepLib; 18open ellipticTheory 19open elliptic_exampleTheory; 20open mechReasoning; 21 22(* 23quietdec := false; 24*) 25 26fun sep_compile def prove_equiv = 27 let 28 val comp = pp_compile def prove_equiv; 29 val _ = print "Translating specification to separation logic\n"; 30 val spec = spec_sep comp 31 in 32 spec 33 end 34 35 36 37val ex1_field_neg_eval = REWRITE_RULE [ex1_prime_def, 38 example1_prime_def] ex1_field_neg_def 39val ex1_field_neg_spec = sep_compile ex1_field_neg_eval true 40 41 42val ex1_field_add_eval = REWRITE_RULE [ex1_prime_def, 43 example1_prime_def] ex1_field_add_def 44val ex1_field_add_spec = sep_compile ex1_field_add_eval true; 45 46 47val ex1_field_sub_eval = REWRITE_RULE [ex1_field_neg_eval,ex1_field_add_eval] ex1_field_sub_def 48val ex1_field_sub_spec___pre = sep_compile ex1_field_sub_eval false; 49 50 51val ex1_field_sub_spec = PROVE_HYP ( 52 prove (hd (hyp ex1_field_sub_spec___pre), 53 54REWRITE_TAC[FUN_EQ_THM] THEN 55Cases_on `x` THEN 56SIMP_TAC std_ss [ex1_field_sub_eval] THEN 57Cases_on `r = 0w` THEN ( 58 ASM_SIMP_TAC std_ss [WORD_ADD_0, LET_THM] THEN 59 WORDS_TAC 60))) ex1_field_sub_spec___pre 61 62 63 64 65val WORD_LO___MEASURE = store_thm ("WORD_LO___MEASURE", 66 ``word_lo = measure w2n``, 67 SIMP_TAC std_ss [FUN_EQ_THM, prim_recTheory.measure_def, 68 relationTheory.inv_image_def, WORD_LO] ); 69 70val fact_def = Hol_defn "fact" 71 `fact (x:word32,a:word32) = if x=0w then a else fact(x-1w, x*a)`; 72 73val (fact_def, fact_ind) = 74Defn.tprove (fact_def, 75 TotalDefn.WF_REL_TAC `inv_image $<+ (\(v1:word32,v2:word32). v1)` THENL [ 76 SIMP_TAC std_ss [WORD_LO___MEASURE, prim_recTheory.WF_measure], 77 SIMP_TAC std_ss [WORD_LO, WORD_PRED_THM] 78 ]); 79 80val fact_spec___pre = sep_compile fact_def false; 81 82val fact_spec = 83 PROVE_HYP 84 (prove (hd (hyp fact_spec___pre), 85 SIMP_TAC std_ss [FUN_EQ_THM, FORALL_PROD] THEN 86 HO_MATCH_MP_TAC fact_ind THEN 87 REPEAT STRIP_TAC THEN 88 ONCE_REWRITE_TAC [fact_def, WHILE] THEN 89 RW_TAC std_ss [] THEN 90 Q.PAT_ASSUM `~(x = 0w) ==> P x` MP_TAC THEN 91 WORDS_TAC THEN 92 ASM_SIMP_TAC std_ss [])) 93 fact_spec___pre 94 95 96(* 97IR.inline_funcs := ["f1"] 98*) 99 100val def1 = Define `f1 (x:word32) = x + 1w`; 101val def2 = Define `f2 (x:word32) = x + f1(x) + 1w`; 102val def3 = Define `f3 (x:word32) = f2(x) + 1w`; 103val def4 = Define `f4 (x:word32, y:word32) = fact(x, 2w) + 1w`; 104val def5 = Define `f5 (x:word32) = if (x = 0w) then (f1 x + 1w) else x`; 105 106val comp1 = pp_compile def1 false 107val comp2 = pp_compile def2 false 108val comp3 = pp_compile def3 false 109val comp4 = pp_compile def4 false 110val comp5 = pp_compile def5 false 111