init

.github/workflows/tests.yaml

@@ -0,0 +1,24 @@
+name: Test juvix-arm-specs
+'on':
+  push:
+    branches:
+      - main
+  pull_request: null
+  workflow_dispatch: null
+jobs:
+  test:
+    name: Run test suite
+    runs-on: ubuntu-latest
+    steps:
+      - name: checkout code
+        uses: actions/checkout@v3
+      - name: Download latest nightly Juvix binary
+        uses: jaxxstorm/[email protected]
+        with:
+          repo: anoma/juvix-nightly-builds
+
+          cache: enable
+      - name: Clean & Update Dependencies
+        run: juvix clean --global && juvix clean && juvix dependencies update
+      - name: Typecheck
+        run: juvix typecheck

.gitignore

@@ -0,0 +1,4 @@
+.juvix-build
+.history
+*.nockma
+.DS_Store

Anoma/Delta.juvix

@@ -0,0 +1,22 @@
+module Anoma.Delta;
+
+import Stdlib.Prelude open;
+import Anoma.MathProperty as MathProperty open;
+
+axiom Delta : Type;
+
+axiom addDelta : Delta -> Delta -> Delta;
+
+axiom zero : Delta;
+
+instance
+Delta-AdditivelyHomomorphic : MathProperty.AdditivelyHomomorphic Delta :=
+  MathProperty.mkAdditivelyHomomorphic@{
+    add (a b : Delta) : Delta := addDelta a b
+  };
+
+instance
+Delta-KindDistinct : MathProperty.KindDistinct Delta :=
+  MathProperty.mkKindDistinct@{
+    add (a b : Delta) : Delta := addDelta a b
+  };

Anoma/MathProperty.juvix

@@ -0,0 +1,13 @@
+module Anoma.MathProperty;
+
+import Stdlib.Prelude open;
+
+trait
+type AdditivelyHomomorphic T := mkAdditivelyHomomorphic {add : T -> T -> T};
+
+Property-AdditivelyHomomorphic
+  {T} {{Eq T}} {{AdditivelyHomomorphic T}} (f : T -> T) (x y : T) : Bool :=
+  f (AdditivelyHomomorphic.add x y) == AdditivelyHomomorphic.add (f x) (f y);
+
+trait
+type KindDistinct T := mkKindDistinct {add : T -> T -> T};

Anoma/Proving/System.juvix

@@ -0,0 +1,12 @@
+module Anoma.Proving.System;
+
+import Stdlib.Prelude open using {Bool};
+import Anoma.Proving.Types open;
+import Anoma.Resource.Index as Resource open using {Instance; Witness};
+
+trait
+type ProvingSystem :=
+  mkProvingSystem {
+    prove : ProvingKey -> Resource.Instance -> Resource.Witness -> Proof;
+    verify : ProofRecord -> Bool
+  };

Anoma/Proving/Types.juvix

@@ -0,0 +1,12 @@
+module Anoma.Proving.Types;
+
+import Stdlib.Prelude open using {Pair};
+import Anoma.Resource.Index as Resource open using {Witness};
+
+axiom Proof : Type;
+
+axiom VerifyingKey : Type;
+
+axiom ProvingKey : Type;
+
+ProofRecord : Type := Pair VerifyingKey (Pair Proof Resource.Witness);

Anoma/Resource/Computable/Commitment.juvix

@@ -0,0 +1,20 @@
+module Anoma.Resource.Computable.Commitment;
+
+import Stdlib.Prelude open;
+import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
+import Anoma.Resource.Types open;
+
+axiom Commitment : Type;
+
+axiom commitment : (resource : Resource) -> Commitment;
+
+axiom compare : Commitment -> Commitment -> Ordering;
+
+instance
+Commitment-Ord : Ord Commitment :=
+  mkOrd@{
+    cmp := compare
+  };
+
+instance
+Commitment-Eq : Eq Commitment := fromOrdToEq;

Anoma/Resource/Computable/Delta.juvix

