add tests

test/Casm/Compilation/Positive.hs

@@ -565,5 +565,13 @@ tests =
         $(mkRelDir ".")
         $(mkRelFile "test078.juvix")
         Nothing
-        $(mkRelFile "out/test078.out")
+        $(mkRelFile "out/test078.out"),
+      posTest
+        "Test079: Trivial resource logic"
+        False
+        True
+        $(mkRelDir ".")
+        $(mkRelFile "test079.juvix")
+        (Just $(mkRelFile "in/test079.json"))
+        $(mkRelFile "out/test079.out")
     ]

test/Casm/Reg/Cairo.hs

@@ -53,5 +53,11 @@ cairoTests =
       $(mkRelDir ".")
       $(mkRelFile "test042.jvr")
       $(mkRelFile "out/test042.out")
-      Nothing
+      Nothing,
+    P.PosTest
+      "Test048: Mock resource logic"
+      $(mkRelDir ".")
+      $(mkRelFile "test048.jvr")
+      $(mkRelFile "out/test048.out")
+      (Just $(mkRelFile "in/test048.json"))
   ]

test/Casm/Reg/Positive.hs

@@ -228,5 +228,29 @@ tests =
       $(mkRelDir ".")
       $(mkRelFile "test043.jvr")
       $(mkRelFile "out/test043.out")
-      Nothing
+      Nothing,
+    PosTest
+      "Test044: Extend closure in true branch"
+      $(mkRelDir ".")
+      $(mkRelFile "test044.jvr")
+      $(mkRelFile "out/test044.out")
+      (Just $(mkRelFile "in/test044.json")),
+    PosTest
+      "Test045: Extend closure in false branch"
+      $(mkRelDir ".")
+      $(mkRelFile "test045.jvr")
+      $(mkRelFile "out/test045.out")
+      (Just $(mkRelFile "in/test045.json")),
+    PosTest
+      "Test046: Call in true branch"
+      $(mkRelDir ".")
+      $(mkRelFile "test046.jvr")
+      $(mkRelFile "out/test046.out")
+      (Just $(mkRelFile "in/test046.json")),
+    PosTest
+      "Test047: Call in false branch"
+      $(mkRelDir ".")
+      $(mkRelFile "test047.jvr")
+      $(mkRelFile "out/test047.out")
+      (Just $(mkRelFile "in/test047.json"))
   ]

tests/Casm/Compilation/positive/in/test079.json

@@ -0,0 +1,31 @@
+{
+    "self_resource": {
+        "logic": "0x373bb1d37414c2edf111cf2f9f076517da99d38e44cdd716ca2ad00a07731e5",
+        "label": "0x12",
+        "quantity": "0x13",
+        "data": "0x14",
+        "eph": false,
+        "nonce": "0x26",
+        "npk": "0x7752582c54a42fe0fa35c40f07293bb7d8efe90e21d8d2c06a7db52d7d9b7a1",
+        "rseed": "0x48"
+    },
+    "resource_nf_key": "0x1",
+    "merkle_path": [
+        {
+            "fst": "0x33",
+            "snd": true
+        },
+        {
+            "fst": "0x83",
+            "snd": false
+        },
+        {
+            "fst": "0x73",
+            "snd": false
+        },
+        {
+            "fst": "0x23",
+            "snd": false
+        }
+    ]
+}

tests/Casm/Compilation/positive/out/test079.out

@@ -0,0 +1,16 @@
+-395556098205570544514862427675713135822454173064116032036066260837844667166
+1199411604616075448730293334298953634347373067899103883531383580500542532805
+741345583372708758677381254341695646215212764479558601822324496916305564860
+906223455619847457072543249061510257957686047823824674682567491887881744554
+-767849295212578246709801782763128612227201311770055823223370752694466982385
+-499605824796177847482548145602529914672118948474574930466002320448397702145
+-739783929947191450539981235446122797172963523649497524598736585887720470605
+11906781661858318111608384113371656853984100876730919753607956359054872835
+1184591657410410618259810478559756080508915282346219818107533089968423438529
+-1196756736539952528850324578540484369187211012447802934902211689810543298321
+-615406306260154438751417537243664316178100185892451009663053034794681290878
+-479989799644409226462391378855274180707944349292197032426785420935231903693
+1666094585867140022923253270503506891580143265539166904031542100935830693071
+874739451078007766457464989774322083649278607533249481151382481072868806602
+152666792071518830868575557812948353041420400780739481342941381225525861407
+1

tests/Casm/Compilation/positive/test079.juvix

