Pedersen hash to curve (#99)

* Adds a simplified version of Pedersen hash, following
https://research.anoma.net/t/revised-zkvm-strategy/546/27
* Reformats the Juvix sources for the CI to pass

Author: lukaszcz

Stdlib/Cairo/Pedersen.juvix

@@ -0,0 +1,28 @@
+module Stdlib.Cairo.Pedersen;
+
+import Stdlib.Data.Field open using {Field};
+import
+Stdlib.Cairo.Ec as Ec;
+
+module ConstantPoints;
+  P0 : Ec.Point :=
+    Ec.mkPoint
+      2089986280348253421170679821480865132823066470938446095505822317253594081284
+      1713931329540660377023406109199410414810705867260802078187082345529207694986;
+
+  P1 : Ec.Point :=
+    Ec.mkPoint
+      996781205833008774514500082376783249102396023663454813447423147977397232763
+      1668503676786377725805489344771023921079126552019160156920634619255970485781;
+
+  P2 : Ec.Point :=
+    Ec.mkPoint
+      2251563274489750535117886426533222435294046428347329203627021249169616184184
+      1798716007562728905295480679789526322175868328062420237419143593021674992973;
+end;
+
+pedersenHashToCurve (x y : Field) : Ec.Point :=
+  let
+    open ConstantPoints;
+    open Ec.Operators;
+  in P0 + x * P1 + y * P2;

Stdlib/Data/Int/Base.juvix

@@ -29,10 +29,9 @@ nonNeg : Int -> Bool
 --- Subtraction for ;Nat;s.
 builtin int-sub-nat
 intSubNat (n m : Nat) : Int :=
-  case sub n m of {
+  case sub n m of
     | zero := ofNat (Nat.sub m n)
-    | suc k := negSuc k
-  };
+    | suc k := negSuc k;
 
 syntax operator + additive;
 

Stdlib/Data/List.juvix

@@ -32,11 +32,10 @@ ordListI {A} {{Ord A}} : Ord (List A) :=
       | nil _ := LT
       | _ nil := GT
       | (x :: xs) (y :: ys) :=
-        case Ord.cmp x y of {
+        case Ord.cmp x y of
           | LT := LT
           | GT := GT
-          | EQ := go xs ys
-        };
+          | EQ := go xs ys;
   in mkOrd go;
 
 instance

Stdlib/Data/List/Base.juvix

@@ -87,7 +87,7 @@ splitAt {A} : Nat → List A → List A × List A
   | zero xs := nil, xs
   | (suc zero) (x :: xs) := x :: nil, xs
   | (suc m) (x :: xs) :=
-    case splitAt m xs of {l1, l2 := x :: l1, l2};
+    case splitAt m xs of l1, l2 := x :: l1, l2;
 
 --- 𝒪(𝓃 + 𝓂). Merges two lists according the given ordering.
 terminating
@@ -104,9 +104,8 @@ merge {A} {{Ord A}} : List A → List A → List A
 partition {A} (f : A → Bool) : List A → List A × List A
   | nil := nil, nil
   | (x :: xs) :=
-    case partition f xs of {
-      l1, l2 := if (f x) (x :: l1, l2) (l1, x :: l2)
-    };
+    case partition f xs of
+      l1, l2 := if (f x) (x :: l1, l2) (l1, x :: l2);
 
 syntax operator ++ cons;
 
@@ -204,9 +203,8 @@ quickSort {A} {{Ord A}} : List A → List A :=
       | nil := nil
       | xs@(_ :: nil) := xs
       | (x :: xs) :=
-        case partition (isGT ∘ Ord.cmp x) xs of {
-          l1, l2 := go l1 ++ x :: go l2
-        };
+        case partition (isGT ∘ Ord.cmp x) xs of
+          l1, l2 := go l1 ++ x :: go l2;
   in go;
 
 --- 𝒪(𝓃) Filters out every ;nothing; from a ;List;.

Stdlib/Data/Product.juvix

@@ -18,11 +18,10 @@ ordProductI {A B} : {{Ord A}} -> {{Ord B}} -> Ord (A × B)
   | {{mkOrd cmp-a}} {{mkOrd cmp-b}} :=
     mkOrd
       λ {(a1, b1) (a2, b2) :=
-        case cmp-a a1 a2 of {
+        case cmp-a a1 a2 of
           | LT := LT
           | GT := GT
-          | EQ := cmp-b b1 b2
-        }};
+          | EQ := cmp-b b1 b2};
 
 instance
 showProductI

