diff --git a/.github/workflows/pull-requests.yml b/.github/workflows/pull-requests.yml index 1372bcaee18..b097494df9b 100644 --- a/.github/workflows/pull-requests.yml +++ b/.github/workflows/pull-requests.yml @@ -78,7 +78,7 @@ jobs: cache: enable rename-to: juvix chmod: 0755 - - uses: actions/cache@v4.0.2 + - uses: actions/cache@v4 with: key: juvix-cache-${{ hashFiles('**/*.juvix.md') }}-${{ hashFiles('**/*.juvix') }} path: .juvix-build @@ -106,14 +106,14 @@ jobs: poetry config virtualenvs.in-project true --local - run: echo "cache_id=$(date --utc '+%V')-${{ hashFiles( '**/poetry.lock' )}}-${{ hashFiles( '**/*.py' )}}" >> $GITHUB_ENV - name: Cache .cache - uses: actions/cache@v4.0.2 + uses: actions/cache@v4 with: key: mkdocs-material-${{ env.cache_id }} path: .cache restore-keys: | mkdocs-material- - name: Cache .cache-juvix-mkdocs - uses: actions/cache@v4.0.2 + uses: actions/cache@v4 with: key: .cache-juvix-mkdocs-${{ env.cache_id }} path: .cache-juvix-mkdocs diff --git a/VERSION b/VERSION index 7a5e833ee3f..174a3d52651 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -v0.1.4 \ No newline at end of file +v0.3 \ No newline at end of file diff --git a/docs/arch/system/state/resource_machine_03/dag.puml b/docs/arch/system/state/resource_machine_03/dag.puml new file mode 100644 index 00000000000..f8210b44f6c --- /dev/null +++ b/docs/arch/system/state/resource_machine_03/dag.puml @@ -0,0 +1,3 @@ +@startuml +Bob -> Alice : [[https://research.anoma.net Forums]] +@enduml diff --git a/docs/arch/system/state/resource_machine_03/dag.txt b/docs/arch/system/state/resource_machine_03/dag.txt new file mode 100644 index 00000000000..8938840c424 --- /dev/null +++ b/docs/arch/system/state/resource_machine_03/dag.txt @@ -0,0 +1,275 @@ +classDiagram + %% Core Interfaces + class IProvingSystem~VerifyingKey,ProvingKey,Instance,Witness,Proof~ { + +prove(ProvingKey, Instance, Witness) Proof + +verify(VerifyingKey, Instance, Proof) Bool + } + %%IProvingSystem done. + %%ProvingSystem done. + class IDeltaProvingSystem~VerifyingKey,ProvingKey,Instance,Witness,Proof~ { + +aggregate(Proof, Proof) Proof + } + class ISet~T~ { + +new() Set + +new(List) Set + +size(Set) Nat + +insert(Set, T) Set + +union(Set, Set) Set + +intersection(Set, Set) Set + +difference(Set, Set) Set + +disjointUnion(Set, Set) Set + +contains(Set, T) Bool + } + class IOrderedSet~T~ + class FixedSize~T,Arg~ { + +bit_size: Int + +new(Arg) T + +equal(T, T) Bool + } + %%Arithmetic done. + class Arithmetic~T,Arg~ { + +add(T, T) T + +sub(T, T) T + } + class Hash~T,Arg~ + class CommitmentAccumulator~Witness,CommitmentIdentifier,AccumulatedValue~ { + +add(Accumulator, CommitmentIdentifier) Witness + +witness(Accumulator, CommitmentIdentifier) Maybe Witness + +verify(CommitmentIdentifier, Witness, AccumulatedValue) Bool + +value(Accumulator) AccumulatedValue + } + class NullifierSet + + %% Core Data Structures + %%Resource done. + class Resource { + +logicRef: LogicHash + +labelRef: LabelHash + +valueRef: ValueHash + +quantity: Quantity + +isEphemeral: Bool + +nonce: Nonce + +nullifierKeyCommitment: NullifierKeyCommitment + +randSeed: RandSeed + +commitment() Commitment + +nullifier(NullifierKey) Nullifier + +kind() Kind + +delta() DeltaHash + +tag(consumed: Bool) Tag + } + class Action { + +created: List Commitment + +consumed: List Nullifier + +resourceLogicProofs: Map Tag (LogicRefHash, PS.Proof) + +complianceUnits: Set ComplianceUnit + +applicationData: Map Tag (BitString, DeletionCriterion) + +verify() Bool + +delta() DeltaHash + } + class ComplianceUnit { + +proof: PS.Proof + +refInstance: ReferencedInstance + +vk: PS.VerifyingKey + +delta() DeltaHash + +verify() Bool + } + class Transaction { + +CMTreeRoots: Set CMtree.Value + +actions: Set Action + +deltaProof: DeltaProvingSystem.Proof + +create(Set CMtree.Value, Set Actions) Transaction + +compose(Transaction, Transaction) Transaction + +verify() Bool + +delta() DeltaHash + } + %%Transaction done. + + %% Implementation Classes + class ResourceLogicProvingSystem + class ComplianceProvingSystem + class DeltaProvingSystem + class OrderedSet + class CMTree + class NFSet + class DeltaHash + class TransactionFunction { + +eval() Transaction + } + class TransactionFunctionVM { + +eval(TransactionFunction, GasLimit) Transaction + } + class TransactionWithPayment { + +stateTransitionFunction: TransactionFunction + +paymentTransaction: Transaction + +gasLimit: Arithmetic + } + + %% Fixed Size Types + class Nonce + class RandSeed + class NullifierKeyCommitment + class NullifierKey + class Quantity + class Balance + class LogicHash + class LabelHash + class ValueHash + class Commitment + class Nullifier + class LogicRefHash + + %% Proof Related Types + class ResourceLogicProofInstance { + +tag: Tag + +isConsumed: Bool + +consumed: List Nullifier + +created: List Commitment + +applicationData: BitString + } + class ResourceLogicProofWitness { + +consumed: OrderedSet (Resource, NullifierKey) + +created: OrderedSet Resource + +applicationInputs: Any + } + class ComplianceProofInstance { + +consumed: List (NullifierRef, RootRef, LogicRefHash) + +created: List (CommitmentRef, LogicRefHash) + +unitDelta: DeltaHash + } + class ComplianceProofWitness { + +consumed: OrderedSet Resource + +consumed_nullifierKey: OrderedSet NullifierKey + +consumed_cmtreePath: OrderedSet CMtreePath + +consumed_commitment: OrderedSet Commitment + +consumed_logicRefHash: OrderedSet LogicRefHash + +created: OrderedSet Resource + +created_logicRefHash: OrderedSet LogicRefHash + } + class DeltaProofInstance { + +delta: DeltaHash + +expectedBalance: Balance + } + class DeltaProofWitness { + +resourceDeltaPreimages: List Resource + } + + %% Inheritance/Implementation + IProvingSystem --|> IDeltaProvingSystem + IProvingSystem --|> ResourceLogicProvingSystem + IProvingSystem --|> ComplianceProvingSystem + IDeltaProvingSystem --|> DeltaProvingSystem + ISet --|> IOrderedSet + IOrderedSet --|> OrderedSet + CommitmentAccumulator --|> CMTree + Timestamp --> CMTree + NFSet --|> NullifierSet + FixedSize --|> Hash + FixedSize --|> Arithmetic + Hash --|> DeltaHash + Arithmetic --|> DeltaHash + + LogicHash --> Resource + LabelHash --> Resource + ValueHash --> Resource + Quantity --> Resource + Nonce --> Resource + NullifierKeyCommitment --> Resource + RandSeed --> Resource + Commitment --> Resource + Nullifier --> Resource + class Kind + Kind --> Resource + DeltaHash --> Resource + Tag --> Resource + Kind --> Resource + + Resource --> ComplianceProofWitness + Resource --> NullifierSet + Resource --> DeltaProofWitness + + %% Action Componenents + Commitment --> Action + Nullifier --> Action + Tag --> Action + IProvingSystem --> Action + LogicRefHash --> Action + DeletionCriterion --> Action + ComplianceUnit --> Action + + %% Action interface reqs + DeltaHash --> Action + NullifierKey --> Action + Resource --> Action + + IProvingSystem --> ComplianceUnit + %%ReferencedInstance --> ComplianceUnit + Commitment --> ComplianceUnit + Nullifier --> ComplianceUnit + DeltaHash --> ComplianceUnit + + Action --> Transaction + CMTree --> Transaction + DeltaProvingSystem --> Transaction + DeltaHash --> Transaction + + Transaction --> TransactionFunction + TransactionFunction --> TransactionWithPayment + Transaction --> TransactionWithPayment + Arithmetic --> TransactionWithPayment + TransactionFunction --> TransactionFunctionVM + + OrderedSet --> ComplianceProofWitness + + Nullifier --> ComplianceProofInstance + CMTree --> ComplianceProofInstance + LogicRefHash --> ComplianceProofInstance + Commitment --> ComplianceProofInstance + + CMTree --> ComplianceProofWitness + NullifierKey --> ComplianceProofWitness + Commitment --> ComplianceProofWitness + LogicRefHash --> ComplianceProofWitness + + Predicate --> DeletionCriterion + + CMTree --> Transaction + NullifierSet --> Transaction + Action --> Transaction + DeltaHash --> Transaction + + %% Fixed Size Type Implementation Dependencies + Hash --> LogicHash + Hash --> LabelHash + Hash --> ValueHash + Hash --> Commitment + Hash --> Nullifier + Hash --> Kind + Hash --> LogicRefHash + Hash --> CMTree + + Arithmetic --> Quantity + Arithmetic --> Balance + + FixedSize --> Nonce + FixedSize --> RandSeed + FixedSize --> NullifierKeyCommitment + FixedSize --> NullifierKey + + Balance --> DeltaProofInstance + DeltaHash --> DeltaProofInstance + NullifierKey --> Nullifier + + %% Input relationships (required for ResourceLogicProofInstance) + Tag --> ResourceLogicProofInstance + Nullifier --> ResourceLogicProofInstance + Commitment --> ResourceLogicProofInstance + Action --> ResourceLogicProofInstance + Resource --> ResourceLogicProofInstance + + %% Output relationships (where ResourceLogicProofInstance is used) + ResourceLogicProofInstance --> ResourceLogicProvingSystem + + %% Input relationships (required for ResourceLogicProofWitness) + OrderedSet --> ResourceLogicProofWitness + NullifierKey --> ResourceLogicProofWitness + Resource --> ResourceLogicProofWitness diff --git a/docs/arch/system/state/resource_machine_03/index.juvix.md b/docs/arch/system/state/resource_machine_03/index.juvix.md new file mode 100644 index 00000000000..3222b824d7a --- /dev/null +++ b/docs/arch/system/state/resource_machine_03/index.juvix.md @@ -0,0 +1,58 @@ +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +tags: + - resource-machine + - protocol + - commitment + - nullifier + - accumulator + - resource logic +--- + +```juvix +module arch.system.state.resource_machine_03.index; +``` + +# Introduction + +The resource machine provides the default interfaces +that controllers can use to perform state changes. + +```kroki-plantuml +@from_file:./arch/system/state/resource_machine_03/rm-overview-diagram.puml +``` + + diff --git a/docs/arch/system/state/resource_machine_03/rm-mindmap.puml b/docs/arch/system/state/resource_machine_03/rm-mindmap.puml new file mode 100644 index 00000000000..5bbdeb7ac36 --- /dev/null +++ b/docs/arch/system/state/resource_machine_03/rm-mindmap.puml @@ -0,0 +1,35 @@ +@startmindmap + ++ Proving System\n- make proofs\n- check proofs + +++ for resource logic +' produce proofs from ... +++ for compliance +' produce proofs from ... +++ for resource deltas +' produce proofs from ... + +'inputs and constraints +-- Architecture-level (aka RM-level) +-- Instantiation-level (aka //instantiation//-specific) +-- Application-level (aka //custom// ≔ application specific) + + + +'+ **myThoughts** +'++ Thought 1 +''tag::details[] +'+++_ Thought 1.1 +'+++_ Thought 1.2 +''end::details[] +'++ Thought 2 +'++ Thought 3 +' +''tag::left[] +'-- Thought A +'-- Thought B +'-- Thought C +''end::left[] +' + +@endmindmap diff --git a/docs/arch/system/state/resource_machine_03/rm-overview-diagram.puml b/docs/arch/system/state/resource_machine_03/rm-overview-diagram.puml new file mode 100644 index 00000000000..9173cdb0343 --- /dev/null +++ b/docs/arch/system/state/resource_machine_03/rm-overview-diagram.puml @@ -0,0 +1,106 @@ +@startuml +' This is an overview of interfaces and classes that are relevant to the resource machine +title +Overview of interfaces and classes that are relevant to the resource machine +end title + +' The proving system interface +interface "ProvingSystem" as PSI { + ' create a proof + +prove(ProvingKey, Instance, Witness): Proof + ' check whether a proof is correct + +verify(VerifyingKey, Instance, Proof): Bool +} +note right +- ""prove"" creates a proof +- ""verify"" checks whether a proof is correct +[[https://specs.anoma.net/v0.1.4/arch/system/state/resource_machine/primitive_interfaces/proving_system/index.html#proving-system-hierarchy → Proving System Hierarchy]] +end note +' note left of PSI +' test +' end note + +note left of PSI + Proving systems are subject to conditions: + - completness and soundness + - proofs attest statements (an implicit parameter) + [[https://specs.anoma.net/latest/arch/system/state/resource_machine/primitive_interfaces/proving_system/proving_system_types.html#proving-system-definition → Proving System Definition]] +end note + +' This is the interface of a `Arithmetic` +' TODO: do we want a group structure on T +interface "Arithmetic" as Arithmetic { + +add(T, T): T + +sub(T, T): T + ' do we want a zero TODO +} +note right +[[https://specs.anoma.net/v0.1.4/arch/system/state/resource_machine/primitive_interfaces/fixed_size_type/arithmetic.html Arithmetic]] +end note + +'note below +' This is actually an additive group. +'end note + +' This is the interface of a `resource` +interface Resource { + ' logic reference, a logic hash + +logicRef: LogicHash + ' logic reference, a label hash + +labelRef: LabelHash + ' value reference, a value hash + +valueRef: ValueHash + ' quantity of Quantity type + +quantity: Quantity + ' whether or not the resource is ephemeral + +isEphemeral: Bool + ' nonce, a number used once + +nonce: Nonce + ' the nullifier key commitment + +nullifierKeyCommitment: NullifierKeyCommitment + ' a seed for pseudo-random number generation + +randSeed: RandSeed + ' computing a commitment to the resource + +commitment(): Commitment + ' computing the nullifier for this resource (requires the NK) + +nullifier(NullifierKey): Nullifier + ' computing the kind + +kind(): Kind + ' computing the delta + +delta(): DeltaHash +} +note right of Resource + fields + [[https://specs.anoma.net/v0.1.4/arch/system/state/resource_machine/data_structures/resource/index.html#resource → Resource]] + + === + + methods + [[https://specs.anoma.net/v0.1.4/arch/system/state/resource_machine/primitive_interfaces/fixed_size_type/hash.html#hash-interface-diagram → computable components]] +end note +note bottom of Resource +see also [[https://specs.anoma.net/v0.1.4/arch/system/state/resource_machine/data_structures/resource/computable_components/introduction.html?h=resource+tag#tag Tag]] of a resource, which is not part of the class +end note + +Arithmetic <|-[dashed]- Resource: := +note bottom on link #red +todo ??? +end note + + +class "Transaction" as Transaction { + ' these are not any more neede + ' +CMTreeRoots: Set CMtree.Value + +actions: Set Action + +deltaProof: DeltaProvingSystem.Proof + +vk: DeltaProvingSystem.Proof + /' TODO: sort the interface out + ' +create(Set CMtree.Value, Set Actions): Transaction + ' +compose(Transaction, Transaction): Transaction + ' +verify(): Bool + ' +delta(): DeltaHash + '/ +} +'--------------------------------------------------------------------------------' +footer "[[https://tinyurl.com/anthonydag evolved from the Anthony DAG]]" +@enduml diff --git a/docs/arch/system/state/resource_machine_03/transaction-mindmap.puml b/docs/arch/system/state/resource_machine_03/transaction-mindmap.puml new file mode 100644 index 00000000000..feec7b31e55 --- /dev/null +++ b/docs/arch/system/state/resource_machine_03/transaction-mindmap.puml @@ -0,0 +1,27 @@ +@startmindmap + +*[#orange] **Transaction** +++ computed by (interpreting) **a** [[https://specs.anoma.net/v0.1.4/arch/system/state/resource_machine/data_structures/transaction/transaction_function.html#transaction-function transaction function]] ++++_ needs to be run by the executor ++++_ transaction function calculation on the [[https://specs.anoma.net/v0.1.4/arch/system/state/resource_machine/primitive_interfaces/transaction_function_vm.html transaction function ᴠᴍ]] ++++_ produces ""transaction"" as a result +++ some kind of //"code"// ++++[#white] **TODO** specifically/examples? + +-- verification\n(via proving systems) +---_ compute ""verify"" operation +---_ check gas +---_ [[https://specs.anoma.net/v0.1.4/arch/system/state/resource_machine/primitive_interfaces/transaction_function_vm.html → Transaction function ᴠᴍ]] +-- //"execution"//\n +--- perform reads an writes +---- transaction function computation +---- transaction //"execution"// +---[#white] **TODO** other side effects ??? + + +/' if we had a "parallel" mindmap //here// + ' *[#green] c + ' ++ b + ' -- a + '/ +@endmindmap diff --git a/mkdocs.yml b/mkdocs.yml index ae1d6d6a8e1..a94ec0b983c 100644 --- a/mkdocs.yml +++ b/mkdocs.yml @@ -179,6 +179,8 @@ nav: - Identity Architecture: - Identity Architecture Types: ./arch/system/identity/identity.juvix.md - State Architecture: + - Resource Machine v0.3: + - ./arch/system/state/resource_machine_03/index.juvix.md - Resource Machine: - ./arch/system/state/resource_machine/index.juvix.md - Primitive interfaces: