Commit 565df286 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

Working on proof of unpack25519

parent 86d87827
......@@ -230,6 +230,20 @@ Proof.
induction a ; intros [] Hi Hl ; go.
Qed.
Definition list_ind_by_2 :
forall A (P : list A Prop),
P []
(forall a, P [a])
(forall (a b:A) (l : list A), P l P (a :: b :: l))
forall (l : list A), P l :=
fun A => fun P => fun P0 => fun P1 => fun PSS =>
fix f (l : list A) := match l with
[] => P0
| [a] => P1 a
| a :: b :: l => PSS a b l (f l)
end.
(*
Lemma app_nill_r : forall (A:Type) (l:list A), l ++ nil = l.
Proof. boum. Qed.
......
default_target: .loadpath Libs ListsOp Op Car Sel Montgomery
default_target: .loadpath Libs ListsOp Op Car Sel Montgomery Unpack
#Note3: for SSReflect, one solution is to install MathComp 1.6
# somewhere add this line to a CONFIGURE file
......@@ -10,7 +10,7 @@ SHOW := $(if $(VERBOSE),@true "",@echo "")
HIDE := $(if $(VERBOSE),,@)
DIRS= Libs ListsOp Op Car Sel Montgomery
DIRS= Libs ListsOp Op Car Sel Montgomery Unpack
INCLUDE= $(foreach a,$(DIRS),$(if $(wildcard $(a)), -Q $(a) $(a)))
......@@ -76,17 +76,23 @@ LISTSOP_FILES = $(notdir $(wildcard ListsOp/*.v))
OP_FILES = $(notdir $(wildcard Op/*.v))
CAR_FILES = $(notdir $(wildcard Car/*.v))
SEL_FILES = $(notdir $(wildcard Sel/*.v))
UNPACK_FILES = $(notdir $(wildcard Unpack/*.v))
MONTGOMERY_FILES = $(notdir $(wildcard Montgomery/*.v))
FILES = \
$(MONTGOMERY_FILES:%=Montgomery/%) \
COUNTFILES = \
$(LIBS_FILES:%=Libs/%) \
$(LISTSOP_FILES:%=ListsOp/%) \
$(OP_FILES:%=Op/%) \
$(CAR_FILES:%=Car/%) \
$(SEL_FILES:%=Sel/%) \
$(UNPACK_FILES:%=Unpack/%) \
FILES = \
$(COUNTFILES) \
$(MONTGOMERY_FILES:%=Montgomery/%) \
ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
ifneq ($(filter-out archclean clean cleanall printenv count,$(MAKECMDGOALS)),)
-include $(addsuffix .d,$(FILES))
else
ifeq ($(MAKECMDGOALS),)
......@@ -94,11 +100,13 @@ ifeq ($(MAKECMDGOALS),)
endif
endif
CLEANFILES = $(call clean_files,LIBS_FILES,Libs) \
CLEANFILES = \
$(call clean_files,LIBS_FILES,Libs) \
$(call clean_files,LISTSOP_FILES,ListsOp) \
$(call clean_files,OP_FILES,Op) \
$(call clean_files,CAR_FILES,Car) \
$(call clean_files,SEL_FILES,Sel) \
$(call clean_files,UNPACK_FILES,Unpack) \
$(call clean_files,MONTGOMERY_FILES,Montgomery)
%_stripped.v: %.v
......@@ -131,9 +139,10 @@ quick: .loadpath $(FILES:.v=.vio)
Libs: .loadpath $(LIBS_FILES:%.v=Libs/%.vo)
ListsOp: .loadpath $(LISTSOP_FILES:%.v=ListsOp/%.vo)
Op: .loadpath $(OP_FILES:%.v=Op/%.vo)
Op: .loadpath $(OP_FILES:%.v=Op/%.vo)
Car: .loadpath $(CAR_FILES:%.v=Car/%.vo)
Sel: .loadpath $(SEL_FILES:%.v=Sel/%.vo)
Unpack: .loadpath $(UNPACK_FILES:%.v=Unpack/%.vo)
Montgomery: .loadpath $(MONTGOMERY_FILES:%.v=Montgomery/%.vo)
_CoqProject: Makefile
......@@ -167,7 +176,7 @@ checkproofs:
$(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(FILES:%.v=%.vio)
count:
wc $(FILES)
wc -l $(COUNTFILES)
printenv:
@"$(COQTOP)" -config
......
Require Import Tweetnacl.Libs.Export.
Require Import Tweetnacl.ListsOp.Export.
Require Import stdpp.prelude.
Open Scope Z.
Section Integer.
Variable n:Z.
Hypothesis Hn: n > 0.
Notation "ℤ.lst A" := (ZofList n A) (at level 65, right associativity).
Fixpoint unpack_for (l:list Z) : list Z := match l with
| [] => []
| h :: [] => [h]
| a :: b :: q => (a + 2^n * b) :: unpack_for q
end.
Lemma unpack_for_nth : forall (i:nat) (l:list Z), nth i (unpack_for l) 0 = nth (2 * i) l 0 + 2 ^ n * nth (2 * i + 1) l 0.
Proof. induction i; intros.
destruct l ; simpl ; flatten ; simpl ; ring.
destruct l ; simpl ; flatten.
omega.
simpl ; flatten ; omega.
replace (i + S(i + 0))%nat with (S (2 * i))%nat by omega.
replace (S(2 * i) + 1)%nat with (S (2 * i + 1))%nat by omega.
simpl nth.
rewrite IHi.
reflexivity.
Qed.
End Integer.
Lemma Unpack_for_ind_step: forall n, 0 < n ->
forall l, ZofList (2*n) (unpack_for n l) = ZofList n l ->
forall a b, ZofList (2*n) (unpack_for n ( a :: b :: l)) = ZofList n (a :: b :: l).
Proof.
intros n Hn l Hl a b.
simpl.
rewrite Hl.
rewrite <- Z.add_assoc.
f_equal.
rewrite <-Zred_factor4.
f_equal.
replace ( 2* n ) with (n + n) by omega.
rewrite Zpower_exp by omega. ring.
Qed.
Lemma Unpack25519_correct: forall n, 0 < n -> forall l, ZofList (2*n) (unpack_for n l) = ZofList n l.
Proof.
intros n Hn l.
induction l using list_ind_by_2.
reflexivity.
simpl. omega.
apply Unpack_for_ind_step ; assumption.
Qed.
Lemma Unpack25519_length : forall n, 0 < n -> forall l m , length l = m -> even m = true -> length (unpack_for n l) = Nat.div m 2.
Proof.
intros n Hn. induction l using list_ind_by_2 ; intros.
simpl in H.
subst m.
reflexivity.
simpl in H.
subst m.
inversion H0.
simpl unpack_for.
simpl length in *.
subst m.
simpl in H0.
replace (S (S (length l))) with (length l + 1*2)%nat by omega.
rewrite NPeano.Nat.div_add by omega.
replace (length l `div` 2 + 1)%nat with (S (length l `div` 2))%nat by omega.
f_equal.
apply IHl ; auto.
Qed.
Close Scope Z.
Corollary Unpack25519_length_16_32 : forall l, length l = 32 -> length (unpack_for 16 l) = 16.
Proof.
intros.
rewrite (Unpack25519_length 16) with (m:=32).
reflexivity.
omega.
assumption.
reflexivity.
Qed.
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