Sel25519

Makefile

-default_target: .loadpath Libs ListsOp Op Car Montgomery
+default_target: .loadpath Libs ListsOp Op Car Sel Montgomery
 
 #Note3: for SSReflect, one solution is to install MathComp 1.6
 # somewhere add this line to a CONFIGURE file
@@ -75,6 +75,7 @@ LIBS_FILES = $(notdir $(wildcard Libs/*.v))
 LISTSOP_FILES = $(notdir $(wildcard ListsOp/*.v))
 OP_FILES = $(notdir $(wildcard Op/*.v))
 CAR_FILES = $(notdir $(wildcard Car/*.v))
+SEL_FILES = $(notdir $(wildcard Sel/*.v))
 MONTGOMERY_FILES = $(notdir $(wildcard Montgomery/*.v))
 
 FILES = \
@@ -83,6 +84,7 @@ FILES = \
  $(LISTSOP_FILES:%=ListsOp/%) \
  $(OP_FILES:%=Op/%) \
  $(CAR_FILES:%=Car/%) \
+ $(SEL_FILES:%=Car/%) \
 
 ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
 -include $(addsuffix .d,$(FILES))
@@ -96,6 +98,7 @@ 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,MONTGOMERY_FILES,Montgomery)
 
 %_stripped.v: %.v
@@ -130,6 +133,7 @@ Libs: 		.loadpath $(LIBS_FILES:%.v=Libs/%.vo)
 ListsOp:	.loadpath $(LISTSOP_FILES:%.v=ListsOp/%.vo)
 Op:		.loadpath $(OP_FILES:%.v=Op/%.vo)
 Car:		.loadpath $(CAR_FILES:%.v=Car/%.vo)
+Sel:		.loadpath $(SEL_FILES:%.v=Sel/%.vo)
 Montgomery:	.loadpath $(MONTGOMERY_FILES:%.v=Montgomery/%.vo)
 
 _CoqProject: Makefile

Sel/Binary_select.v

+Require Import Tweetnacl.Libs.Export.
+Require Import stdpp.prelude.
+
+Open Scope Z.
+
+Definition set_xor (i:Z) := Z.lnot (i - 1).
+
+Eval compute in (set_xor 0).
+Eval compute in (set_xor 1).
+
+Lemma set_xor_0 : set_xor 0 = 0.
+Proof. reflexivity. Qed.
+
+Lemma set_xor_1 : set_xor 1 = -1.
+Proof. reflexivity. Qed.
+
+Lemma land_0 : forall i, Z.land 0 i = 0.
+Proof. intro. go. Qed.
+
+Lemma land_minus_1 : forall i, Z.land (-1) i = i.
+Proof. intro. apply Z.land_m1_l. Qed.
+

Sel/Sel25519.v

+Require Import Tweetnacl.Libs.Export.
+Require Import stdpp.prelude.
+
+Open Scope Z.
+
+(* Some definitions relating to the functional spec of this particular program.  *)
+Definition list_cswap (b:Z) (p q : list Z) : list Z := 
+  if (Z.eqb b 0) then
+    p
+  else q.
+
+Lemma list_cswap_nth_true: forall i d p q,
+  nth i (list_cswap 1 p q) d = nth i q d.
+Proof.
+  intros. go.
+Qed.
+
+Lemma list_cswap_nth_false: forall i d p q,
+  nth i (list_cswap 0 p q) d = nth i p d.
+Proof.
+  intros. go.
+Qed.
+
+Close Scope Z.
\ No newline at end of file