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
|
Require Export Crypto.SpecificGen.GF2519_32Reflective.Common.
Require Import Crypto.SpecificGen.GF2519_32BoundedCommon.
Require Import Crypto.Reflection.Z.Interpretations64.
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Reflection.SmartMap.
Require Import Crypto.Util.Tactics.
Local Opaque Interp.
Local Notation eta_and x := (let (a, b) := x in a, let (a, b) := x in b) (only parsing).
Lemma Expr9_4Op_correct_and_bounded
ropW op (ropZ_sig : rexpr_9_4op_sig op)
(Hbounds : correct_and_bounded_genT ropW ropZ_sig)
(H0 : forall x012345678
(x012345678
:= (eta_fe2519_32W (fst (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
eta_fe2519_32W (snd (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
eta_fe2519_32W (snd (fst (fst (fst (fst (fst (fst x012345678))))))),
eta_fe2519_32W (snd (fst (fst (fst (fst (fst x012345678)))))),
eta_fe2519_32W (snd (fst (fst (fst (fst x012345678))))),
eta_fe2519_32W (snd (fst (fst (fst x012345678)))),
eta_fe2519_32W (snd (fst (fst x012345678))),
eta_fe2519_32W (snd (fst x012345678)),
eta_fe2519_32W (snd x012345678)))
(Hx012345678
: is_bounded (fe2519_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
/\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
/\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst x012345678)))))))) = true
/\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst x012345678))))))) = true
/\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst x012345678)))))) = true
/\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst x012345678))))) = true
/\ is_bounded (fe2519_32WToZ (snd (fst (fst x012345678)))) = true
/\ is_bounded (fe2519_32WToZ (snd (fst x012345678))) = true
/\ is_bounded (fe2519_32WToZ (snd x012345678)) = true),
let (Hx0, Hx12345678) := (eta_and Hx012345678) in
let (Hx1, Hx2345678) := (eta_and Hx12345678) in
let (Hx2, Hx345678) := (eta_and Hx2345678) in
let (Hx3, Hx45678) := (eta_and Hx345678) in
let (Hx4, Hx5678) := (eta_and Hx45678) in
let (Hx5, Hx678) := (eta_and Hx5678) in
let (Hx6, Hx78) := (eta_and Hx678) in
let (Hx7, Hx8) := (eta_and Hx78) in
let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in
match LiftOption.of'
(Interp (@BoundedWordW.interp_op) ropW
(LiftOption.to' (Some args)))
with
| Some _ => True
| None => False
end)
(H1 : forall x012345678
(x012345678
:= (eta_fe2519_32W (fst (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
eta_fe2519_32W (snd (fst (fst (fst (fst (fst (fst (fst x012345678)))))))),
eta_fe2519_32W (snd (fst (fst (fst (fst (fst (fst x012345678))))))),
eta_fe2519_32W (snd (fst (fst (fst (fst (fst x012345678)))))),
eta_fe2519_32W (snd (fst (fst (fst (fst x012345678))))),
eta_fe2519_32W (snd (fst (fst (fst x012345678)))),
eta_fe2519_32W (snd (fst (fst x012345678))),
eta_fe2519_32W (snd (fst x012345678)),
eta_fe2519_32W (snd x012345678)))
(Hx012345678
: is_bounded (fe2519_32WToZ (fst (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
/\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst (fst x012345678))))))))) = true
/\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst (fst x012345678)))))))) = true
/\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst (fst x012345678))))))) = true
/\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst (fst x012345678)))))) = true
/\ is_bounded (fe2519_32WToZ (snd (fst (fst (fst x012345678))))) = true
/\ is_bounded (fe2519_32WToZ (snd (fst (fst x012345678)))) = true
/\ is_bounded (fe2519_32WToZ (snd (fst x012345678))) = true
/\ is_bounded (fe2519_32WToZ (snd x012345678)) = true),
let (Hx0, Hx12345678) := (eta_and Hx012345678) in
let (Hx1, Hx2345678) := (eta_and Hx12345678) in
let (Hx2, Hx345678) := (eta_and Hx2345678) in
let (Hx3, Hx45678) := (eta_and Hx345678) in
let (Hx4, Hx5678) := (eta_and Hx45678) in
let (Hx5, Hx678) := (eta_and Hx5678) in
let (Hx6, Hx78) := (eta_and Hx678) in
let (Hx7, Hx8) := (eta_and Hx78) in
let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in
let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
match LiftOption.of'
(Interp (@ZBounds.interp_op) ropW (LiftOption.to' (Some x')))
with
| Some bounds => op9_4_bounds_good bounds = true
| None => False
end)
: op9_4_correct_and_bounded ropW op.
Proof.
intros xs Hxs.
pose xs as xs'.
compute in xs.
destruct_head' prod.
cbv [Tuple.map Tuple.on_tuple Tuple.to_list Tuple.to_list' fst snd List.map Tuple.from_list Tuple.from_list' HList.hlistP HList.hlistP'] in Hxs.
pose Hxs as Hxs'.
destruct Hxs as [ [ [ [ [ [ [ [ Hx0 Hx1 ] Hx2 ] Hx3 ] Hx4 ] Hx5 ] Hx6 ] Hx7 ] Hx8 ].
specialize (H0 xs'
(conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 Hx8))))))))).
specialize (H1 xs'
(conj Hx0 (conj Hx1 (conj Hx2 (conj Hx3 (conj Hx4 (conj Hx5 (conj Hx6 (conj Hx7 Hx8))))))))).
Time let args := constr:(op9_args_to_bounded xs' Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8) in
admit; t_correct_and_bounded ropZ_sig Hbounds H0 H1 args. (* On 8.6beta1, with ~2 GB RAM, Finished transaction in 46.56 secs (46.372u,0.14s) (successful) *)
Admitted. (*Time Qed. (* On 8.6beta1, with ~4.3 GB RAM, Finished transaction in 67.652 secs (66.932u,0.64s) (successful) *)*)
|
