Commit ca175107 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

moving to coq.8.7.2

parent 1c1a0fb6
Require Import Tweetnacl.Libs.Export.
Definition get_a (t:(list Z * list Z * list Z * list Z * list Z * list Z)) : list Z := match t with
Section get.
Context {T:Type}.
Definition get_a (t:(T * T * T * T * T * T)) : T := match t with
(a,b,c,d,e,f) => a
end.
Definition get_b (t:(T * T * T * T * T * T)) : T := match t with
(a,b,c,d,e,f) => b
end.
Definition get_c (t:(T * T * T * T * T * T)) : T := match t with
(a,b,c,d,e,f) => c
end.
Definition get_d (t:(T * T * T * T * T * T)) : T := match t with
(a,b,c,d,e,f) => d
end.
Definition get_e (t:(T * T * T * T * T * T)) : T := match t with
(a,b,c,d,e,f) => e
end.
Definition get_f (t:(T * T * T * T * T * T)) : T := match t with
(a,b,c,d,e,f) => f
end.
End get.
(*
Definition get_b (t:(list Z * list Z * list Z * list Z * list Z * list Z)) : list Z := match t with
(a,b,c,d,e,f) => b
end.
......@@ -18,7 +40,7 @@ end.
Definition get_f (t:(list Z * list Z * list Z * list Z * list Z * list Z)) : list Z := match t with
(a,b,c,d,e,f) => f
end.
*)
Definition get_m (c:(list Z * list Z)) : list Z := match c with
(m,t) => m
end.
......@@ -27,23 +49,23 @@ Definition get_t (c:(list Z * list Z)) : list Z := match c with
end.
Lemma get_a_length : forall a b c d e f, length (get_a (a,b,c,d,e,f)) = length a. Proof. go. Qed.
Lemma get_b_length : forall a b c d e f, length (get_b (a,b,c,d,e,f)) = length b. Proof. go. Qed.
Lemma get_c_length : forall a b c d e f, length (get_c (a,b,c,d,e,f)) = length c. Proof. go. Qed.
Lemma get_d_length : forall a b c d e f, length (get_d (a,b,c,d,e,f)) = length d. Proof. go. Qed.
Lemma get_e_length : forall a b c d e f, length (get_e (a,b,c,d,e,f)) = length e. Proof. go. Qed.
Lemma get_f_length : forall a b c d e f, length (get_f (a,b,c,d,e,f)) = length f. Proof. go. Qed.
Lemma get_a_length : forall (a b c d e f:list Z), length (get_a (a,b,c,d,e,f)) = length a. Proof. go. Qed.
Lemma get_b_length : forall (a b c d e f:list Z), length (get_b (a,b,c,d,e,f)) = length b. Proof. go. Qed.
Lemma get_c_length : forall (a b c d e f:list Z), length (get_c (a,b,c,d,e,f)) = length c. Proof. go. Qed.
Lemma get_d_length : forall (a b c d e f:list Z), length (get_d (a,b,c,d,e,f)) = length d. Proof. go. Qed.
Lemma get_e_length : forall (a b c d e f:list Z), length (get_e (a,b,c,d,e,f)) = length e. Proof. go. Qed.
Lemma get_f_length : forall (a b c d e f:list Z), length (get_f (a,b,c,d,e,f)) = length f. Proof. go. Qed.
Lemma get_m_length : forall m t, length (get_m (m,t)) = length m. Proof. go. Qed.
Lemma get_t_length : forall m t, length (get_t (m,t)) = length t. Proof. go. Qed.
Open Scope Z.
Lemma get_a_Zlength : forall a b c d e f, Zlength (get_a (a,b,c,d,e,f)) = Zlength a. Proof. go. Qed.
Lemma get_b_Zlength : forall a b c d e f, Zlength (get_b (a,b,c,d,e,f)) = Zlength b. Proof. go. Qed.
Lemma get_c_Zlength : forall a b c d e f, Zlength (get_c (a,b,c,d,e,f)) = Zlength c. Proof. go. Qed.
Lemma get_d_Zlength : forall a b c d e f, Zlength (get_d (a,b,c,d,e,f)) = Zlength d. Proof. go. Qed.
Lemma get_e_Zlength : forall a b c d e f, Zlength (get_e (a,b,c,d,e,f)) = Zlength e. Proof. go. Qed.
Lemma get_f_Zlength : forall a b c d e f, Zlength (get_f (a,b,c,d,e,f)) = Zlength f. Proof. go. Qed.
Lemma get_a_Zlength : forall (a b c d e f:list Z), Zlength (get_a (a,b,c,d,e,f)) = Zlength a. Proof. go. Qed.
Lemma get_b_Zlength : forall (a b c d e f:list Z), Zlength (get_b (a,b,c,d,e,f)) = Zlength b. Proof. go. Qed.
Lemma get_c_Zlength : forall (a b c d e f:list Z), Zlength (get_c (a,b,c,d,e,f)) = Zlength c. Proof. go. Qed.
Lemma get_d_Zlength : forall (a b c d e f:list Z), Zlength (get_d (a,b,c,d,e,f)) = Zlength d. Proof. go. Qed.
Lemma get_e_Zlength : forall (a b c d e f:list Z), Zlength (get_e (a,b,c,d,e,f)) = Zlength e. Proof. go. Qed.
Lemma get_f_Zlength : forall (a b c d e f:list Z), Zlength (get_f (a,b,c,d,e,f)) = Zlength f. Proof. go. Qed.
Lemma get_m_Zlength : forall m t, Zlength (get_m (m,t)) = Zlength m. Proof. go. Qed.
Lemma get_t_Zlength : forall m t, Zlength (get_t (m,t)) = Zlength t. Proof. go. Qed.
......
......@@ -28,7 +28,7 @@ COQTOP=$(COQBIN)coqtop
COQDEP=$(COQBIN)coqdep $(DEPFLAGS)
COQDOC=$(COQBIN)coqdoc -d doc -g -utf8 $(DEPFLAGS)
COQVERSION= 8.7.0 or-else 8.7.1
COQVERSION= 8.7.0 or-else 8.7.1 or-else 8.7.2
COQV=$(shell $(COQC) -v)
ifeq ("$(filter $(COQVERSION),$(COQV))","")
$(error FAILURE: You need Coq $(COQVERSION) but you have this version: $(COQV))
......
From Tweetnacl.Low Require Import Pack25519.
From Tweetnacl.Low Require Import Unpack25519.
From Tweetnacl.Low Require Import M.
From Tweetnacl.Low Require Import Inv25519.
From Tweetnacl.Low Require Import ScalarMult_rev.
From Tweetnacl.Low Require Import Get_abcdef.
From Tweetnacl.Low Require Import Constant.
From Tweetnacl.Low Require Import Prep_n.
Definition Crypto_Scalarmult n p :=
let a := get_a (montgomery_fn 255 254 (clamp n) One16 (Unpack25519 p) nul16 One16 nul16 nul16 (Unpack25519 p)) in
let c := get_c (montgomery_fn 255 254 (clamp n) One16 (Unpack25519 p) nul16 One16 nul16 nul16 (Unpack25519 p)) in
Pack25519 (M a (Inv25519 c)).
\ No newline at end of file
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment