fix extraction directives -- tested enc((l+1)B)=enc(B)

3 files changed, 34 insertions, 10 deletions

diff --git a/Makefile b/Makefile
index e1f99befe..c3e34c2f1 100644
--- a/Makefile
+++ b/Makefile
@@ -95,10 +95,10 @@ src/Experiments/Ed25519.hs: src/Experiments/Ed25519_noimports.hs src/Experiments
 		> Ed25519.hs )
 
 src/Experiments/Ed25519.o src/Experiments/Ed25519.core: src/Experiments/Ed25519.hs
-	( cd src/Experiments && ghc -O3 Ed25519.hs -ddump-simpl > Ed25519.core )
+	( cd src/Experiments && ghc -XStrict -O3 Ed25519.hs -ddump-simpl > Ed25519.core )
 
 extraction: src/Experiments/Ed25519.hs
-ghc: src/Experiments/Ed25519.core
+ghc: src/Experiments/Ed25519.core src/Experiments/Ed25519.o
 
 clean::
 	rm -f Makefile.coq
diff --git a/src/Experiments/Ed25519Extraction.v b/src/Experiments/Ed25519Extraction.v
index 17c90b2a2..47cf4f791 100644
--- a/src/Experiments/Ed25519Extraction.v
+++ b/src/Experiments/Ed25519Extraction.v
@@ -150,6 +150,7 @@ Extract Inlined Constant N.even => "Prelude.even".
 Extract Constant N.shiftr => "(\w n -> Data.Bits.shiftR w (Prelude.fromIntegral n))".
 Extract Constant N.shiftl => "(\w n -> Data.Bits.shiftL w (Prelude.fromIntegral n))".
 Extract Constant N.testbit => "(\w n -> Data.Bits.testBit w (Prelude.fromIntegral n))".
+Extract Constant N.testbit_nat => "(\w n -> Data.Bits.testBit w (Prelude.fromIntegral n))".
 
 Extract Constant N.pred => "(\n -> Prelude.max 0 (Prelude.pred n))".
 Extract Constant N.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))".
@@ -157,7 +158,7 @@ Extract Constant N.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n
 Extract Constant N.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
 
 Extract Inductive N => "Prelude.Integer" [ "0" "(\x -> x)" ]
-  "(\fO fS n -> {- match_on_N -} if n Prelude.== 0 then fO () else fS (n Prelude.- 1))".
+  "(\fO fS n -> {- match_on_N -} if n Prelude.== 0 then fO () else fS n)".
 
 (** Z *)
 Require Import ZArith.BinInt.
@@ -246,16 +247,16 @@ Extract Inlined Constant GF25519BoundedCommon.word64 => "Data.Word.Word64".
 Extract Inlined Constant GF25519BoundedCommon.w64eqb => "(Prelude.==)".
 Extract Inlined Constant Word64.word64ToZ => "Prelude.fromIntegral".
 Extract Inlined Constant GF25519BoundedCommon.word64ToZ => "Prelude.fromIntegral".
-Extract Inlined Constant GF25519BoundedCommon.NToWord64 => "".
-Extract Inlined Constant GF25519BoundedCommon.ZToWord64 => "".
+Extract Inlined Constant GF25519BoundedCommon.NToWord64 => "Prelude.fromIntegral".
+Extract Inlined Constant GF25519BoundedCommon.ZToWord64 => "Prelude.fromIntegral".
 Extract Inlined Constant Word64.add => "(Prelude.+)".
 Extract Inlined Constant Word64.mul => "(Prelude.*)".
 Extract Inlined Constant Word64.sub => "(Prelude.-)".
 Extract Inlined Constant Word64.land => "(Data.Bits..&.)".
 Extract Inlined Constant Word64.lor => "(Data.Bits..|.)".
 Extract Constant Word64.neg => "(\_ w -> Prelude.negate w)". (* FIXME: reification: drop arg1 *)
-Extract Constant Word64.shl => "(\w n -> Data.Bits.shiftR w (Prelude.fromIntegral n))".
-Extract Constant Word64.shr => "(\w n -> Data.Bits.shiftL w (Prelude.fromIntegral n))".
+Extract Constant Word64.shr => "(\w n -> Data.Bits.shiftR w (Prelude.fromIntegral n))".
+Extract Constant Word64.shl => "(\w n -> Data.Bits.shiftL w (Prelude.fromIntegral n))".
 Extract Constant Word64.cmovle => "(\x y r1 r2 -> if x Prelude.<= y then r1 else r2)".
 Extract Constant Word64.cmovne => "(\x y r1 r2 -> if x Prelude.== y then r1 else r2)".
 
@@ -282,7 +283,13 @@ Extract Constant Ed25519.H =>
        bytesToLEBits (x:xs) = (x `Data.Bits.testBit` 0) : (x `Data.Bits.testBit` 1) : (x `Data.Bits.testBit` 2) : (x `Data.Bits.testBit` 3) : (x `Data.Bits.testBit` 4) : (x `Data.Bits.testBit` 5) : (x `Data.Bits.testBit` 6) : (x `Data.Bits.testBit` 7) : bytesToLEBits xs } in
  (bytesToLEBits Prelude.. B.unpack Prelude.. SHA.bytestringDigest Prelude.. SHA.sha512 Prelude.. B.pack Prelude.. leBitsToBytes)".
 
-(* invW makes GHC compile very slow *)
-Extract Constant GF25519Bounded.invW => "Prelude.error ('i':'n':'v':'W':[])".
+(* invW makes ghc -XStrict very slow *)
+(* Extract Constant GF25519Bounded.invW => "Prelude.error ('i':'n':'v':'W':[])". *)
 
-Extraction "src/Experiments/Ed25519_noimports.hs" Ed25519.sign (* Ed25519.verify *).
\ No newline at end of file
+Extraction "src/Experiments/Ed25519_noimports.hs" Ed25519.sign (* Ed25519.verify *).
+(*
+*Ed25519 Prelude> and (eRepEnc ((sRepERepMul l eRepB))) == False
+True
+*Ed25519 Prelude> eRepEnc ((sRepERepMul l eRepB) `erepAdd` eRepB) == eRepEnc eRepB
+True
+*)
\ No newline at end of file
diff --git a/src/Experiments/ExtrHaskellNats.v b/src/Experiments/ExtrHaskellNats.v
index ef9fd06d9..3e2974ea1 100644
--- a/src/Experiments/ExtrHaskellNats.v
+++ b/src/Experiments/ExtrHaskellNats.v
@@ -51,12 +51,18 @@ Module Export Import_NPeano_Nat.
   Extract Inlined Constant ltb => "(Prelude.<)".
   Extract Inlined Constant leb => "(Prelude.<=)".
   Extract Inlined Constant eqb => "(Prelude.==)".
+  Extract Inlined Constant eq_dec => "(Prelude.==)".
   Extract Inlined Constant odd => "Prelude.odd".
   Extract Inlined Constant even => "Prelude.even".
   Extract Constant pred => "(\n -> Prelude.max 0 (Prelude.pred n))".
   Extract Constant sub => "(\n m -> Prelude.max 0 (n Prelude.- m))".
   Extract Constant div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
   Extract Constant modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
+
+  (* XXX: unsound due to potential overflow in the second argument *)
+  Extract Constant shiftr => "(\w n -> Data.Bits.shiftR w (Prelude.fromIntegral n))".
+  Extract Constant shiftl => "(\w n -> Data.Bits.shiftL w (Prelude.fromIntegral n))".
+  Extract Constant testbit => "(\w n -> Data.Bits.testBit w (Prelude.fromIntegral n))".
 End Import_NPeano_Nat.
 
 
@@ -72,17 +78,28 @@ Module Export Import_Init_Nat.
 
   Extract Constant div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
   Extract Constant modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
+
+  (* XXX: unsound due to potential overflow in the second argument *)
+  Extract Constant shiftr => "(\w n -> Data.Bits.shiftR w (Prelude.fromIntegral n))".
+  Extract Constant shiftl => "(\w n -> Data.Bits.shiftL w (Prelude.fromIntegral n))".
+  Extract Constant testbit => "(\w n -> Data.Bits.testBit w (Prelude.fromIntegral n))".
 End Import_Init_Nat.
 
 
 Module Export Import_PeanoNat_Nat.
   Import Coq.Arith.PeanoNat.Nat.
 
+  Extract Inlined Constant eq_dec => "(Prelude.==)".
   Extract Inlined Constant add => "(Prelude.+)".
   Extract Inlined Constant mul => "(Prelude.*)".
   Extract Inlined Constant max => "Prelude.max".
   Extract Inlined Constant min => "Prelude.min".
   Extract Inlined Constant compare => "Prelude.compare".
+
+  (* XXX: unsound due to potential overflow in the second argument *)
+  Extract Constant shiftr => "(\w n -> Data.Bits.shiftR w (Prelude.fromIntegral n))".
+  Extract Constant shiftl => "(\w n -> Data.Bits.shiftL w (Prelude.fromIntegral n))".
+  Extract Constant testbit => "(\w n -> Data.Bits.testBit w (Prelude.fromIntegral n))".
 End Import_PeanoNat_Nat.
 
 Extract Inlined Constant Compare_dec.nat_compare_alt => "Prelude.compare".