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

Sel25519

parent ef2c1bd0
...@@ -10,7 +10,7 @@ SHOW := $(if $(VERBOSE),@true "",@echo "") ...@@ -10,7 +10,7 @@ SHOW := $(if $(VERBOSE),@true "",@echo "")
HIDE := $(if $(VERBOSE),,@) HIDE := $(if $(VERBOSE),,@)
DIRS= Libs ListsOp Op Car Montgomery DIRS= Libs ListsOp Op Car Sel Montgomery
INCLUDE= $(foreach a,$(DIRS),$(if $(wildcard $(a)), -Q $(a) $(a))) INCLUDE= $(foreach a,$(DIRS),$(if $(wildcard $(a)), -Q $(a) $(a)))
......
...@@ -5,8 +5,10 @@ Open Scope Z. ...@@ -5,8 +5,10 @@ Open Scope Z.
Definition set_xor (i:Z) := Z.lnot (i - 1). Definition set_xor (i:Z) := Z.lnot (i - 1).
(*
Eval compute in (set_xor 0). Eval compute in (set_xor 0).
Eval compute in (set_xor 1). Eval compute in (set_xor 1).
*)
Lemma set_xor_0 : set_xor 0 = 0. Lemma set_xor_0 : set_xor 0 = 0.
Proof. reflexivity. Qed. Proof. reflexivity. Qed.
...@@ -20,3 +22,4 @@ Proof. intro. go. Qed. ...@@ -20,3 +22,4 @@ Proof. intro. go. Qed.
Lemma land_minus_1 : forall i, Z.land (-1) i = i. Lemma land_minus_1 : forall i, Z.land (-1) i = i.
Proof. intro. apply Z.land_m1_l. Qed. Proof. intro. apply Z.land_m1_l. Qed.
Close Scope Z.
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