@@ -0,0 +1,15 @@
+module Anoma.Resource.Computable.Delta;
+
+import Anoma.Delta open;
+import Anoma.Resource.Types open;
+import Anoma.Resource.Computable.Kind as Computable open;
+
+module Internal;
+  axiom delta : (kind : Kind) -> (quantity : Quantity) -> Delta;
+end;
+
+delta (resource : Resource) : Delta :=
+  Internal.delta@{
+    kind := Computable.kind resource;
+    quantity := Resource.quantity resource
+  };

Anoma/Resource/Computable/Kind.juvix

@@ -0,0 +1,17 @@
+module Anoma.Resource.Computable.Kind;
+
+import Anoma.Resource.Types open;
+import Anoma.Resource.Logic open;
+import Anoma.Resource.Label open;
+
+axiom Kind : Type;
+
+module Internal;
+  axiom kind : (logicRef : LogicRef) -> (labelRef : LabelRef) -> Kind;
+end;
+
+kind (resource : Resource) : Kind :=
+  Internal.kind@{
+    logicRef := Resource.logicRef resource;
+    labelRef := Resource.labelRef resource
+  };

Anoma/Resource/Computable/Nullifier.juvix

@@ -0,0 +1,22 @@
+module Anoma.Resource.Computable.Nullifier;
+
+import Stdlib.Prelude open;
+import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
+import Anoma.Resource.Types open;
+
+axiom Nullifier : Type;
+
+axiom NullifierKey : Type;
+
+axiom nullifier : (resource : Resource) -> (nullifierKey : NullifierKey) -> Nullifier;
+
+axiom compare : Nullifier -> Nullifier -> Ordering;
+
+instance
+Nullifier-Ord : Ord Nullifier :=
+  mkOrd@{
+    cmp := compare
+  };
+
+instance
+Nullifier-Eq : Eq Nullifier := fromOrdToEq;

Anoma/Resource/Index.juvix

@@ -0,0 +1,6 @@
+module Anoma.Resource.Index;
+
+import Anoma.Resource.Computable.Commitment open using {Commitment; commitment} public;
+import Anoma.Resource.Computable.Nullifier open using {Nullifier; NullifierKey; nullifier} public;
+import Anoma.Resource.Logic open public;
+import Anoma.Resource.Computable.Delta open public;

Anoma/Resource/Label.juvix

@@ -0,0 +1,13 @@
+module Anoma.Resource.Label;
+
+import Anoma.Resource.Types open using {Ref; mkRef; LabelRef} public;
+
+axiom Label : Type;
+
+axiom labelRef : Label -> LabelRef;
+
+instance
+Label-Ref : Ref Label LabelRef :=
+  mkRef@{
+    ref (label : Label) : LabelRef := labelRef label
+  };

Anoma/Resource/Logic.juvix

@@ -0,0 +1,44 @@
+module Anoma.Resource.Logic;
+
+import Stdlib.Prelude open using {Bool};
+import Data.Set as Set open using {Set};
+
+import Anoma.Resource.Types open using {Resource; Ref; mkRef; LogicRef} public;
+import Anoma.Resource.Computable.Commitment open;
+import Anoma.Resource.Computable.Nullifier open;
+
+Logic : Type := Tag -> Instance -> Witness -> Bool;
+
+axiom logicRef : Logic -> LogicRef;
+
+instance
+Logic-Ref : Ref Logic LogicRef :=
+  mkRef@{
+    ref (logic : Logic) : LogicRef := logicRef logic
+  };
+
+--- The reference to the ;Resource; carrying the ;Logic; function.
+type Tag :=
+  | Created Commitment
+  | Consumed Nullifier;
+
+--- The public inputs to the ;Logic; function.
+type Instance :=
+  mkInstance {
+    commitments : Set Commitment;
+    nullifiers : Set Nullifier;
+    tag : Tag;
+    custom : CustomInstance
+  };
+
+axiom CustomInstance : Type;
+
+--- The private inputs to the ;Logic; function.
+type Witness :=
+  mkWitness {
+    created : Set Resource;
+    consumed : Set Resource;
+    custom : CustomWitness
+  };
+
+axiom CustomWitness : Type;

