diff --git a/.github/workflows/clean-up.yaml b/.github/workflows/clean-up.yaml index 4ac6dcaa64b..0d2378b5205 100644 --- a/.github/workflows/clean-up.yaml +++ b/.github/workflows/clean-up.yaml @@ -20,7 +20,7 @@ jobs: cleanup: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v4.2.0 + - uses: actions/checkout@v4 with: ref: gh-pages clean: true diff --git a/.github/workflows/deploy.yml b/.github/workflows/deploy.yml index 7b897e7476f..dae650bc9ae 100644 --- a/.github/workflows/deploy.yml +++ b/.github/workflows/deploy.yml @@ -28,7 +28,7 @@ jobs: deploy: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v4.2.0 + - uses: actions/checkout@v4 with: submodules: true fetch-depth: 0 @@ -41,14 +41,14 @@ jobs: MSG: "The build is in progress. Please wait for the preview link." GH_FLAGS: pr -R anoma/nspec comment ${{ github.event.pull_request.number }} - name: Install the right Juvix for the Specs - uses: jaxxstorm/action-install-gh-release@v1.12.0 + uses: jaxxstorm/action-install-gh-release@v1 with: repo: anoma/juvix tag: ${{ env.JUVIX_VERSION }} 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 @@ -59,11 +59,11 @@ jobs: run: | juvix typecheck docs/everything.juvix.md - name: Install Python - uses: actions/setup-python@v5.2.0 + uses: actions/setup-python@v5 with: python-version: ${{ env.PYTHON_VERSION }} - name: Install Poetry - uses: abatilo/actions-poetry@v3.0.0 + uses: abatilo/actions-poetry@v3 with: poetry-version: ${{ env.POETRY_VERSION }} - name: Setup a local virtual environment (if no poetry.toml file) @@ -72,14 +72,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 @@ -109,7 +109,7 @@ jobs: PROCESS_JUVIX: true TIMELIMIT: 100 - if: success() - uses: JamesIves/github-pages-deploy-action@v4.6.4 + uses: JamesIves/github-pages-deploy-action@v4 with: folder: ${{ env.BRANCH_NAME }} target-folder: ${{ env.BRANCH_NAME }} @@ -117,7 +117,7 @@ jobs: clean: false git-config-name: Anoma Research git-config-email: arts@heliax.dev - - uses: JamesIves/github-pages-deploy-action@v4.6.4 + - uses: JamesIves/github-pages-deploy-action@v4 with: folder: ${{ env.BRANCH_NAME }} target-folder: ${{ env.BRANCH_NAME }} diff --git a/.github/workflows/pull-requests.yml b/.github/workflows/pull-requests.yml index 1372bcaee18..dece90627d3 100644 --- a/.github/workflows/pull-requests.yml +++ b/.github/workflows/pull-requests.yml @@ -4,8 +4,6 @@ - opened - synchronize - reopened - - edited - - ready_for_review env: CI: true GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} @@ -32,7 +30,7 @@ jobs: runs-on: ubuntu-latest steps: - name: Checkout repository - uses: actions/checkout@v4.2.0 + uses: actions/checkout@v4 with: fetch-depth: 0 ref: ${{ github.event.pull_request.head.ref }} @@ -57,7 +55,7 @@ jobs: runs-on: ubuntu-latest concurrency: ci-${{ github.ref }} steps: - - uses: actions/checkout@v4.2.0 + - uses: actions/checkout@v4 with: submodules: true fetch-depth: 0 @@ -71,14 +69,14 @@ jobs: MSG: "The build is in progress. Please wait for the preview link." GH_FLAGS: pr -R anoma/nspec comment ${{ github.event.pull_request.number }} - name: Install the right Juvix for the Specs - uses: jaxxstorm/action-install-gh-release@v1.12.0 + uses: jaxxstorm/action-install-gh-release@v1 with: repo: anoma/juvix tag: ${{ env.JUVIX_VERSION }} 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 @@ -93,11 +91,11 @@ jobs: run: | juvix typecheck docs/everything.juvix.md - name: Install Python - uses: actions/setup-python@v5.2.0 + uses: actions/setup-python@v5 with: python-version: ${{ env.PYTHON_VERSION }} - name: Install Poetry - uses: abatilo/actions-poetry@v3.0.0 + uses: abatilo/actions-poetry@v3 with: poetry-version: ${{ env.POETRY_VERSION }} - name: Setup a local virtual environment (if no poetry.toml file) @@ -106,14 +104,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 @@ -123,20 +121,6 @@ jobs: run: sudo apt-get install -y libcairo2-dev libfreetype6-dev libffi-dev libjpeg-dev libpng-dev libz-dev pngquant graphviz - name: Install Python dependencies run: poetry install - - name: Build MkDocs - id: mkdocs-basic - run: | - poetry run mkdocs build --clean --config-file mkdocs.yml --site-dir $SITE_DIR - env: - SITE_DIR: pr-${{ github.event.pull_request.number }} - SITE_URL: https://specs.anoma.net/pr-${{ github.event.pull_request.number }}/ - SITE_VERSION: (PR ${{ github.event.pull_request.number }}) - PROCESS_JUVIX: true - TIMELIMIT: 100 - - name: The build failed comment - if: failure() - run: | - gh pr -R anoma/nspec comment ${{ github.event.pull_request.number }} --edit-last --body "The build failed. Please check the logs." - name: get the last commit short hash id: commit run: echo "::set-output name=commit::$(git rev-parse --short HEAD)" @@ -165,7 +149,7 @@ jobs: continue-on-error: true - name: Deploy MkDocs with insiders theme if: success() - uses: JamesIves/github-pages-deploy-action@v4.6.4 + uses: JamesIves/github-pages-deploy-action@v4 with: repository-name: anoma/nspec branch: gh-pages @@ -194,3 +178,49 @@ jobs: run: | gh pr -R anoma/nspec comment ${{ github.event.pull_request.number }} --edit-last --body "The preview of this PR failed to build. Check the logs." continue-on-error: true + build-basic: # without insiders and juvix + runs-on: ubuntu-latest + concurrency: ci-basic-${{ github.ref }} + steps: + - uses: actions/checkout@v4 + with: + submodules: true + fetch-depth: 0 + - name: Install Python + uses: actions/setup-python@v5 + with: + python-version: ${{ env.PYTHON_VERSION }} + - name: Install Poetry + uses: abatilo/actions-poetry@v3 + with: + poetry-version: ${{ env.POETRY_VERSION }} + - name: Setup a local virtual environment (if no poetry.toml file) + run: | + poetry config virtualenvs.create true --local + 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 + with: + key: mkdocs-basic-material-${{ env.cache_id }} + path: .cache + restore-keys: | + mkdocs-basic-material- + - name: Install Linux dependencies + run: sudo apt-get install -y libcairo2-dev libfreetype6-dev libffi-dev libjpeg-dev libpng-dev libz-dev pngquant graphviz + - name: Install Python dependencies + run: poetry install + - name: Build MkDocs + id: mkdocs-basic + run: | + poetry run mkdocs build --clean --config-file mkdocs.yml --site-dir $SITE_DIR + env: + SITE_DIR: pr-${{ github.event.pull_request.number }} + SITE_URL: https://specs.anoma.net/pr-${{ github.event.pull_request.number }}/ + SITE_VERSION: (PR ${{ github.event.pull_request.number }}) + PROCESS_JUVIX: false + TIMELIMIT: 100 + - name: The build failed comment + if: failure() + run: | + gh pr -R anoma/nspec comment ${{ github.event.pull_request.number }} --edit-last --body "The build failed. Please check the logs." diff --git a/docs/arch/system/state/resource_machine/prelude.juvix.md b/docs/arch/system/state/resource_machine/prelude.juvix.md index a4654aec536..b27198cdc4d 100644 --- a/docs/arch/system/state/resource_machine/prelude.juvix.md +++ b/docs/arch/system/state/resource_machine/prelude.juvix.md @@ -67,6 +67,42 @@ syntax alias LabelHash := Digest; syntax alias LogicHash := Digest; ``` +#### `LogicRef` + +```juvix +syntax alias LogicRef := LogicHash; +``` + +#### `KindHash` + +```juvix +syntax alias KindHash := Digest; +``` + +#### `ExtraInput` + +```juvix +syntax alias ExtraInput := ByteString; +``` + +#### `NullifierRef` + +```juvix +syntax alias NullifierRef := Digest; +``` + +#### `RootRef` + +```juvix +syntax alias RootRef := Digest; +``` + +#### `CommitmentRef` + +```juvix +syntax alias CommitmentRef := Digest; +``` + #### `Quantity` There are two numeric types of unspecified character mentioned in the RM, which @@ -380,6 +416,16 @@ orderedSetFromList (mkOrderedSet Set.empty []); ``` +#### `orderedSetMap` + +```juvix +orderedSetMap + {A B} {{Ord A}} {{Ord B}} + (f : A -> B) + (s : OrderedSet A) : OrderedSet B := + orderedSetFromList (map f (orderedSetToList s)); +``` + #### `IOrderedSet` instance for `OrderedSet` ```juvix diff --git a/docs/arch/system/types/compliance_proving_system.juvix.md b/docs/arch/system/types/compliance_proving_system.juvix.md new file mode 100644 index 00000000000..8dd96d4a5df --- /dev/null +++ b/docs/arch/system/types/compliance_proving_system.juvix.md @@ -0,0 +1,195 @@ +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +tags: + - compliance-proving-system + - resource-machine + - type +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.types.compliance_proving_system; + import prelude open; + import arch.system.state.resource_machine.prelude open; + + import Stdlib.Data.Fixity open; + import Stdlib.Data.List as List open; + import Stdlib.Data.Pair as Pair open; + import Stdlib.Data.Unit as Unit open; + import Stdlib.Data.Bool open; + import Stdlib.Data.String open; + import Stdlib.Data.Nat open; + import Stdlib.Data.Maybe open; + + import arch.system.types.proving_system open; + import arch.system.types.resource open; + import arch.system.types.nullifier open; + import arch.system.types.nullifierkey open; + import arch.system.types.commitment open; + import arch.system.types.commitmenttree open; + ``` + +# Compliance Proving System + +A **compliance proving system** is a specialized proving system used to verify +**compliance proofs**. These proofs ensure that resources are consumed and +created in a manner consistent with the resource machine’s constraints: +Merkle path validity, logic integrity, and delta correctness. + +Below we define the data types for the compliance instance and witness, as +described in the compliance proof documentation, and then provide a +`ComplianceProvingSystem` trait specializing the generic `ProvingSystem`. + +## Data Definitions + +### Consumed Resource Witness + +The doc (compliance_proof.juvix.md) states that each consumed resource has five data points in the witness: +1. `resource` object +2. `nullifierKey` +3. `CTreePath` +4. `commitment` +5. opening of `logicRefHash` (stored as `ByteString` below) + +```juvix +type ConsumedResourceWitness A : Type := + mkConsumedResourceWitness + Resource + NullifierKey + CTreePath + (Commitment A) + ByteString; +``` + +### Created Resource Witness + +Each created resource has two data points: +1. `resource` object +2. opening of `logicRefHash` (again `ByteString`) + +```juvix +type CreatedResourceWitness : Type := + mkCreatedResourceWitness + Resource + ByteString; +``` + +### ComplianceWitness + +The doc (compliance_proof.juvix.md) merges all consumed resource witness data and created resource witness +data. We store them as lists in a single data structure: + +```juvix +type ComplianceWitness A : Type := + mkComplianceWitness + (List (ConsumedResourceWitness A)) + (List CreatedResourceWitness); +``` + +### ComplianceInstance + +The doc (compliance_proof.juvix.md) states that compliance instance data has: +1. `consumed : OrderedSet (NullifierRef, RootRef, LogicRef)` +2. `created : OrderedSet (CommitmentRef, LogicRef)` +3. `unitDelta: DeltaHash` + +```juvix +type ComplianceInstance : Type := + mkComplianceInstance { + consumed : (OrderedSet (Pair NullifierRef (Pair RootRef LogicRef))); + created : (OrderedSet (Pair CommitmentRef LogicRef)); + unitDelta : DeltaHash; + } +``` + +There also has to exist some method to dereference resources. + +```juvix +axiom dereferenceNullifier : LogicRef -> Nullifier; +axiom dereferenceCommitment {A} : CommitmentRef -> Commitment A; + +axiom dereferenceConsumed : (Pair NullifierRef (Pair RootRef LogicRef)) -> Resource; +axiom dereferenceCreated : (Pair CommitmentRef LogicRef) -> Resource; +``` + +## Local Constraint Checks + +NOTE: These are unfinished and need to be redone. IGNORE THIS SECTION. + +The doc’s (compliance_proof.juvix.md) constraints for each consumed resource: + +1. `resourceNullifier(r, nk) == nfRef` +2. `resourceCommitment(r) == cm` +3. `resourceLogicRefHash(r) == logicRef` +4. `merkleVerify(cm, cmPath, rootRef) == true` + +Analogously for created resources: + +1. `resourceCommitment(r) == cm` +2. `resourceLogicRefHash(r) == logRef` + +We define checks for these constraints: + +NOTE: There are a bunch of functions here that aren't currently defined. + +``` +checkConsumedResource + (consWitness : ConsumedResourceWitness) + (consRef : (Pair NullifierRef (Pair RootRef LogicRef))) + : Bool + := case consWitness of { + | mkConsumedResourceWitness r nk path cm logOp := + case consRef of { + | (nfRefAndRootRef, logRf) := + case nfRefAndRootRef of { + | (nfRef, rootRf) := + let + passNF : Bool := nfRef == resourceNullifier r nk; + passCommit : Bool := resourceCommitment r == cm; + passLog : Bool := resourceLogicRefHash r == logRf; + passMerkle : Bool := merkleVerify cm path rootRf; + in + passNF && passCommit && passLog && passMerkle + } + } + }; + +checkCreatedResource + (creatWitness : CreatedResourceWitness) + (creatRef : (Pair CommitmentRef LogicRef)) + : Bool + := case creatWitness of { + | mkCreatedResourceWitness r logOp := + case creatRef of { + | (cmRef, logRf) := + let passC : Bool := commitmentHash (resourceCommitment r) == cmRef; + passLog : Bool := resourceLogicRefHash r == logRf; + in passC && passLog + } + }; +``` + +## Trait: `ComplianceProvingSystem` + +We embed a reference to a ProvingSystem specialized +to `(ComplianceInstance, ComplianceWitness)`. + +```juvix +trait +type ComplianceProvingSystem A + (Proof : Type) + (VerifyingKey : Type) + (ProvingKey : Type) +:= mkComplianceProvingSystem@{ + baseSystem : ProvingSystem + Proof + VerifyingKey + ProvingKey + ComplianceInstance + (ComplianceWitness A); +}; +``` diff --git a/docs/arch/system/types/compliance_unit.juvix.md b/docs/arch/system/types/compliance_unit.juvix.md new file mode 100644 index 00000000000..7a5119c1b09 --- /dev/null +++ b/docs/arch/system/types/compliance_unit.juvix.md @@ -0,0 +1,185 @@ +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +tags: + - compliance-unit + - resource-machine + - type +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.types.compliance_unit; + import prelude open; + import arch.system.state.resource_machine.prelude open; + + import Stdlib.Data.Fixity open; + import Stdlib.Data.List as List open; + import Stdlib.Data.Pair as Pair open; + import Stdlib.Data.Unit as Unit open; + import Stdlib.Data.Bool open; + import Stdlib.Data.String open; + import Stdlib.Data.Nat open; + import Stdlib.Data.Maybe open; + + import arch.system.types.delta open; + import arch.system.types.resource open; + import arch.system.types.nullifier open; + import arch.system.types.commitment open; + import arch.system.types.nullifierkey open; + import arch.system.types.proving_system open; + import arch.system.types.compliance_proving_system open; + ``` + +# Compliance Unit + +A **compliance unit** partitions consumed and created resources for a single +compliance proof. It references a *compliance instance* to expand its actual +data, as well as the verifying key, the cryptographic proof, and so on. This +file defines: + +- The `ComplianceUnit` type, +- A `HasDelta` instance that re-derives the unit's delta by summing resource deltas, +- Functions `consumed`, `created`, `createComplianceUnit` and `verifyComplianceUnit` (fromr the doc's interface). + +## The `ComplianceUnit` Type + +The doc (compliance_unit.juvix.md) states that a compliance unit has: + +1. A reference to the **compliance proving system** used, +2. The verifying key, +3. A reference to an instance, +4. A `delta : DeltaHash`, +5. A `proof : Proof`. + +```juvix +axiom ReferenceInstance : Type; +axiom dereference : ReferenceInstance -> ComplianceInstance; + +type ComplianceUnit A + (Proof : Type) + (VerifyingKey : Type) + (ProvingKey : Type) +:= mkComplianceUnit { + system : ComplianceProvingSystem A Proof VerifyingKey ProvingKey; + vk : VerifyingKey; + refInst : ReferenceInstance; + delta : DeltaHash; + proof : Proof +}; +``` + +## HasDelta(ComplianceUnit) + +The doc (compliance_unit.juvix.md) states we can re-derive the compliance unit's delta from the consumed +and created resource deltas: \(\sum(\text{consumed}) - \sum(\text{created})\). +We assert an additive group over `DeltaHash` and define a fold to hash a set of resources. +We define: + +```juvix +syntax alias DeltaHashGroup := DeltaHash; + +axiom groupZero : DeltaHashGroup; +axiom groupAdd : DeltaHashGroup -> DeltaHashGroup -> DeltaHashGroup; +axiom groupSub : DeltaHashGroup -> DeltaHashGroup -> DeltaHashGroup; + +sumOfResourceDeltas + (rList : List Resource) + : DeltaHashGroup + := + listFoldl + (\{acc r := groupAdd acc (HasDelta.delta r)}) + groupZero + rList; + +instance +hasDeltaComplianceUnit {A} + {Proof} + {VerifyingKey} + {ProvingKey} + : HasDelta (ComplianceUnit A Proof VerifyingKey ProvingKey) + := mkHasDelta@{ + delta := \{u := + case u of { + | mkComplianceUnit sys vk rInst d pf := + let cInst := dereference rInst; + consumedVal := sumOfResourceDeltas (map dereferenceConsumed (orderedSetToList (ComplianceInstance.consumed cInst))); + createdVal := sumOfResourceDeltas (map dereferenceCreated (orderedSetToList (ComplianceInstance.created cInst))); + in groupSub consumedVal createdVal + } + } + }; +``` + +## `createComplianceUnit` and `verifyComplianceUnit` + +NOTE: These are unfinished and need to be redone. IGNORE THIS SECTION. + +The doc (compliance_unit.juvix.md) states: + +1. `create(PS.ProvingKey, PS.Instance, PS.Proof) -> ComplianceUnit` +2. `verify(ComplianceUnit) -> Bool` + +We define them top-level: + +``` +createComplianceUnit + (pk : ProvingKey) + (cInst : ComplianceInstance) + (pr : Proof) + : ComplianceUnit Proof VerifyingKey ProvingKey + := + -- doc (compliance_unit.juvix.md) says we might call system.prove(...) etc. + -- I don't really know what all to do here + mkComplianceUnit + { system = ??? -- should be present in env already + ; vk = ??? -- unclear where this comes from + ; refInst = cInst + ; delta = unitDelta cInst -- doc's "unitDelta" + ; proof = pr + }; +``` + +```juvix +verifyComplianceUnit + (A Proof VerifyingKey ProvingKey : Type) + (u : ComplianceUnit A Proof VerifyingKey ProvingKey) + : Bool + := + case u of { + | mkComplianceUnit sys verK rInst delt pr := + -- doc: returns sys.verify(verK, cInst, pr) + ProvingSystem.verify {{ComplianceProvingSystem.baseSystem {{sys}}}} verK (dereference rInst) pr + }; +``` + +!!! note + This code is partial. In a real system, `createComplianceUnit` might produce + the proof itself via `sys.prove(pk, cInst, someWitness)`, or store references + differently. The doc's (compliance_unit.juvix.md) detail aren't really clear + +## `consumed` and `created` Functions + +The doc (compliance_unit.juvix.md) says: + +- `consumed(ComplianceUnit) -> Set Nullifier` +- `created(ComplianceUnit) -> Set Commitment` + +```juvix +consumed (A Proof VerifyingKey ProvingKey : Type) + (u : ComplianceUnit A Proof VerifyingKey ProvingKey) + : OrderedSet Nullifier + := case u of { + | mkComplianceUnit _ _ rInst _ _ := orderedSetMap \{(k, _) := dereferenceNullifier k} (ComplianceInstance.consumed (dereference rInst)) + }; + +created (A Proof VerifyingKey ProvingKey : Type) {{Ord A}} + (u : ComplianceUnit A Proof VerifyingKey ProvingKey) + : OrderedSet (Commitment A) + := case u of { + | mkComplianceUnit _ _ rInst _ _ := orderedSetMap \{(k, _) := dereferenceCommitment k} (ComplianceInstance.created (dereference rInst)) + }; +``` diff --git a/docs/arch/system/types/delta.juvix.md b/docs/arch/system/types/delta.juvix.md new file mode 100644 index 00000000000..8aac3974282 --- /dev/null +++ b/docs/arch/system/types/delta.juvix.md @@ -0,0 +1,38 @@ +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +tags: + - delta + - resource-machine + - type +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.types.delta; + import prelude open; + import arch.system.state.resource_machine.prelude open; + ``` + +# Resource Delta + +A **delta** is a cryptographic commitment to the resource’s quantity (and +possibly other data). The Resource Machine can use this delta to track and +verify resource balances across different structures such as compliance units, +actions, or transactions. + + +## HasDelta Trait + +We define a *HasDelta* trait for data types that can compute a `DeltaHash`: + +```juvix +trait +type HasDelta (A : Type) := + mkHasDelta@{ + delta : A -> DeltaHash + }; +``` diff --git a/docs/arch/system/types/kind.juvix.md b/docs/arch/system/types/kind.juvix.md new file mode 100644 index 00000000000..b0c81f828f6 --- /dev/null +++ b/docs/arch/system/types/kind.juvix.md @@ -0,0 +1,31 @@ +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +tags: + - kind + - resource-machine + - type +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.types.kind; + import prelude open; + import arch.system.state.resource_machine.prelude open; + ``` + +# Kind + +A resource’s *kind* distinguishes its fungibility domain. A kind is produced as the digest of two +digests from the resouce; it's label and its logic. + +## Computation + +We assume an axiomatic function to combine a label and logic hash into a delta‐value. + +```juvix +axiom kindHash : LabelHash -> LogicHash -> KindHash; +``` diff --git a/docs/arch/system/types/proving_system.juvix.md b/docs/arch/system/types/proving_system.juvix.md new file mode 100644 index 00000000000..7bdb6b63a35 --- /dev/null +++ b/docs/arch/system/types/proving_system.juvix.md @@ -0,0 +1,66 @@ +--- +icon: material/file-document-outline +search: + exclude: false + boost: 2 +tags: + - proving-system + - resource-machine + - type +--- + +??? quote "Juvix imports" + + ```juvix + module arch.system.types.proving_system; + import prelude open; + import arch.system.state.resource_machine.prelude open; + ``` + +# Proving System + +A **proving system** is defined by five type parameters: `Proof`, `VerifyingKey`, +`ProvingKey`, `Instance`, and `Witness`. It provides two core functions: + +1. `prove(pk, instance, witness) -> Proof` +2. `verify(vk, instance, proof) -> Bool` + +These functions are used to produce and verify proofs that some statement +involving the instance and witness is correct, under the assumptions of +completeness and soundness. + +## Trait Definition + +Below is the Juvix trait `ProvingSystem`, parameterized by these five types: + +```juvix +trait +type ProvingSystem + (Proof : Type) + (VerifyingKey : Type) + (ProvingKey : Type) + (Instance : Type) + (Witness : Type) +:= mkProvingSystem@{ + prove : ProvingKey -> Instance -> Witness -> Proof; + verify : VerifyingKey -> Instance -> Proof -> Bool; +}; +``` + +!!! note + - **Completeness** means that if the statement is true, a proof can be + generated that passes verification. + - **Soundness** means that if the statement is false, no valid proof can be + created (or equivalently, any purported proof will fail verification). + +## Usage + +The trait can be instantiated to model different proving schemes: + +- **Trivial scheme**: replicate the computation in `verify`. +- **Trusted delegation**: rely on a trusted party’s signature. +- **Succinct Proof of Knowledge**: e.g., SNARKs, STARKs, possibly zero-knowledge. + +The particular instantiation is determined by how `ProvingKey`, `VerifyingKey`, +`Instance`, `Witness`, and `Proof` are defined, and by the implementations of +`prove` and `verify`. \ No newline at end of file diff --git a/docs/arch/system/types/resource.juvix.md b/docs/arch/system/types/resource.juvix.md index 8721381a776..827e4c0d0c3 100644 --- a/docs/arch/system/types/resource.juvix.md +++ b/docs/arch/system/types/resource.juvix.md @@ -11,6 +11,8 @@ search: module arch.system.types.resource; import prelude open; import arch.system.types.nullifierkey open; + import arch.system.types.delta open; + import arch.system.types.kind open; import arch.system.state.resource_machine.prelude open; ``` @@ -95,3 +97,32 @@ Resources have the following key properties: - Fungibility: Resources sharing the same label are considered fungible - Nullification: Resources can be consumed only once using their [[Nullifier|nullifier key]] - Ephemerality: Ephemeral resources bypass existence checks when consumed + +# Kind + +The function `kind` computes the kind of a resource by extracting its label and logic fields. + +```juvix +kind (r : Resource) : KindHash := + kindHash (Resource.labelRef r) (Resource.logicRef r); +``` + +## Delta for Resource + +Below is the *HasDelta* instance for a `Resource`. It calls `deltaHash` with the +resource’s `kind`, `quantity`, and some `extraInput`. + +```juvix +axiom extraInput : ExtraInput; + +axiom deltaHash : + KindHash -> Nat -> ExtraInput -> DeltaHash; + +instance +hasDeltaResourceI : HasDelta Resource := + mkHasDelta@{ + delta := \{r := + deltaHash (kind r) (Resource.quantity r) extraInput + } + }; +```