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