From ed114ae2a336ed7516ee4b1aa91f374897d4dfb2 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Mon, 2 Dec 2024 10:24:44 +0100 Subject: [PATCH] Re-enable resource machine builtins tests --- test/Anoma/Compilation/Positive.hs | 13 +- .../Anoma/Compilation/positive/Package.juvix | 2 +- .../Anoma/Compilation/positive/test085.juvix | 92 ------------- .../positive/test085/Package.juvix | 9 ++ .../positive/test085/client/Package.juvix | 8 ++ .../test085/client/ResourceMachine.juvix | 130 ++++++++++++++++++ .../Compilation/positive/test085/delta.juvix | 40 ++++++ 7 files changed, 194 insertions(+), 100 deletions(-) delete mode 100644 tests/Anoma/Compilation/positive/test085.juvix create mode 100644 tests/Anoma/Compilation/positive/test085/Package.juvix create mode 100644 tests/Anoma/Compilation/positive/test085/client/Package.juvix create mode 100644 tests/Anoma/Compilation/positive/test085/client/ResourceMachine.juvix create mode 100644 tests/Anoma/Compilation/positive/test085/delta.juvix diff --git a/test/Anoma/Compilation/Positive.hs b/test/Anoma/Compilation/Positive.hs index 6b3541aef5..fb3affd259 100644 --- a/test/Anoma/Compilation/Positive.hs +++ b/test/Anoma/Compilation/Positive.hs @@ -250,7 +250,7 @@ classify AnomaTest {..} = case _anomaTestNum of 82 -> ClassWorking 83 -> ClassWorking 84 -> ClassWorking - 85 -> ClassNodeError + 85 -> ClassWorking 86 -> ClassExpectedFail _ -> error "non-exhaustive test classification" @@ -1039,14 +1039,13 @@ allTests = 85 AnomaTestModeNodeOnly "Anoma Resource Machine builtins" - $(mkRelDir ".") - $(mkRelFile "test085.juvix") + $(mkRelDir "test085") + $(mkRelFile "delta.juvix") [] $ checkOutput - [ [nock| [[[11 22] 110] 0] |], - [nock| [10 11] |], - [nock| 478793196187462788804451 |], - [nock| 418565088612 |], + [ [nock| 0 |], + [nock| 0 |], + [nock| 0 |], [nock| 0 |] ], mkAnomaTest diff --git a/tests/Anoma/Compilation/positive/Package.juvix b/tests/Anoma/Compilation/positive/Package.juvix index 2f2f7969e7..39b0d6b001 100644 --- a/tests/Anoma/Compilation/positive/Package.juvix +++ b/tests/Anoma/Compilation/positive/Package.juvix @@ -4,5 +4,5 @@ import PackageDescription.V2 open; package : Package := defaultPackage@?{ - name := "positive" + name := "positive"; }; diff --git a/tests/Anoma/Compilation/positive/test085.juvix b/tests/Anoma/Compilation/positive/test085.juvix deleted file mode 100644 index 04a3eb7b3b..0000000000 --- a/tests/Anoma/Compilation/positive/test085.juvix +++ /dev/null @@ -1,92 +0,0 @@ -module test085; - -import Stdlib.Prelude open; -import Stdlib.Debug.Trace open; - --- This definition does not match the spec. For testing purposes only -builtin anoma-resource -type Resource := - mkResource@{ - label : Nat; - logic : Nat; - ephemeral : Bool; - quantity : Nat; - data : Pair Nat Nat; - nullifier-key : Nat; - nonce : Nat; - rseed : Nat - }; - -mkResource' (label logic : Nat) {quantity : Nat := 0} : Resource := - mkResource@{ - label; - logic; - ephemeral := false; - quantity; - data := 0, 0; - nullifier-key := 0; - nonce := 0; - rseed := 0 - }; - --- This definition does not match the spec. For testing purposes only -builtin anoma-action -type Action := mkAction Nat; - -builtin anoma-delta -axiom Delta : Type; - -builtin anoma-kind -axiom Kind : Type; - -builtin anoma-resource-commitment -axiom commitment : Resource -> Nat; - -builtin anoma-resource-nullifier -axiom nullifier : Resource -> Nat; - -builtin anoma-resource-kind -axiom kind : Resource -> Kind; - -builtin anoma-resource-delta -axiom resourceDelta : Resource -> Delta; - -builtin anoma-action-delta -axiom actionDelta : Action -> Delta; - -builtin anoma-actions-delta -axiom actionsDelta : List Action -> Delta; - -builtin anoma-prove-action -axiom proveAction : Action -> Nat; - -builtin anoma-prove-delta -axiom proveDelta : Delta -> Nat; - -builtin anoma-zero-delta -axiom zeroDelta : Delta; - -builtin anoma-add-delta -axiom addDelta : Delta -> Delta -> Delta; - -builtin anoma-sub-delta -axiom subDelta : Delta -> Delta -> Delta; - -main : Delta := - trace - (resourceDelta - mkResource'@{ - label := 11; - logic := 22; - quantity := 55 - }) - >-> trace (commitment (mkResource' 0 0)) - >-> trace (nullifier (mkResource' 0 0)) - >-> trace (actionDelta (mkAction 0)) - >-> trace (actionsDelta [mkAction 0]) - >-> trace (addDelta zeroDelta zeroDelta) - >-> trace (subDelta zeroDelta zeroDelta) - >-> trace (kind (mkResource' 10 11)) - >-> trace (proveAction (mkAction 0)) - >-> trace (proveDelta zeroDelta) - >-> zeroDelta; diff --git a/tests/Anoma/Compilation/positive/test085/Package.juvix b/tests/Anoma/Compilation/positive/test085/Package.juvix new file mode 100644 index 0000000000..613da5f3b1 --- /dev/null +++ b/tests/Anoma/Compilation/positive/test085/Package.juvix @@ -0,0 +1,9 @@ +module Package; + +import PackageDescription.V2 open; + +package : Package := + defaultPackage@?{ + name := "test085"; + dependencies := [defaultStdlib; path "client/"]; + }; diff --git a/tests/Anoma/Compilation/positive/test085/client/Package.juvix b/tests/Anoma/Compilation/positive/test085/client/Package.juvix new file mode 100644 index 0000000000..7a1c28caf9 --- /dev/null +++ b/tests/Anoma/Compilation/positive/test085/client/Package.juvix @@ -0,0 +1,8 @@ +module Package; + +import PackageDescription.V2 open; + +package : Package := + defaultPackage@?{ + name := "addtransaction"; + }; diff --git a/tests/Anoma/Compilation/positive/test085/client/ResourceMachine.juvix b/tests/Anoma/Compilation/positive/test085/client/ResourceMachine.juvix new file mode 100644 index 0000000000..7e98d1fed8 --- /dev/null +++ b/tests/Anoma/Compilation/positive/test085/client/ResourceMachine.juvix @@ -0,0 +1,130 @@ +--- A rendering of https://github.com/anoma/anoma/blob/f52cd44235f35a907c22c428ce1fdf3237c97927/hoon/resource-machine.hoon +module ResourceMachine; + +import Stdlib.Prelude open; + +module Resource; + + Resource-Logic : Type := Public-Inputs -> Private-Inputs -> Bool; + + builtin anoma-resource + type Resource := + mkResource@{ + label : Nat; + logic : Resource-Logic; + ephemeral : Bool; + quantity : Nat; + data : Pair Nat Nat; + --- 256 bits + nullifier-key : Nat; + --- nonce for commitments 256 bits + nonce : Nat; + rseed : Nat; + }; + + positive + type Public-Inputs := + mkPublic-Inputs@{ + commitments : List Nat; + nullifiers : List Nat; + --- exactly one commitment or nullifier + self-tag : Nat; + other-public : Nat; + }; + + positive + type Private-Inputs := + mkPrivate-Inputs@{ + committed-resources : List Resource; + nullified-resources : List Resource; + other-private : Nat; + }; + +end; + +open Resource using { + Resource; + mkResource; + Resource-Logic; + Public-Inputs; + mkPublic-Inputs; + Private-Inputs; + mkPrivate-Inputs; +} public; + +builtin anoma-delta +axiom Delta : Type; + +builtin anoma-kind +axiom Kind : Type; + +builtin anoma-resource-commitment +axiom commitment : Resource -> Nat; + +builtin anoma-resource-nullifier +axiom nullifier : Resource -> Nat; + +builtin anoma-resource-kind +axiom kind : Resource -> Kind; + +builtin anoma-resource-delta +axiom resource-delta : Resource -> Delta; + +type Logic-Proof : Type := + mkLogicProof@{ + resource : Resource; + inputs : Pair Public-Inputs Private-Inputs; + }; + +Compliance-Proof : Type := Nat; + +type Proof := + | proofCompliance + | proofLogic Resource (Pair Public-Inputs Private-Inputs); + +mkProofCompliance (_ : Compliance-Proof) : Proof := proofCompliance; + +mkProofLogic + (resource : Resource) (inputs : Pair Public-Inputs Private-Inputs) : Proof := + proofLogic resource inputs; + +builtin anoma-action +type Action := + mkAction@{ + commitments : List Nat; + nullifiers : List Nat; + proofs : List Proof; + app-data : Nat; + }; + +builtin anoma-action-delta +axiom actionDelta : Action -> Delta; + +builtin anoma-actions-delta +axiom actionsDelta : List Action -> Delta; + +builtin anoma-prove-action +axiom proveAction : Action -> Nat; + +builtin anoma-prove-delta +axiom proveDelta : Delta -> Nat; + +builtin anoma-zero-delta +axiom zeroDelta : Delta; + +builtin anoma-add-delta +axiom addDelta : Delta -> Delta -> Delta; + +builtin anoma-sub-delta +axiom subDelta : Delta -> Delta -> Delta; + +Commitment-Root : Type := Nat; + +type Transaction := + mkTransaction@{ + --- root set for spent resources + roots : List Commitment-Root; + actions : List Action; + delta : Delta; + delta-proof : Nat; + }; diff --git a/tests/Anoma/Compilation/positive/test085/delta.juvix b/tests/Anoma/Compilation/positive/test085/delta.juvix new file mode 100644 index 0000000000..7bbb7b2401 --- /dev/null +++ b/tests/Anoma/Compilation/positive/test085/delta.juvix @@ -0,0 +1,40 @@ +module delta; + +import Stdlib.Prelude open; +import Stdlib.Debug.Trace open; +import ResourceMachine open; + +main : Delta := + let + resource : Resource := + mkResource@{ + label := 11; + logic := \{_ _ := true}; + ephemeral := true; + quantity := 55; + data := 0, 0; + nullifier-key := 0; + nonce := 0; + rseed := 0; + }; + action : Action := + mkAction@{ + commitments := []; + nullifiers := []; + proofs := []; + app-data := 1; + }; + in -- Most of these call return large nouns that are not appropritate for testing. + -- This test checks that these functions do not crash. + commitment + resource + >-> nullifier resource + >-> kind resource + >-> addDelta (resource-delta resource) (resource-delta resource) + >-> addDelta (resource-delta resource) (resource-delta resource) + >-> proveDelta zeroDelta + >-> trace (subDelta zeroDelta zeroDelta) + >-> trace (addDelta zeroDelta zeroDelta) + >-> proveAction action + >-> trace (actionDelta action) + >-> actionsDelta [action];