forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
basis_ffiLib.sml
157 lines (148 loc) · 6.61 KB
/
basis_ffiLib.sml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
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
(*
Automation for instantiating the FFI oracle with the
basis library functions, and removing CF separation logic.
*)
structure basis_ffiLib :> basis_ffiLib =
struct
open preamble
open ml_progLib basis_ffiTheory set_sepTheory cfHeapsBaseTheory
CommandLineProofTheory TextIOProofTheory
fun ERR f s = mk_HOL_ERR"basis_ffiLib" f s;
val basis_ffi_const = prim_mk_const{Thy="basis_ffi",Name="basis_ffi"};
val basis_ffi_tm =
list_mk_comb(basis_ffi_const,
map mk_var
(zip ["cl","fs"]
(#1(strip_fun(type_of basis_ffi_const)))))
(*This tactic proves that for a given state, parts_ok holds for the ffi and the basis_proj2*)
val prove_parts_ok_st =
qmatch_goalsub_abbrev_tac`st.ffi`
\\ `st.ffi.oracle = basis_ffi_oracle`
by( simp[Abbr`st`] \\ EVAL_TAC \\ NO_TAC)
\\ rw[cfStoreTheory.parts_ok_def]
\\ TRY ( simp[Abbr`st`] \\ EVAL_TAC \\ NO_TAC )
\\ TRY ( imp_res_tac oracle_parts \\ rfs[] \\ NO_TAC)
\\ qpat_x_assum`MEM _ basis_proj2`mp_tac
\\ simp[basis_proj2_def,basis_ffi_part_defs,cfHeapsBaseTheory.mk_proj2_def]
\\ TRY (qpat_x_assum`_ = SOME _`mp_tac)
\\ simp[basis_proj1_def,basis_ffi_part_defs,cfHeapsBaseTheory.mk_proj1_def,FUPDATE_LIST_THM]
\\ rw[] \\ rw[] \\ pairarg_tac \\ fs[FLOOKUP_UPDATE] \\ rw[]
\\ fs[FAPPLY_FUPDATE_THM,cfHeapsBaseTheory.mk_ffi_next_def]
\\ TRY PURE_FULL_CASE_TAC
\\ fs[]
\\ EVERY (map imp_res_tac (CONJUNCTS basis_ffi_length_thms))
\\ fs[fs_ffi_no_ffi_div,cl_ffi_no_ffi_div]
\\ srw_tac[DNF_ss][] \\ simp[basis_ffi_oracle_def];
(* TODO
* - the functionality should be the same when we want a RUNTIME postcond
* with a custom precondition. *)
local
val heap_thms = [COMMANDLINE_precond, STDIO_precond];
val heap_thms2 = [COMMANDLINE_precond, STDIO_precond, RUNTIME_precond];
val user_thms = ref ([]: thm list);
fun build_set [] = raise(ERR"subset_basis_st""no STDOUT in precondition")
| build_set [th] = th
| build_set (th1::th2::ths) =
let
val th = MATCH_MP append_hprop (CONJ th1 th2)
val th = CONV_RULE(LAND_CONV EVAL)th
val th = MATCH_MP th TRUTH |> SIMP_RULE (srw_ss()) [UNION_EMPTY]
val th = (CONV_RULE(RAND_CONV (pred_setLib.UNION_CONV EVAL)) th
handle _ => th) (* TODO quick fix *)
in build_set (th::ths) end
in
fun add_user_heap_thm thm =
(user_thms := thm :: (!user_thms);
HOL_MESG ("Adding user heap theorem:\n" ^ thm_to_string thm ^ "\n"))
val sets_thm2 = build_set heap_thms2;
val sets2 = rand (concl sets_thm2)
fun mk_user_sets_thm () = build_set (heap_thms @ (!user_thms))
end
(* This function proves the SPLIT pre-condition of call_main_thm_basis *)
fun subset_basis_st st precond sets sets_thm =
let
val to_inst = free_vars sets
val goal = pred_setSyntax.mk_subset(sets,st)
val tac = (
fs[cfStoreTheory.st2heap_def, cfStoreTheory.FFI_part_NOT_IN_store2heap,
cfStoreTheory.Mem_NOT_IN_ffi2heap, cfStoreTheory.ffi2heap_def]
\\ qmatch_goalsub_abbrev_tac`parts_ok ffii (basis_proj1,basis_proj2)`
\\ `parts_ok ffii (basis_proj1,basis_proj2)`
by (fs[Abbr`ffii`] \\ prove_parts_ok_st)
\\ fs[Abbr`ffii`]
\\ EVAL_TAC
\\ rw[cfAppTheory.store2heap_aux_append_many,INJ_MAP_EQ_IFF,INJ_DEF,FLOOKUP_UPDATE]
\\ rw[cfStoreTheory.store2heap_aux_def]
)
val (subgoals,_) = tac ([],goal)
fun mk_mapping (x,y) =
if tmem x to_inst then SOME (x |-> y) else
if tmem y to_inst then SOME (y |-> x) else NONE
fun safe_dest_eq tm =
if boolSyntax.is_eq tm then boolSyntax.dest_eq tm else
Lib.tryfind boolSyntax.dest_eq (boolSyntax.strip_disj tm)
handle HOL_ERR _ =>
raise(ERR"subset_basis_st"("Could not prove heap subgoal: "^(Parse.term_to_string tm)))
val s =
List.mapPartial (mk_mapping o safe_dest_eq o #2) subgoals
val goal' = Term.subst s goal
val th = prove(goal',tac)
val th =
MATCH_MP SPLIT_exists (CONJ (INST s sets_thm) th)
val length_hyps = mapfilter (assert listSyntax.is_length o lhs) (hyp th)
|> map EVAL
in
foldl (uncurry PROVE_HYP) th length_hyps
end;
fun whole_prog_thm st name spec =
let
val call_ERR = ERR "whole_prog_thm"
val whole_prog_spec_tm = spec |> concl |> strip_imp |> snd |> strip_comb |> fst
val (whole_prog_spec_thm,sets_term,sets_theorem) =
if same_const whole_prog_spec_tm ``whole_prog_spec`` orelse
same_const whole_prog_spec_tm ``whole_prog_spec2``
then
let
val sets_thm = mk_user_sets_thm ()
val sets = rand (concl sets_thm)
val thm =
if same_const whole_prog_spec_tm ``whole_prog_spec`` then
whole_prog_spec_semantics_prog
else
whole_prog_spec2_semantics_prog
in
(thm, sets, sets_thm)
end
else if same_const whole_prog_spec_tm ``whole_prog_ffidiv_spec`` then
(whole_prog_spec_semantics_prog_ffidiv,sets2,sets_thm2)
else raise(call_ERR "Conclusion must be a whole_prog_spec or whole_prog_spec2 or whole_prog_ffidiv_spec")
val ffi_v = st |> get_Decls_thm |> concl |> free_vars
|> first (fn v => fst (dest_var v) = "ffi")
val s_th = (st |> get_Decls_thm |> GEN ffi_v |> ISPEC basis_ffi_tm) |> SPEC_ALL
val th =
whole_prog_spec_thm
|> (fn th => MATCH_MP th s_th handle HOL_ERR _ =>
MATCH_MP th (PURE_ONCE_REWRITE_RULE [GSYM same_eval_state] s_th)
|> PURE_REWRITE_RULE [same_eval_state])
|> SPEC(stringSyntax.fromMLstring name)
|> CONV_RULE(QUANT_CONV(LAND_CONV(LAND_CONV EVAL THENC SIMP_CONV std_ss [])))
|> CONV_RULE(HO_REWR_CONV UNWIND_FORALL_THM1)
|> C HO_MATCH_MP spec
|> SIMP_RULE bool_ss [option_case_def, set_sepTheory.SEP_CLAUSES]
(* TS: what is this doing? why not call remove_snocs? *)
val prog_with_snoc = th |> concl |> find_term listSyntax.is_snoc
val prog_rewrite = EVAL prog_with_snoc
val th = PURE_REWRITE_RULE[prog_rewrite] th
val (split,precondh1) = th |> concl |> dest_imp |> #1 |> strip_exists |> #2 |> dest_conj
val precond = rator precondh1
val st = split |> rator |> rand
val SPLIT_thm = subset_basis_st st precond sets_term sets_theorem
val th = PART_MATCH_A (#1 o dest_imp) th (concl SPLIT_thm)
val th = MATCH_MP th SPLIT_thm
val th = DISCH_ALL th
|> REWRITE_RULE [AND_IMP_INTRO]
|> CONV_RULE ((RATOR_CONV o RAND_CONV) (SIMP_CONV std_ss [LENGTH]))
|> REWRITE_RULE [GSYM AND_IMP_INTRO]
|> UNDISCH_ALL
in (th,rhs(concl prog_rewrite)) end;
end