@@ -0,0 +1,284 @@
+--- Trivial resource logic
+module test079;
+
+import Stdlib.Prelude open;
+import Stdlib.Cairo.Ec as Ec;
+import Stdlib.Cairo.Poseidon open;
+import Stdlib.Cairo.Pedersen open;
+
+type Resource :=
+  mkResource@{
+    logic : Field;
+    label : Field;
+    quantity : Field;
+    data : Field;
+    eph : Bool;
+    nonce : Field;
+    npk : Field;
+    rseed : Field;
+  };
+
+type LogicResult :=
+  mkResult@{
+    -- nullifier of input resource or commitment of output resource
+    self_resource_id : Field;
+    -- The merkle root of resources
+    root : Field;
+    cipher_text_elem0 : Field;
+    cipher_text_elem1 : Field;
+    cipher_text_elem2 : Field;
+    cipher_text_elem3 : Field;
+    cipher_text_elem4 : Field;
+    cipher_text_elem5 : Field;
+    cipher_text_elem6 : Field;
+    cipher_text_elem7 : Field;
+    cipher_text_elem8 : Field;
+    cipher_text_elem9 : Field;
+    mac : Field;
+    pk_x : Field;
+    pk_y : Field;
+    nonce : Field;
+  };
+
+check_merkle (current_root : Field) : Pair 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 (Pair Field Bool) -> Field
+  | [] := cur
+  | (p :: ps) := check_merkle_path (check_merkle cur p) ps;
+
+type EncryptionResult :=
+  mkEncryptionResult@{
+    cipher_text_elem0 : Field;
+    cipher_text_elem1 : Field;
+    cipher_text_elem2 : Field;
+    cipher_text_elem3 : Field;
+    cipher_text_elem4 : Field;
+    cipher_text_elem5 : Field;
+    cipher_text_elem6 : Field;
+    cipher_text_elem7 : Field;
+    cipher_text_elem8 : Field;
+    cipher_text_elem9 : Field;
+    mac : Field;
+    sender_pk_x : Field;
+    sender_pk_y : Field;
+    nonce : Field;
+  };
+
+type Cipher :=
+  mkCipher@{
+    cipher_text : List Field;
+    cur_state : Field;
+  };
+
+update_poseidon_state
+  (cur_msg secret_key_x : Field) (cipher : Cipher) : Cipher :=
+  let
+    new_state := Cipher.cur_state cipher + cur_msg;
+    new_text := new_state :: Cipher.cipher_text cipher;
+  in mkCipher@{
+       cipher_text := new_text;
+       cur_state := poseidonHash2 new_state secret_key_x;
+     };
+
+generate_cipher
+  (poseidon_state : Field)
+  (secret_key_x : Field)
+  (plaintext : List Field)
+  : Cipher :=
+  let
+    go (cipher : Cipher) : List Field -> Cipher
+      | [] := cipher@Cipher{cipher_text := reverse (Cipher.cipher_text cipher)}
+      | (m :: ms) := go (update_poseidon_state m secret_key_x cipher) ms;
+  in go
+    mkCipher@{
+      cipher_text := [];
+      cur_state := poseidon_state;
+    }
+    plaintext;
+
+encryption
+  (messages : List Field)
+  (pk_x : Field)
+  (pk_y : Field)
+  (sk : Field)
+  (nonce : Field)
+  : EncryptionResult :=
+
+  let
+    -- Generate encryption key
+    pk := Ec.mkPoint pk_x pk_y;
+    secret_key := Ec.mul sk pk;
+
+    -- PLAINTEXT_NUM := 10;
+
+    -- TODO: Pad the messages here or outside of the circuit?
+    plaintext := messages;
+
+    -- Init poseidon state
+    secret_key_x := Ec.Point.x secret_key;
+    poseidon_state :=
+      poseidonHashList [secret_key_x; Ec.Point.y secret_key; nonce; 10];
+
+    -- Generate cipher
+    final_cipher := generate_cipher poseidon_state secret_key_x plaintext;
+
+    -- Get MAC
+    mac := Cipher.cur_state final_cipher;
+
+    -- Generate sender's pk
+    generator := Ec.mkPoint Ec.StarkCurve.GEN_X Ec.StarkCurve.GEN_Y;
+    sender_pk := Ec.mul sk generator;
+
+  in case Cipher.cipher_text final_cipher of
+       | [
+           elem0;
+           elem1;
+           elem2;
+           elem3;
+           elem4;
+           elem5;
+           elem6;
+           elem7;
+           elem8;
+           elem9;
+         ] :=
+         mkEncryptionResult@{
+           cipher_text_elem0 := elem0;
+           cipher_text_elem1 := elem1;
+           cipher_text_elem2 := elem2;
+           cipher_text_elem3 := elem3;
+           cipher_text_elem4 := elem4;
+           cipher_text_elem5 := elem5;
+           cipher_text_elem6 := elem6;
+           cipher_text_elem7 := elem7;
+           cipher_text_elem8 := elem8;
+           cipher_text_elem9 := elem9;
+           mac;
+           sender_pk_x := Ec.Point.x sender_pk;
+           sender_pk_y := Ec.Point.y sender_pk;
+           nonce;
+         }
+       | _ := mkEncryptionResult 0 0 0 0 0 0 0 0 0 0 0 0 0 0;
+
+main
+  (self_resource : Resource)
+  (resource_nf_key : Field)
+  (merkle_path : List (Pair Field Bool))
+  : LogicResult :=
+
+  -- Check the self_resource resource commitment:
+  let
+    generated_npk : Field := poseidonHash2 resource_nf_key 0;
+
+    is_output_resource :=
+      case merkle_path of
+        -- merkle_path can not be empty
+        | nil := true
+        | (_, is_left) :: t := is_left;
+
+    -- Actual npk
+    actual_npk :=
+      if
+        | is_output_resource := Resource.npk self_resource
+        | else := generated_npk;
+
+    -- check outside of circuit: assert resource_npk == (Resource.npk self_resource)
+
+    -- PRF_EXPAND_PERSONALIZATION_FELT is from cairo_prover/src/lib.rs/PRF_EXPAND_PERSONALIZATION_FELT
+    PRF_EXPAND_PERSONALIZATION_FELT := 89564067232354163924078705540990330212;
+    resource_psi :=
+      poseidonHashList
+        [
+          PRF_EXPAND_PERSONALIZATION_FELT;
+          0;
+          Resource.rseed self_resource;
+          Resource.nonce self_resource;
+        ];
+    resource_rcm :=
+      poseidonHashList
+        [
+          PRF_EXPAND_PERSONALIZATION_FELT;
+          1;
+          Resource.rseed self_resource;
+          Resource.nonce self_resource;
+        ];
+
+    resource_eph_field : Field :=
+      if
+        | Resource.eph self_resource := 1
+        | else := 0;
+    resource_cm :=
+      poseidonHashList
+        [
+          Resource.logic self_resource;
+          Resource.label self_resource;
+          Resource.data self_resource;
+          actual_npk;
+          Resource.nonce self_resource;
+          resource_psi;
+          Resource.quantity self_resource;
+          resource_eph_field;
+          resource_rcm;
+        ];
+
+    -- Generate the nullifier of self_resource resource
+    resource_nullifier_ :=
+      poseidonHashList
+        [
+          resource_nf_key;
+          Resource.nonce self_resource;
+          resource_psi;
+          resource_cm;
+        ];
+
+    self_resource_id_ :=
+      if
+        | is_output_resource := resource_cm
+        | else := resource_nullifier_;
+
+    root_ := check_merkle_path self_resource_id_ merkle_path;
+
+    -- Encryption
+    messages :=
+      [
+        Resource.logic self_resource;
+        Resource.label self_resource;
+        Resource.quantity self_resource;
+        Resource.data self_resource;
+        resource_eph_field;
+        Resource.nonce self_resource;
+        Resource.npk self_resource;
+        Resource.rseed self_resource;
+        0;
+        0;
+      ];
+
+    cihper := encryption messages Ec.StarkCurve.GEN_X Ec.StarkCurve.GEN_Y 1 1;
+  -- cihper_ := encryption [Resource.logic self_resource; Resource.label self_resource; Resource.quantity self_resource; Resource.data self_resource; Resource.eph self_resource; Resource.nonce self_resource; Resource.npk self_resource; Resource.rseed self_resource; 0; 0 ] Ec.StarkCurve.GEN_X Ec.StarkCurve.GEN_Y 1 1;
+  in mkResult@{
+       self_resource_id := self_resource_id_;
+       root := root_;
+       cipher_text_elem0 := EncryptionResult.cipher_text_elem0 cihper;
+       cipher_text_elem1 := EncryptionResult.cipher_text_elem1 cihper;
+       cipher_text_elem2 := EncryptionResult.cipher_text_elem2 cihper;
+       cipher_text_elem3 := EncryptionResult.cipher_text_elem3 cihper;
+       cipher_text_elem4 := EncryptionResult.cipher_text_elem4 cihper;
+       cipher_text_elem5 := EncryptionResult.cipher_text_elem5 cihper;
+       cipher_text_elem6 := EncryptionResult.cipher_text_elem6 cihper;
+       cipher_text_elem7 := EncryptionResult.cipher_text_elem7 cihper;
+       cipher_text_elem8 := EncryptionResult.cipher_text_elem8 cihper;
+       cipher_text_elem9 := EncryptionResult.cipher_text_elem9 cihper;
+       mac := EncryptionResult.mac cihper;
+       pk_x := EncryptionResult.sender_pk_x cihper;
+       pk_y := EncryptionResult.sender_pk_y cihper;
+       nonce := EncryptionResult.nonce cihper;
+     };

tests/Casm/Reg/positive/in/test044.json

@@ -0,0 +1,3 @@
+{
+    "val": 10
+}