blob: 7fd723cb81969f91fea8f85412e16bac55bb7c40 (
plain)
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
|
Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef.
Require Import Coq.QArith.QArith_base.
Require Import Coq.Lists.List. Import ListNotations.
Require Import Crypto.Arithmetic.CoreUnfolder.
Require Import Crypto.Arithmetic.Saturated.CoreUnfolder.
Require Import Crypto.Arithmetic.Saturated.FreezeUnfolder.
Require Import Crypto.Arithmetic.Core. Import B.
Require Import Crypto.Arithmetic.Saturated.Freeze.
Require Crypto.Specific.Framework.CurveParameters.
Require Import Crypto.Specific.Framework.ArithmeticSynthesis.Base.
Require Import Crypto.Specific.Framework.ArithmeticSynthesis.HelperTactics.
Require Import Crypto.Util.Decidable.
Require Import Crypto.Util.LetIn Crypto.Util.ZUtil.Definitions.
Require Crypto.Util.Tuple.
Require Import Crypto.Util.Tactics.CacheTerm.
Module Export Exports.
Hint Opaque freeze : uncps.
Hint Rewrite freeze_id : uncps.
End Exports.
Local Open Scope Z_scope.
Local Infix "^" := Tuple.tuple : type_scope.
Section gen.
Context (m : positive)
(base : Q)
(sz : nat)
(c : list limb)
(bitwidth : Z)
(m_enc : Z^sz)
(base_pos : (1 <= base)%Q)
(sz_nonzero : sz <> 0%nat).
Local Notation wt := (wt_gen base).
Local Notation sz2 := (sz2' sz).
Local Notation wt_divides' := (wt_gen_divides' base base_pos).
Local Notation wt_nonzero := (wt_gen_nonzero base base_pos).
Context (c_small : 0 < Associational.eval c < wt sz)
(m_enc_bounded : Tuple.map (BinInt.Z.land (Z.ones bitwidth)) m_enc = m_enc)
(m_enc_correct : Positional.eval wt m_enc = Z.pos m)
(m_correct_wt : Z.pos m = wt sz - Associational.eval c).
Definition freeze_sig'
: { freeze : (Z^sz -> Z^sz)%type |
forall a : Z^sz,
(0 <= Positional.eval wt a < 2 * Z.pos m)->
let eval := Positional.Fdecode (m := m) wt in
eval (freeze a) = eval a }.
Proof.
eexists; cbv beta zeta; (intros a ?).
pose proof wt_nonzero; pose proof (wt_gen_pos base base_pos).
pose proof (wt_gen0_1 base).
pose proof div_mod; pose proof (wt_gen_divides base base_pos).
pose proof (wt_gen_multiples base base_pos).
pose proof div_correct; pose proof modulo_correct.
let x := constr:(freeze (n:=sz) wt (Z.ones bitwidth) m_enc a) in
presolve_op_F constr:(wt) x;
[ autorewrite with pattern_runtime; reflexivity | ].
rewrite eval_freeze with (c := c);
try eassumption; try omega; try reflexivity.
Defined.
End gen.
Ltac pose_m_correct_wt m c sz wt m_correct_wt :=
cache_proof_with_type_by
(Z.pos m = wt sz - Associational.eval c)
ltac:(vm_decide_no_check)
m_correct_wt.
Ltac pose_freeze_sig wt m base sz c bitwidth m_enc base_pos sz_nonzero freeze_sig :=
cache_sig_with_type_by_existing_sig_helper
ltac:(fun _ => cbv [freeze_sig'])
{freeze : (Z^sz -> Z^sz)%type |
forall a : Z^sz,
(0 <= Positional.eval wt a < 2 * Z.pos m)->
let eval := Positional.Fdecode (m := m) wt in
eval (freeze a) = eval a}
(freeze_sig' m base sz c bitwidth m_enc base_pos sz_nonzero)
freeze_sig.
|
