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
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
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2016 *)
(* *)
(* Michaël Armand *)
(* Benjamin Grégoire *)
(* Chantal Keller *)
(* *)
(* Inria - École Polytechnique - Université Paris-Sud *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
open Entries
open Declare
open Decl_kinds
open SmtMisc
open CoqTerms
open SmtForm
open SmtAtom
open SmtTrace
open SmtCertif
let euf_checker_modules = [ ["SMTCoq";"Trace";"Euf_Checker"] ]
let certif_ops = CoqTerms.make_certif_ops euf_checker_modules
let cCertif = gen_constant euf_checker_modules "Certif"
let ccertif = gen_constant euf_checker_modules "certif"
let cchecker = gen_constant euf_checker_modules "checker"
let cchecker_correct = gen_constant euf_checker_modules "checker_correct"
let cchecker_b_correct =
gen_constant euf_checker_modules "checker_b_correct"
let cchecker_b = gen_constant euf_checker_modules "checker_b"
let cchecker_eq_correct =
gen_constant euf_checker_modules "checker_eq_correct"
let cchecker_eq = gen_constant euf_checker_modules "checker_eq"
(* Given an SMT-LIB2 file and a certif, build the corresponding objects *)
let compute_roots roots last_root =
let r = ref last_root in
while (has_prev !r) do
r := prev !r
done;
let rec find_root i root = function
| [] -> assert false
| t::q -> if Form.equal t root then (i,q) else find_root (i+1) root q in
let rec used_roots acc i roots r =
if isRoot r.kind then
match r.value with
| Some [root] ->
let (j,roots') = find_root i root roots in
used_roots (j::acc) (j+1) roots' (next r)
| _ -> assert false
else
acc in
used_roots [] 0 roots !r
let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf, roots, max_id, confl) =
let (tres, last_root) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) certif_ops confl in
let certif =
mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
let ce4 = Structures.mkConst certif in
let _ = declare_constant trace (DefinitionEntry ce4, IsDefinition Definition) in
let used_roots = compute_roots roots last_root in
let roots =
let res = Array.make (List.length roots + 1) (mkInt 0) in
let i = ref 0 in
List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
Structures.mkArray (Lazy.force cint, res) in
let used_roots =
let l = List.length used_roots in
let res = Array.make (l + 1) (mkInt 0) in
let i = ref (l-1) in
List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots;
mklApp cSome [|mklApp carray [|Lazy.force cint|]; Structures.mkArray (Lazy.force cint, res)|] in
let ce3 = Structures.mkConst roots in
let _ = declare_constant root (DefinitionEntry ce3, IsDefinition Definition) in
let ce3' = Structures.mkConst used_roots in
let _ = declare_constant used_root (DefinitionEntry ce3', IsDefinition Definition) in
let t_i' = make_t_i rt in
let t_func' = make_t_func ro t_i' in
let ce5 = Structures.mkConst t_i' in
let _ = declare_constant t_i (DefinitionEntry ce5, IsDefinition Definition) in
let ce6 = Structures.mkConst t_func' in
let _ = declare_constant t_func (DefinitionEntry ce6, IsDefinition Definition) in
let ce1 = Structures.mkConst (Atom.interp_tbl ra) in
let _ = declare_constant t_atom (DefinitionEntry ce1, IsDefinition Definition) in
let ce2 = Structures.mkConst (snd (Form.interp_tbl rf)) in
let _ = declare_constant t_form (DefinitionEntry ce2, IsDefinition Definition) in
()
(* Given an SMT-LIB2 file and a certif, build the corresponding theorem *)
let interp_roots roots =
let interp = Form.interp_to_coq (Atom.interp_to_coq (Hashtbl.create 17)) (Hashtbl.create 17) in
match roots with
| [] -> Lazy.force ctrue
| f::roots -> List.fold_left (fun acc f -> mklApp candb [|acc; interp f|]) (interp f) roots
let build_certif (rt, ro, ra, rf, roots, max_id, confl) =
let (tres,last_root) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) certif_ops confl in
let certif =
mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
let used_roots = compute_roots roots last_root in
let used_rootsCstr =
let l = List.length used_roots in
let res = Array.make (l + 1) (mkInt 0) in
let i = ref (l-1) in
List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots;
mklApp cSome [|mklApp carray [|Lazy.force cint|]; Structures.mkArray (Lazy.force cint, res)|] in
let rootsCstr =
let res = Array.make (List.length roots + 1) (mkInt 0) in
let i = ref 0 in
List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
Structures.mkArray (Lazy.force cint, res) in
let t_atom = Atom.interp_tbl ra in
let t_form = snd (Form.interp_tbl rf) in
let t_i = make_t_i rt in
let t_func = make_t_func ro t_i in
(rootsCstr, used_rootsCstr, certif, t_atom, t_form, t_i, t_func)
let theorem name ((rt, ro, ra, rf, roots, max_id, confl) as p) =
let (rootsCstr, used_rootsCstr, certif, t_atom, t_form, t_i, t_func) = build_certif p in
let theorem_concl = mklApp cnot [|mklApp cis_true [|interp_roots roots|]|] in
let theorem_proof =
Term.mkLetIn (mkName "used_roots", used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|], (*7*)
Term.mkLetIn (mkName "t_atom", t_atom, mklApp carray [|Lazy.force catom|], (*6*)
Term.mkLetIn (mkName "t_form", t_form, mklApp carray [|Lazy.force cform|], (*5*)
Term.mkLetIn (mkName "d", rootsCstr, mklApp carray [|Lazy.force cint|], (*4*)
Term.mkLetIn (mkName "c", certif, Lazy.force ccertif, (*3*)
Term.mkLetIn (mkName "t_i", t_i, mklApp carray [|Lazy.force ctyp_eqb|], (*2*)
Term.mkLetIn (mkName "t_func", t_func, mklApp carray [|mklApp ctval [|t_i|]|], (*1*)
mklApp cchecker_correct
[|Term.mkRel 2; Term.mkRel 1; Term.mkRel 6; Term.mkRel 5; Term.mkRel 4; Term.mkRel 7; Term.mkRel 3;
vm_cast_true
(mklApp cchecker [|Term.mkRel 2; Term.mkRel 1; Term.mkRel 6; Term.mkRel 5; Term.mkRel 4; Term.mkRel 7; Term.mkRel 3|])|]))))))) in
let ce = Structures.mkConst theorem_proof in
let _ = declare_constant name (DefinitionEntry ce, IsDefinition Definition) in
()
(* Given an SMT-LIB2 file and a certif, call the checker *)
let checker ((rt, ro, ra, rf, roots, max_id, confl) as p) =
let (rootsCstr, used_rootsCstr, certif, t_atom, t_form, t_i, t_func) = build_certif p in
let tm = mklApp cchecker [|t_i; t_func; t_atom; t_form; rootsCstr; used_rootsCstr; certif|] in
let res = Vnorm.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in
Format.eprintf " = %s\n : bool@."
(if Term.eq_constr res (Lazy.force CoqTerms.ctrue) then
"true" else "false")
(* Tactic *)
let build_body rt ro ra rf l b (max_id, confl) =
let (tres,_) = SmtTrace.to_coq Form.to_coq certif_ops confl in
let certif =
mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
let t_atom = Atom.interp_tbl ra in
let t_form = snd (Form.interp_tbl rf) in
let t_i = make_t_i rt in
let t_func = make_t_func ro t_i in
let ntatom = mkName "t_atom" in
let ntform = mkName "t_form" in
let nc = mkName "c" in
let nti = mkName "t_i" in
let ntfunc = mkName "t_func" in
let vtatom = Term.mkRel 5 in
let vtform = Term.mkRel 4 in
let vc = Term.mkRel 3 in
let vti = Term.mkRel 2 in
let vtfunc = Term.mkRel 1 in
Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
Term.mkLetIn (nc, certif, Lazy.force ccertif,
Term.mkLetIn (nti, Structures.lift 3 t_i, mklApp carray [|Lazy.force ctyp_eqb|],
Term.mkLetIn (ntfunc, Structures.lift 4 t_func, mklApp carray [|mklApp ctval [|t_i|]|],
mklApp cchecker_b_correct
[|vti;vtfunc;vtatom; vtform; l; b; vc;
vm_cast_true (mklApp cchecker_b [|vti;vtfunc;vtatom;vtform;l;b;vc|])|])))))
let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) =
let (tres,_) = SmtTrace.to_coq Form.to_coq certif_ops confl in
let certif =
mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
let t_atom = Atom.interp_tbl ra in
let t_form = snd (Form.interp_tbl rf) in
let t_i = make_t_i rt in
let t_func = make_t_func ro t_i in
let ntatom = mkName "t_atom" in
let ntform = mkName "t_form" in
let nc = mkName "c" in
let nti = mkName "t_i" in
let ntfunc = mkName "t_func" in
let vtatom = Term.mkRel 5 in
let vtform = Term.mkRel 4 in
let vc = Term.mkRel 3 in
let vti = Term.mkRel 2 in
let vtfunc = Term.mkRel 1 in
Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
Term.mkLetIn (nc, certif, Lazy.force ccertif,
Term.mkLetIn (nti, Structures.lift 3 t_i, mklApp carray [|Lazy.force ctyp_eqb|],
Term.mkLetIn (ntfunc, Structures.lift 4 t_func, mklApp carray [|mklApp ctval [|t_i|]|],
mklApp cchecker_eq_correct
[|vti;vtfunc;vtatom; vtform; l1; l2; l; vc;
vm_cast_true (mklApp cchecker_eq [|vti;vtfunc;vtatom;vtform;l1;l2;l;vc|])|])))))
let get_arguments concl =
let f, args = Term.decompose_app concl in
match args with
| [ty;a;b] when (Term.eq_constr f (Lazy.force ceq)) && (Term.eq_constr ty (Lazy.force cbool)) -> a, b
| [a] when (Term.eq_constr f (Lazy.force cis_true)) -> a, Lazy.force ctrue
| _ -> failwith ("Verit.tactic: can only deal with equality over bool")
let make_proof call_solver rt ro rf l =
let fl = Form.flatten rf l in
let root = SmtTrace.mkRootV [l] in
call_solver rt ro fl (root,l)
let tactic call_solver rt ro ra rf env sigma t =
let (forall_let, concl) = Term.decompose_prod_assum t in
let env = Environ.push_rel_context forall_let env in
let a, b = get_arguments concl in
let body =
if ((Term.eq_constr b (Lazy.force ctrue)) || (Term.eq_constr b (Lazy.force cfalse))) then
let l = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf a in
let l' = if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in
let max_id_confl = make_proof call_solver rt ro rf l' in
build_body rt ro ra rf (Form.to_coq l) b max_id_confl
else
let l1 = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf a in
let l2 = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf b in
let l = Form.neg (Form.get rf (Fapp(Fiff,[|l1;l2|]))) in
let max_id_confl = make_proof call_solver rt ro rf l in
build_body_eq rt ro ra rf (Form.to_coq l1) (Form.to_coq l2) (Form.to_coq l) max_id_confl in
let compose_lam_assum forall_let body =
List.fold_left (fun t rd -> Term.mkLambda_or_LetIn rd t) body forall_let in
let res = compose_lam_assum forall_let body in
let cuts = Btype.get_cuts rt in
List.fold_right (fun (eqn, eqt) tac ->
Structures.tclTHENLAST (Structures.assert_before (Names.Name eqn) eqt) tac
) cuts (Structures.vm_cast_no_check res)
|