Stdlib/Trait/Ord.juvix

@@ -39,22 +39,20 @@ syntax operator <= comparison;
 --- Returns ;true; iff the first element is less than or equal to the second.
 {-# inline: always #-}
 <= {A} {{Ord A}} (x y : A) : Bool :=
-  case Ord.cmp x y of {
+  case Ord.cmp x y of
     | EQ := true
     | LT := true
-    | GT := false
-  };
+    | GT := false;
 
 syntax operator < comparison;
 
 --- Returns ;true; iff the first element is less than the second.
 {-# inline: always #-}
 < {A} {{Ord A}} (x y : A) : Bool :=
-  case Ord.cmp x y of {
+  case Ord.cmp x y of
     | EQ := false
     | LT := true
-    | GT := false
-  };
+    | GT := false;
 
 syntax operator > comparison;
 

Stdlib/Trait/Ord/Eq.juvix

@@ -10,10 +10,9 @@ fromOrdToEq {A} {{Ord A}} : Eq.Eq A := Eq.mkEq (==);
 syntax operator == comparison;
 
 == {A} {{Ord A}} (x y : A) : Bool :=
-  case Ord.cmp x y of {
+  case Ord.cmp x y of
     | EQ := true
-    | _ := false
-  };
+    | _ := false;
 
 syntax operator /= comparison;
 

test/Test.juvix

@@ -23,31 +23,28 @@ prop-tailLengthOneLess : List Int -> Bool
 
 prop-splitAtRecombine : Nat -> List Int -> Bool
   | n xs :=
-    case splitAt n xs of {
-      lhs, rhs := eqListInt xs (lhs ++ rhs)
-    };
+    case splitAt n xs of
+      lhs, rhs := eqListInt xs (lhs ++ rhs);
 
 prop-splitAtLength : Nat -> List Int -> Bool
   | n xs :=
     case
       splitAt n (xs ++ replicate (sub n (length xs)) (ofNat 0))
-    of {
+    of
       lhs, rhs :=
-        length lhs == n && length rhs == sub (length xs) n
-    };
+        length lhs == n && length rhs == sub (length xs) n;
 -- Make sure the list has length at least n
 
 prop-mergeSumLengths : List Int -> List Int -> Bool
   | xs ys := length xs + length ys == length (merge xs ys);
 
 prop-partition : List Int -> (Int -> Bool) -> Bool
   | xs p :=
-    case partition p xs of {
+    case partition p xs of
       lhs, rhs :=
         all p lhs
           && not (any p rhs)
-          && eqListInt (sortInt xs) (sortInt (lhs ++ rhs))
-    };
+          && eqListInt (sortInt xs) (sortInt (lhs ++ rhs));
 
 prop-distributive : Int -> Int -> (Int -> Int) -> Bool
   | a b f := f (a + b) == f a + f b;
@@ -119,15 +116,13 @@ prop-transposeMatrixDimensions : List (List Int) -> Bool
     let
       txs : List (List Int) := transpose xs;
       checkTxsRowXsCol : Bool :=
-        case xs of {
+        case xs of
           | x :: _ := length txs == length x
-          | _ := null txs
-        };
+          | _ := null txs;
       checkXsRowTxsCol : Bool :=
-        case txs of {
+        case txs of
           | tx :: _ := length xs == length tx
-          | _ := null xs
-        };
+          | _ := null xs;
     in checkTxsRowXsCol && checkXsRowTxsCol;
 
 sortTest : String -> (List Int -> List Int) -> QC.Test