diff --git a/src/Juvix/Compiler/Casm/Translation/FromReg.hs b/src/Juvix/Compiler/Casm/Translation/FromReg.hs index 2ea500f89f..4ad691280f 100644 --- a/src/Juvix/Compiler/Casm/Translation/FromReg.hs +++ b/src/Juvix/Compiler/Casm/Translation/FromReg.hs @@ -194,7 +194,9 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI Nothing -> do massert (isJust mout) massert (HashSet.member (fromJust mout) liveVars0) - goCallBlock False Nothing liveVars0 + goAssignApBuiltins + whenJust mout saveLiveVar + goCallBlock mout liveVars0 where output'' :: Instruction -> Sem r () output'' i = do @@ -206,22 +208,24 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI output'' i incAP apOff - goCallBlock :: Bool -> Maybe Reg.VarRef -> HashSet Reg.VarRef -> Sem r () - goCallBlock updatedBuiltins outVar liveVars = do - let liveVars' = toList (maybe liveVars (`HashSet.delete` liveVars) outVar) + saveLiveVar :: Reg.VarRef -> Sem r () + saveLiveVar var = do + ref <- mkMemRef var + let comment = Reg.ppPrint tab var + goAssignAp' (Just comment) (Val (Ref ref)) + + -- The `goCallBlock` function is used to switch to a new basic block. + -- Assumes that the builtins pointer and outVar (if present) were + -- already saved (in this order). + goCallBlock :: Maybe Reg.VarRef -> HashSet Reg.VarRef -> Sem r () + goCallBlock outVar liveVars = do + let liveVars' = sort $ toList (maybe liveVars (`HashSet.delete` liveVars) outVar) n = length liveVars' - bltOff = - if - | updatedBuiltins -> - -argsOffset - n - fromEnum (isJust outVar) - | otherwise -> - -argsOffset - n + bltOff = -argsOffset - n - fromEnum (isJust outVar) vars = HashMap.fromList $ - maybe [] (\var -> [(var, -argsOffset - n - if updatedBuiltins then 0 else 1)]) outVar + maybe [] (\var -> [(var, -argsOffset - n)]) outVar ++ zipWithExact (\var k -> (var, -argsOffset - k)) liveVars' [0 .. n - 1] - unless updatedBuiltins $ - goAssignApBuiltins mapM_ saveLiveVar (reverse liveVars') output'' (mkCallRel $ Imm 3) output'' Return @@ -232,12 +236,6 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI setAP 0 setVars vars setBuiltinOffset bltOff - where - saveLiveVar :: Reg.VarRef -> Sem r () - saveLiveVar var = do - ref <- mkMemRef var - let comment = Reg.ppPrint tab var - goAssignAp' (Just comment) (Val (Ref ref)) goLocalBlock :: Int -> HashMap Reg.VarRef Int -> Int -> HashSet Reg.VarRef -> Maybe Reg.VarRef -> Reg.Block -> Sem r () goLocalBlock ap0 vars bltOff liveVars mout' block = do @@ -573,7 +571,11 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI val <- mkMemRef _instrExtendClosureValue goAssignAp (Val $ Ref val) output'' $ mkCallRel $ Lab $ LabelRef (blts ^. stdlibExtendClosure) (Just (blts ^. stdlibExtendClosureName)) - goCallBlock False (Just _instrExtendClosureResult) liveVars + -- the `juvix_extend_closure` runtime function does not accept or + -- return the builtins pointer + goAssignApBuiltins + goAssignAp (Val $ Ref $ MemRef Ap (-2)) + goCallBlock (Just _instrExtendClosureResult) liveVars goCall' :: Reg.CallType -> [Reg.Value] -> Sem r () goCall' ct args = case ct of @@ -593,7 +595,7 @@ fromReg tab = mkResult $ run $ runLabelInfoBuilderWithNextId (Reg.getNextSymbolI goCall :: HashSet Reg.VarRef -> Reg.InstrCall -> Sem r () goCall liveVars Reg.InstrCall {..} = do goCall' _instrCallType _instrCallArgs - goCallBlock True (Just _instrCallResult) liveVars + goCallBlock (Just _instrCallResult) liveVars -- There is no way to make "proper" tail calls in Cairo, because -- the only way to set the `fp` register is via the `call` instruction. diff --git a/src/Juvix/Compiler/Reg/Language/Instrs.hs b/src/Juvix/Compiler/Reg/Language/Instrs.hs index 55da2a0387..507ad9425f 100644 --- a/src/Juvix/Compiler/Reg/Language/Instrs.hs +++ b/src/Juvix/Compiler/Reg/Language/Instrs.hs @@ -26,7 +26,7 @@ data ConstrField = ConstrField data VarGroup = VarGroupArgs | VarGroupLocal - deriving stock (Eq, Generic, Show) + deriving stock (Eq, Ord, Generic, Show) instance Hashable VarGroup @@ -48,6 +48,9 @@ instance Eq VarRef where vr1 ^. varRefGroup == vr2 ^. varRefGroup && vr1 ^. varRefIndex == vr2 ^. varRefIndex +instance Ord VarRef where + compare = compare `on` \vr -> (vr ^. varRefGroup, vr ^. varRefIndex) + deriving stock instance (Eq ConstrField) deriving stock instance (Eq Value) diff --git a/test/Casm/Compilation/Positive.hs b/test/Casm/Compilation/Positive.hs index b644123aaf..95951c0cde 100644 --- a/test/Casm/Compilation/Positive.hs +++ b/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") ] diff --git a/test/Casm/Reg/Cairo.hs b/test/Casm/Reg/Cairo.hs index 05b541464a..730ceb1b16 100644 --- a/test/Casm/Reg/Cairo.hs +++ b/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")) ] diff --git a/test/Casm/Reg/Positive.hs b/test/Casm/Reg/Positive.hs index 2a75405e7a..0825be2556 100644 --- a/test/Casm/Reg/Positive.hs +++ b/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")) ] diff --git a/tests/Casm/Compilation/positive/in/test079.json b/tests/Casm/Compilation/positive/in/test079.json new file mode 100644 index 0000000000..c7a6a2f5ff --- /dev/null +++ b/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 + } + ] +} diff --git a/tests/Casm/Compilation/positive/out/test079.out b/tests/Casm/Compilation/positive/out/test079.out new file mode 100644 index 0000000000..9855d1c8f8 --- /dev/null +++ b/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 diff --git a/tests/Casm/Compilation/positive/test079.juvix b/tests/Casm/Compilation/positive/test079.juvix new file mode 100644 index 0000000000..296017de8e --- /dev/null +++ b/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; + }; diff --git a/tests/Casm/Reg/positive/in/test044.json b/tests/Casm/Reg/positive/in/test044.json new file mode 100644 index 0000000000..09cd5f957e --- /dev/null +++ b/tests/Casm/Reg/positive/in/test044.json @@ -0,0 +1,3 @@ +{ + "val": 10 +} diff --git a/tests/Casm/Reg/positive/in/test045.json b/tests/Casm/Reg/positive/in/test045.json new file mode 100644 index 0000000000..09cd5f957e --- /dev/null +++ b/tests/Casm/Reg/positive/in/test045.json @@ -0,0 +1,3 @@ +{ + "val": 10 +} diff --git a/tests/Casm/Reg/positive/in/test046.json b/tests/Casm/Reg/positive/in/test046.json new file mode 100644 index 0000000000..09cd5f957e --- /dev/null +++ b/tests/Casm/Reg/positive/in/test046.json @@ -0,0 +1,3 @@ +{ + "val": 10 +} diff --git a/tests/Casm/Reg/positive/in/test047.json b/tests/Casm/Reg/positive/in/test047.json new file mode 100644 index 0000000000..09cd5f957e --- /dev/null +++ b/tests/Casm/Reg/positive/in/test047.json @@ -0,0 +1,3 @@ +{ + "val": 10 +} diff --git a/tests/Casm/Reg/positive/in/test048.json b/tests/Casm/Reg/positive/in/test048.json new file mode 100644 index 0000000000..c7a6a2f5ff --- /dev/null +++ b/tests/Casm/Reg/positive/in/test048.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 + } + ] +} diff --git a/tests/Casm/Reg/positive/out/test044.out b/tests/Casm/Reg/positive/out/test044.out new file mode 100644 index 0000000000..b4de394767 --- /dev/null +++ b/tests/Casm/Reg/positive/out/test044.out @@ -0,0 +1 @@ +11 diff --git a/tests/Casm/Reg/positive/out/test045.out b/tests/Casm/Reg/positive/out/test045.out new file mode 100644 index 0000000000..b4de394767 --- /dev/null +++ b/tests/Casm/Reg/positive/out/test045.out @@ -0,0 +1 @@ +11 diff --git a/tests/Casm/Reg/positive/out/test046.out b/tests/Casm/Reg/positive/out/test046.out new file mode 100644 index 0000000000..48082f72f0 --- /dev/null +++ b/tests/Casm/Reg/positive/out/test046.out @@ -0,0 +1 @@ +12 diff --git a/tests/Casm/Reg/positive/out/test047.out b/tests/Casm/Reg/positive/out/test047.out new file mode 100644 index 0000000000..2bd5a0a98a --- /dev/null +++ b/tests/Casm/Reg/positive/out/test047.out @@ -0,0 +1 @@ +22 diff --git a/tests/Casm/Reg/positive/out/test048.out b/tests/Casm/Reg/positive/out/test048.out new file mode 100644 index 0000000000..fd88d17557 --- /dev/null +++ b/tests/Casm/Reg/positive/out/test048.out @@ -0,0 +1 @@ +-245332851819226602385083744327390214455788255951827084039649627662983776294 diff --git a/tests/Casm/Reg/positive/test044.jvr b/tests/Casm/Reg/positive/test044.jvr new file mode 100644 index 0000000000..4bea0317f9 --- /dev/null +++ b/tests/Casm/Reg/positive/test044.jvr @@ -0,0 +1,20 @@ +-- Extend closure in true branch + +function f(x : field, y : field) : field { + tmp[0] = fadd x y; + ret tmp[0]; +} + +function main(val : field) : field { + tmp[0] = calloc f (); + br val, out: tmp[1] { + true: { + tmp[1] = cextend tmp[0] (1); + }; + false: { + tmp[1] = calloc f (1); + }; + }; + tmp[2] = call tmp[1] (val); + ret tmp[2]; +} diff --git a/tests/Casm/Reg/positive/test045.jvr b/tests/Casm/Reg/positive/test045.jvr new file mode 100644 index 0000000000..c1b1cce2f2 --- /dev/null +++ b/tests/Casm/Reg/positive/test045.jvr @@ -0,0 +1,20 @@ +-- Extend closure in false branch + +function f(x : field, y : field) : field { + tmp[0] = fadd x y; + ret tmp[0]; +} + +function main(val : field) : field { + tmp[0] = calloc f (); + br val, out: tmp[1] { + true: { + tmp[1] = calloc f (1); + }; + false: { + tmp[1] = cextend tmp[0] (1); + }; + }; + tmp[2] = call tmp[1] (val); + ret tmp[2]; +} diff --git a/tests/Casm/Reg/positive/test046.jvr b/tests/Casm/Reg/positive/test046.jvr new file mode 100644 index 0000000000..00788c4423 --- /dev/null +++ b/tests/Casm/Reg/positive/test046.jvr @@ -0,0 +1,20 @@ +-- Call in true branch + +function f(x : field) : field { + tmp[0] = fadd x 1F; + ret tmp[0]; +} + +function main(val : field) : field { + tmp[0] = fadd val 1F; + br val, out: tmp[1] { + true: { + tmp[1] = call f (val); + }; + false: { + tmp[1] = 1; + }; + }; + tmp[2] = fadd tmp[1] tmp[0]; + ret tmp[2]; +} diff --git a/tests/Casm/Reg/positive/test047.jvr b/tests/Casm/Reg/positive/test047.jvr new file mode 100644 index 0000000000..0a74fea229 --- /dev/null +++ b/tests/Casm/Reg/positive/test047.jvr @@ -0,0 +1,20 @@ +-- Call in false branch + +function f(x : field) : field { + tmp[0] = fadd x 1F; + ret tmp[0]; +} + +function main(val : field) : field { + tmp[0] = fadd val 1F; + br val, out: tmp[1] { + true: { + tmp[1] = 1; + }; + false: { + tmp[1] = call f (val); + }; + }; + tmp[2] = fadd tmp[1] tmp[0]; + ret tmp[2]; +} diff --git a/tests/Casm/Reg/positive/test048.jvr b/tests/Casm/Reg/positive/test048.jvr new file mode 100644 index 0000000000..c987ebdfa9 --- /dev/null +++ b/tests/Casm/Reg/positive/test048.jvr @@ -0,0 +1,116 @@ +-- Mock resource logic + +type Pair { + __comma__ : (*, *) -> Pair; +} + +type List { + nil : List; + __colon____colon__ : (*, List) -> List; +} + +type Resource { + mkResource : (field, field, field, field, bool, field, field, field) -> Resource; +} + +type LogicResult { + mkResult : field -> LogicResult; +} + +function poseidonHashList'(List) : field; +function poseidonHash2'(field, field) : field; +function main(Resource, field, List) : LogicResult; + +function poseidonHashList'(_X : List) : field { + tmp[1] = _X; + case[List] tmp[1] { + __colon____colon__: { + { + tmp[0] = tmp[1]; + tmp[1] = tmp[0].__colon____colon__[1]; + tmp[1] = call poseidonHashList' (tmp[1]); + tmp[2] = tmp[0].__colon____colon__[0]; + tmp[1] = fadd tmp[2] tmp[1]; + ret tmp[1]; + }; + }; + nil: { + nop; + tmp[1] = 0F; + ret tmp[1]; + }; + }; +} + +function poseidonHash2'(x : field, y : field) : field { + tmp[0] = y; + tmp[1] = x; + tmp[0] = fadd tmp[1] tmp[0]; + ret tmp[0]; +} + +function main(self_resource : Resource, resource_nf_key : field, merkle_path : List) : LogicResult { + tmp[2] = alloc nil (); + tmp[3] = alloc nil (); + tmp[4] = self_resource; + case[Resource] tmp[4], out: tmp[4] { + mkResource: { + tmp[0] = tmp[4]; + tmp[4] = tmp[0].mkResource[2]; + }; + }; + tmp[3] = alloc __colon____colon__ (tmp[4], tmp[3]); + tmp[4] = self_resource; + case[Resource] tmp[4], out: tmp[4] { + mkResource: { + tmp[0] = tmp[4]; + tmp[4] = tmp[0].mkResource[5]; + }; + }; + tmp[3] = alloc __colon____colon__ (tmp[4], tmp[3]); + tmp[4] = merkle_path; + case[List] tmp[4], out: tmp[4] { + __colon____colon__: { + { + tmp[0] = tmp[4]; + tmp[4] = tmp[0].__colon____colon__[0]; + case[Pair] tmp[4], out: tmp[4] { + __comma__: { + { + tmp[1] = tmp[4]; + tmp[4] = tmp[1].__comma__[1]; + }; + }; + }; + }; + }; + nil: { + nop; + tmp[4] = true; + }; + }; + br tmp[4], out: tmp[4] { + true: { + tmp[4] = self_resource; + case[Resource] tmp[4], out: tmp[4] { + mkResource: { + tmp[0] = tmp[4]; + tmp[4] = tmp[0].mkResource[6]; + }; + }; + }; + false: { + tmp[4] = 0F; + tmp[5] = resource_nf_key; + tmp[4] = call poseidonHash2' (tmp[5], tmp[4]); + }; + }; + tmp[3] = alloc __colon____colon__ (tmp[4], tmp[3]); + tmp[3] = call poseidonHashList' (tmp[3]); + tmp[2] = alloc __colon____colon__ (tmp[3], tmp[2]); + tmp[3] = resource_nf_key; + tmp[2] = alloc __colon____colon__ (tmp[3], tmp[2]); + tmp[2] = call poseidonHashList' (tmp[2]); + tmp[2] = alloc mkResult (tmp[2]); + ret tmp[2]; +}