diff options
Diffstat (limited to 'src/Spec/PointEncoding.v')
| -rw-r--r-- | src/Spec/PointEncoding.v | 34 |
1 files changed, 20 insertions, 14 deletions
diff --git a/src/Spec/PointEncoding.v b/src/Spec/PointEncoding.v index 1d79a018d..3668632f4 100644 --- a/src/Spec/PointEncoding.v +++ b/src/Spec/PointEncoding.v @@ -6,22 +6,21 @@ Require Crypto.ModularArithmetic.PrimeFieldTheorems. Require Bedrock.Word. Require Crypto.Tactics.VerdiTactics. Require Crypto.Encoding.PointEncodingPre. -Obligation Tactic := eauto using PointEncodingPre.point_encoding_canonical. +Obligation Tactic := eauto; exact PointEncodingPre.point_encoding_canonical. -Require Import Crypto.Spec.Encoding Crypto.Spec.ModularArithmetic. -Require Import Crypto.Spec.CompleteEdwardsCurve. +Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding. +Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.Spec.ModularArithmetic. Local Open Scope F_scope. Section PointEncoding. - Context {prm: CompleteEdwardsCurve.TwistedEdwardsParams} {sz : nat} - {FqEncoding : encoding of ModularArithmetic.F (CompleteEdwardsCurve.q) as Word.word sz}. - - Definition sign_bit (x : F CompleteEdwardsCurve.q) := - match (enc x) with - | Word.WO => false - | Word.WS b _ w' => b - end. + Context {prm: TwistedEdwardsParams} {sz : nat} {sz_nonzero : (0 < sz)%nat} + {bound_check : (BinInt.Z.to_nat q < NPeano.Nat.pow 2 sz)%nat} {q_5mod8 : (q mod 8 = 5)%Z} + {sqrt_minus1_valid : (@ZToField q 2 ^ BinInt.Z.to_N (q / 4)) ^ 2 = opp 1} + {FqEncoding : encoding of (F q) as (Word.word sz)} + {sign_bit : F q -> bool} {sign_bit_zero : sign_bit 0 = false} + {sign_bit_opp : forall x, x <> 0 -> negb (sign_bit x) = sign_bit (opp x)}. + Existing Instance prime_q. Definition point_enc (p : E.point) : Word.word (S sz) := let '(x,y) := proj1_sig p in Word.WS (sign_bit x) (enc y). @@ -29,13 +28,20 @@ Section PointEncoding. Program Definition point_dec_with_spec : {point_dec : Word.word (S sz) -> option E.point | forall w x, point_dec w = Some x -> (point_enc x = w) - } := PointEncodingPre.point_dec. - + } := @PointEncodingPre.point_dec _ _ _ sign_bit. + Definition point_dec := Eval hnf in (proj1_sig point_dec_with_spec). + Definition point_encoding_valid : forall p : E.point, point_dec (point_enc p) = Some p := + @PointEncodingPre.point_encoding_valid _ _ sz_nonzero bound_check q_5mod8 sqrt_minus1_valid _ _ sign_bit_zero sign_bit_opp. + + Definition point_encoding_canonical : forall x_enc x, point_dec x_enc = Some x -> point_enc x = x_enc := + PointEncodingPre.point_encoding_canonical . + Instance point_encoding : encoding of E.point as (Word.word (S sz)) := { enc := point_enc; dec := point_dec; - encoding_valid := PointEncodingPre.point_encoding_valid + encoding_valid := point_encoding_valid; + encoding_canonical := point_encoding_canonical }. End PointEncoding.
\ No newline at end of file |