Carlo/compliance circuit (#4)

* compliance circuit layout * compliance circuit: clarify the constant elements * add pedersen_hash_to_curve * juvix compliance circuit * compliance circuit, with thest, compiled json file and input hson file * minor changes * fixed NotCurvePoint bug * added json file, with fix to no point of curve bug (2nd) * updated juvix * fixed mix test error * input npk change --------- Co-authored-by: Xuyang Song <[email protected]>
anoma · Jun 27, 2024 · 4a1be7a · 4a1be7a
1 parent 32e9adb
commit 4a1be7a
Show file tree

Hide file tree

Showing 5 changed files with 163 additions and 2 deletions.
diff --git a/lib/cairo.ex b/lib/cairo.ex
@@ -16,8 +16,7 @@ defmodule Cairo do
     :world
   end
 
-  @spec cairo_vm_runner(list(byte()), list(byte())) ::
-          {list(byte()), list(byte())}
+  @spec cairo_vm_runner(binary(), binary()) :: {[byte()], [byte()]}
   defdelegate cairo_vm_runner(program_content, program_input),
     to: Cairo.CairoVM,
     as: :cairo_vm_runner

diff --git a/native/cairo_vm/compliance.json b/native/cairo_vm/compliance.json
diff --git a/native/cairo_vm/compliance.juvix b/native/cairo_vm/compliance.juvix
@@ -0,0 +1,115 @@
+module compliance;
+
+import Stdlib.Prelude open;
+import Stdlib.Cairo.Ec as Ec;
+import Stdlib.Cairo.Poseidon open;
+import Stdlib.Cairo.Pedersen open;
+
+-- type Quantity := Field;
+-- quantityCheck := ...;
+
+type Resource :=
+  mkResource {
+    logic : Field;
+    label : Field;
+    quantity : Field;
+    data : Field;
+    eph : Bool;
+    nonce : Field;
+    npk : Field;
+    rseed : Field
+  };
+
+type ComplianceResult :=
+  mkResult {
+    -- The nullifier of input resource
+    input_nullifier : Field;
+    -- The commitment to the output resource
+    output_cm : Field;
+    -- The root of the resource commitment Merkle tree
+    root : Field;
+    -- Resource delta is used to reason about total quantities of different kinds of resources
+    delta_x : Field;
+    delta_y : Field;
+    -- TODO: add resource logic commitments (for functional privacy)
+    -- input_logic_commitment: 
+    -- output_logic_commitment: 
+  };
+
+bool (x : Field) : Bool :=
+  x * (x - 1) == 0;
+
+check_merkle (current_root : Field) : Field × Bool -> Field
+  | (node, is_left) := 
+  let pair :=
+  if 
+    | is_left := (node, current_root)
+    | else := (current_root, node)
+
+  in
+  case pair of (lhs , rhs) := poseidonHash2 lhs rhs;
+
+
+--- Check the merkle tree path validity and return the root
+check_merkle_path (cur : Field) : (List (Field × Bool)) -> Field
+  | [] := cur
+  | (p :: ps) := check_merkle_path (check_merkle cur p) ps;  
+
+
+main (input output : Resource) (merkle_path : List (Field × Bool)) (rcv : Field) (eph_root : Field): ComplianceResult := 
+
+  -- Check the input resource commitment:
+  let 
+  input_npk : Field := poseidonHash2 (Resource.npk input) 0; 
+  PRF_EXPAND_PERSONALIZATION_TO_FIELD : Field := poseidonHash1 12345;
+  input_psi := poseidonHashList [PRF_EXPAND_PERSONALIZATION_TO_FIELD; 0; Resource.rseed input; Resource.nonce input];
+  input_rcm := poseidonHashList [PRF_EXPAND_PERSONALIZATION_TO_FIELD; 1; Resource.rseed input; Resource.nonce input];
+
+  eph_field : Field :=
+  if
+    | (Resource.eph input) := 1
+    | else := 0
+  ;
+  input_cm := poseidonHashList [Resource.logic input; Resource.label input; Resource.data input; input_npk; Resource.nonce input; input_psi; Resource.quantity input; eph_field; input_rcm];
+
+  -- Generate the nullifier of input resource
+  input_nullifier_ := poseidonHashList [(Resource.npk input);  (Resource.nonce input);  input_psi;  input_cm];
+
+
+  -- Check the output resource commitment
+  output_psi := poseidonHashList [PRF_EXPAND_PERSONALIZATION_TO_FIELD; 0; Resource.rseed output; Resource.nonce output];
+  output_rcm := poseidonHashList [PRF_EXPAND_PERSONALIZATION_TO_FIELD; 1; Resource.rseed output; Resource.nonce output];
+  output_cm_ := poseidonHashList [Resource.logic output; Resource.label output; Resource.data output; Resource.npk output; input_cm; output_psi; Resource.quantity output; eph_field; output_rcm];
+
+  root_ :=
+  if
+    | (Resource.eph input) := eph_root
+    | else := check_merkle_path input_cm merkle_path
+  ;
+
+  -- Compute the delta commitment
+  b1 : Field := poseidonHash1 345678;
+  b2 : Field := poseidonHash1 789012;
+  blind_base := pedersenHashToCurve b1 b2;
+  input_kind := pedersenHashToCurve (Resource.logic input) (Resource.label input);
+  output_kind := pedersenHashToCurve (Resource.logic output) (Resource.label output);
+  d1 := Ec.mul (Resource.quantity input) input_kind;
+  d2 := Ec.mul (Resource.quantity output) output_kind;
+  d3 := Ec.mul rcv blind_base;
+  delta := Ec.add (Ec.sub d1  d2) d3;
+  in
+
+mkResult@{
+    -- The nullifier of input resource
+    input_nullifier := input_nullifier_;
+    -- The commitment to the output resource
+    output_cm := output_cm_;
+    -- The root of the resource commitment Merkle tree
+    root := root_;
+    -- Resource delta is used to reason about total quantities of different kinds of resources
+    delta_x := Ec.Point.x delta;
+    delta_y := Ec.Point.y delta;
+    -- TODO: add resource logic commitments
+    -- input_logic_commitment: 
+    -- output_logic_commitment: 
+  };
diff --git a/native/cairo_vm/compliance_input.json b/native/cairo_vm/compliance_input.json
@@ -0,0 +1,25 @@
+{
+    "input": {
+        "logic" : 41,
+        "label" : 12,
+        "quantity" : 13,
+        "data" : 14,
+        "eph" : 15,
+        "nonce" : 26,
+        "npk" : 37,
+        "rseed" : 48
+    },
+    "output": {
+        "logic" : 59,
+        "label" : 6432,
+        "quantity" : 711,
+        "data" : 812,
+        "eph" : 93,
+        "nonce" : 104,
+        "npk" : 195,
+        "rseed" : 16
+    },
+    "merkle_path": [{"fst": 33, "snd": true}, {"fst": 83, "snd": false}, {"fst": 73, "snd": false}, {"fst": 23, "snd": false}, {"fst": 33, "snd": false}, {"fst": 43, "snd": false}, {"fst": 53, "snd": false}, {"fst": 3, "snd": false}, {"fst": 36, "snd": false}, {"fst": 37, "snd": false}, {"fst": 118, "snd": false}, {"fst": 129, "snd": false}, {"fst": 12, "snd": true}, {"fst": 33, "snd": false}, {"fst": 43, "snd": false}, {"fst": 156, "snd": true}, {"fst": 63, "snd": false}, {"fst": 128, "snd": false}, {"fst": 32, "snd": false}, {"fst": 230, "snd": true}, {"fst": 3, "snd": false}, {"fst": 33, "snd": false}, {"fst": 223, "snd": false}, {"fst": 2032, "snd": true}, {"fst": 32, "snd": false}, {"fst": 323, "snd": false}, {"fst": 3223, "snd": false}, {"fst": 203, "snd": true}, {"fst": 31, "snd": false}, {"fst": 32, "snd": false}, {"fst": 22, "snd": false}, {"fst": 23, "snd": true}],
+    "rcv": 3,
+    "eph_root": 4
+}
diff --git a/test/cairo_compliance_test.exs b/test/cairo_compliance_test.exs
@@ -0,0 +1,21 @@
+defmodule CairoComplianceTest do
+  use ExUnit.Case
+
+  doctest Cairo.CairoProver
+  doctest Cairo.CairoVM
+
+  test "compliance_circuit" do
+    {:ok, program} = File.read("./native/cairo_vm/compliance.json")
+    {:ok, input} = File.read("./native/cairo_vm/compliance_input.json")
+
+    {output, trace, memory} =
+      Cairo.cairo_vm_runner(
+        program,
+        input
+      )
+
+    # Prove and verify
+    {proof, public_input} = Cairo.prove(trace, memory)
+    assert true = Cairo.verify(proof, public_input)
+  end
+end