Anoma/Resource/Types.juvix

@@ -0,0 +1,33 @@
+module Anoma.Resource.Types;
+
+import Stdlib.Prelude open using {Bool} public;
+import Data.Set as Set open using {Set} public;
+
+axiom LogicRef : Type;
+
+axiom LabelRef : Type;
+
+axiom ValueRef : Type;
+
+axiom Quantity : Type;
+
+axiom NullifierKeyCommitment : Type;
+
+axiom Nonce : Type;
+
+axiom RandSeed : Type;
+
+type Resource :=
+  mkResource {
+    logicRef : LogicRef;
+    labelRef : LabelRef;
+    valueRef : ValueRef;
+    quantity : Quantity;
+    ephemerality : Bool;
+    nullifierKeyCommitment : NullifierKeyCommitment;
+    nonce : Nonce;
+    randSeed : RandSeed
+  };
+
+trait
+type Ref DataType RefType := mkRef {ref : DataType -> RefType};

Anoma/Resource/Value.juvix

@@ -0,0 +1,13 @@
+module Anoma.Resource.Value;
+
+import Anoma.Resource.Types open using {Ref; mkRef; ValueRef} public;
+
+axiom Value : Type;
+
+axiom valueRef : Value -> ValueRef;
+
+instance
+Value-Ref : Ref Value ValueRef :=
+  mkRef@{
+    ref (value : Value) : ValueRef := valueRef value
+  };

Anoma/State/CommitmentTree.juvix

@@ -0,0 +1,18 @@
+module Anoma.State.CommitmentTree;
+
+import Stdlib.Prelude open using {Maybe; Bool};
+import Anoma.Resource.Index as Resource;
+
+axiom Root : Type;
+
+axiom Path : Type;
+
+positive
+trait
+type CommitmentTree :=
+  mkCommitmentTree {
+    add : CommitmentTree -> Resource.Commitment -> Path;
+    path : CommitmentTree -> Resource.Commitment -> Maybe Path;
+    verify : Resource.Commitment -> Path -> Root -> Bool;
+    root : CommitmentTree -> Root
+  };

Anoma/State/Machine.juvix

@@ -0,0 +1,16 @@
+module Anoma.State.Machine;
+
+import Stdlib.Prelude open using {Bool};
+import Data.Set as Set open using {Set};
+
+import Anoma.Delta open;
+import Anoma.State.CommitmentTree as CommitmentTree open;
+import Anoma.Transaction.Index as Transaction open;
+
+trait
+type Machine :=
+  mkMachine {
+    create : Transaction.Constructor;
+    compose : Transaction -> Transaction -> Transaction;
+    verify : Transaction.Transaction -> Bool
+  };

Anoma/State/NullifierSet.juvix

@@ -0,0 +1,11 @@
+module Anoma.State.NullifierSet;
+
+import Stdlib.Prelude open using {Bool};
+import Anoma.Resource.Index as Resource;
+
+trait
+type NullifierSet :=
+  mkAccumulator {
+    add : Resource.Nullifier -> NullifierSet;
+    exists : Resource.Nullifier -> Bool
+  };

Anoma/Transaction/Action.juvix

@@ -0,0 +1,21 @@
+module Anoma.Transaction.Action;
+
+import Stdlib.Prelude open using {Pair};
+import Data.Set as Set open using {Set};
+
+import Anoma.Resource.Index as Resource;
+import Anoma.Proving.Types as Proving open;
+
+axiom AppDataKeyType : Type;
+
+axiom AppDataValueType : Type;
+
+AppDataMap : Type := Set (Pair AppDataKeyType AppDataValueType);
+
+type Action :=
+  mkAction {
+    commitments : Set Resource.Commitment;
+    nullifiers : Set Resource.Nullifier;
+    proofs : Set Proving.ProofRecord;
+    appData : AppDataMap
+  };