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
|
(*** Proving ℤ-Like via Architecture *)
Require Import Coq.ZArith.ZArith.
Require Import Crypto.BoundedArithmetic.Interface.
Require Import Crypto.BoundedArithmetic.InterfaceProofs.
Require Import Crypto.BoundedArithmetic.DoubleBounded.
Require Import Crypto.BoundedArithmetic.DoubleBoundedProofs.
Require Import Crypto.BoundedArithmetic.ArchitectureToZLike.
Require Import Crypto.ModularArithmetic.ZBounded.
Require Import Crypto.Util.Tuple.
Require Import Crypto.Util.ZUtil Crypto.Util.Tactics.
Local Open Scope nat_scope.
Local Open Scope Z_scope.
Local Open Scope type_scope.
Local Coercion Z.of_nat : nat >-> Z.
Section fancy_machine_p256_montgomery_foundation.
Context {n_over_two : Z}.
Local Notation n := (2 * n_over_two)%Z.
Context (ops : fancy_machine.instructions n) (modulus : Z).
Local Arguments Z.mul !_ !_.
Local Arguments BaseSystem.decode !_ !_ / .
Local Arguments BaseSystem.accumulate / .
Local Arguments BaseSystem.decode' !_ !_ / .
Local Ltac introduce_t_step :=
match goal with
| [ |- forall x : bool, _ ] => intros [|]
| [ |- True -> _ ] => intros _
| [ |- _ <= _ < _ -> _ ] => intro
| _ => let x := fresh "x" in
intro x;
try pose proof (decode_range (fst x));
try pose proof (decode_range (snd x));
pose proof (decode_range x)
end.
Local Ltac unfolder_t :=
progress unfold LargeT, SmallT, modulus_digits, decode_large, decode_small, Mod_SmallBound, DivBy_SmallBound, DivBy_SmallerBound, Mul, CarryAdd, CarrySubSmall, ConditionalSubtract, ConditionalSubtractModulus, ZLikeOps_of_ArchitectureBoundedOps in *.
Local Ltac saturate_context_step :=
match goal with
| _ => unique assert (0 <= 2 * n_over_two) by solve [ eauto using decode_exponent_nonnegative with typeclass_instances | omega ]
| _ => unique assert (0 <= n_over_two) by solve [ eauto using decode_exponent_nonnegative with typeclass_instances | omega ]
| _ => unique assert (0 <= 2 * (2 * n_over_two)) by (eauto using decode_exponent_nonnegative with typeclass_instances)
| [ H : 0 <= ?x < _ |- _ ] => unique pose proof (proj1 H); unique pose proof (proj2 H)
end.
Local Ltac pre_t :=
repeat first [ tauto
| introduce_t_step
| unfolder_t
| saturate_context_step ].
Local Ltac post_t_step :=
match goal with
| _ => reflexivity
| _ => progress autorewrite with zsimplify_const
| [ |- fst ?x = (?a <=? ?b) :> bool ]
=> cut (((if fst x then 1 else 0) = (if a <=? b then 1 else 0))%Z);
[ destruct (fst x), (a <=? b); intro; congruence | ]
| [ H : (_ =? _) = true |- _ ] => apply Z.eqb_eq in H; subst
| [ H : (_ =? _) = false |- _ ] => apply Z.eqb_neq in H
| _ => autorewrite with push_Zpow in *; solve [ reflexivity | assumption ]
| _ => autorewrite with pull_Zpow in *; pull_decode; reflexivity
| _ => progress push_decode
| _ => rewrite (Z.add_comm (_ << _) _); progress pull_decode
| [ |- context[if ?x =? ?y then _ else _] ] => destruct (x =? y) eqn:?
| _ => autorewrite with Zshift_to_pow; Z.rewrite_mod_small; reflexivity
end.
Local Ltac post_t := repeat post_t_step.
Local Ltac t := pre_t; post_t.
Global Instance ZLikeProperties_of_ArchitectureBoundedOps
{arith : fancy_machine.arithmetic ops}
(modulus_in_range : 0 <= modulus < 2^n)
(smaller_bound_exp : Z)
(smaller_bound_smaller : 0 <= smaller_bound_exp <= n)
(n_pos : 0 < n)
: ZLikeProperties (ZLikeOps_of_ArchitectureBoundedOps ops modulus smaller_bound_exp)
:= { large_valid v := True;
medium_valid v := 0 <= decode_large v < 2^n * 2^smaller_bound_exp;
small_valid v := True }.
Proof.
(* In 8.5: *)
(* par:t. *)
{ abstract t. }
{ abstract t. }
{ abstract t. }
{ abstract t. }
{ abstract t. }
{ abstract t. }
{ abstract t. }
{ abstract t. }
{ abstract t. }
{ abstract t. }
{ abstract t. }
{ abstract t. }
{ abstract t. }
{ abstract t. }
{ abstract t. }
{ abstract t. }
{ abstract t. }
{ abstract t. }
{ abstract t. }
{ abstract t. }
{ abstract t. }
{ abstract t. }
{ abstract t. }
{ abstract t. }
Defined.
End fancy_machine_p256_montgomery_foundation.
|
