Add type files for proving system, compliance proving system, delta, and kind. #344

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Open

AHartNtkn wants to merge 15 commits into topic-transaction-function from anthony/types_1

+657 −35

Contributor

AHartNtkn commented Feb 21, 2025

Adds four files to the types folder, corresponding to proving system, compliance proving system, delta, and kind from the RM specs. I'll be honest, I don't know how well I succeeded, or how well it would even be possible to succeed. I did my best; hopefully it's enough to move on.

PR Todo List

Type of Change: Mark the relevant option(s) with 'x':
- System Architecture Change
- Node Architecture Change
- Tutorial Enhancement
- Juvix Types/Package Update
- Repository Maintenance
PR Management:
- Provide a clear and concise description of the changes.
- Link to important pages of the PR preview if available.
- Add the changelog entry by running the unclog command, after creating
  the PR so that the PR number is taken into account.
- Add the appropriate labels to the PR.
- Assign the PR to the correct person, typically the author.
- Set the milestone for the PR, ensuring it aligns with the next release.
- Confirm if the PR is ready for review; if not, mark it as a draft.
- Ensure the PR title and description are clear and concise.
- Verify that changes are closely related to the PR title and description,
  focusing on a single change topic per PR.
Grammar Checks: Ensure that all text in the PR is grammatically correct.
Whitespace: Verify that there are no unnecessary whitespaces in the
code. Although, this is may be done automatically by the CI/CD pipeline.

AHartNtkn added 7 commits

February 19, 2025 23:09


          kind implementation

9d2311e


          Add proving system

6b96503


          Add kind aqnd delta to resources

6e69c73


          missed for resources

7eaae09


          add delta page

eabf315


          compliance proofs

509a9f4


          compliance unit

89117ca

AHartNtkn added the resource-machine label

AHartNtkn requested a review from jonaprieto

February 21, 2025 04:22

AHartNtkn self-assigned this

github-actions bot commented Feb 21, 2025 •

edited

Loading

The typecheck failed. Please check the logs. However, the preview is available at https://specs.anoma.net/pr-344/.

Anoma Research and others added 2 commits

February 21, 2025 04:24


          Fix issues detected by pre-commit

0735bca


          Merge branch 'topic-transaction-function' into anthony/types_1

0c34ac4

heueristik requested changes

View reviewed changes

Contributor

heueristik left a comment

Review Part 1

docs/arch/system/types/compliance_proving_system.juvix.md Outdated


		### Consumed Resource Witness

		The doc states that each consumed resource has five data points in the witness:

Contributor

heueristik Feb 25, 2025

Which doc? This sentence sounds like a leftover

Contributor Author

AHartNtkn Feb 25, 2025

I expect everything I wrote to eventually be overwritten. Copy/editing for leftovers is a waste of time at this point.

Contributor Author

AHartNtkn Feb 25, 2025

compliance_proof.juvix.md

docs/arch/system/types/compliance_proving_system.juvix.md

+              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

Contributor

heueristik Feb 25, 2025

Would a link to the compliance proof documentation make sense here??

docs/arch/system/types/compliance_proving_system.juvix.md Outdated


		### ComplianceWitness

		The doc merges all consumed resource witness data and created resource witness

Contributor

heueristik Feb 25, 2025

Which doc? (See above)
I will stop marking this in the following

Contributor Author

AHartNtkn Feb 25, 2025

compliance_proof.juvix.md

docs/arch/system/types/compliance_proving_system.juvix.md

+. `nullifierKey`
+. `CTreePath`
+. `commitment`
+. opening of `logicRefHash` (stored as `ByteString` below)

Contributor

heueristik Feb 25, 2025

What's an opening?

Contributor Author

AHartNtkn Feb 25, 2025 •

edited

Loading

Good question! I have no idea, and it's not explained. It's mentioned in compliance_proof.juvix.md under Witness.

docs/arch/system/types/compliance_proving_system.juvix.md

+              There also has to exist some method to dereference resources.
+              ```juvix
+              axiom dereferenceNullifier : LogicRef -> Nullifier;

Contributor

heueristik Feb 25, 2025

Suggested change

      
            axiom dereferenceNullifier : LogicRef -> Nullifier;
          
            axiom dereferenceNullifier : NullifierRef -> Nullifier;

docs/arch/system/types/compliance_proving_system.juvix.md

Comment on lines +89 to +90

		(List (ConsumedResourceWitness A))
		(List CreatedResourceWitness);

Contributor

heueristik Feb 25, 2025

Shouldn't these be the consumed and created ordered sets from the Action (having the same order as the nullifiers and commitments)?

They allow to map tags (nullifiers and commitments) to resource objects which is often required in the resource logic.

Contributor Author

AHartNtkn Feb 26, 2025 •

edited

Loading

Are these the same? compliance_proof.juvix.md doesn't mention Action when defining the components of witnesses under the #### Witness section. All it says about Action is

Compliance proofs must be composition-independent: composing two actions, the compliance proof sets can be simply united to provide a valid composed action compliance proof set.

otherwise, actions aren't mentioned. I also can't claim to know what actions are supposed to be in the first place.

docs/arch/system/types/compliance_proving_system.juvix.md


		The doc’s constraints for each consumed resource:

		1. `resourceNullifier(r, nk) == nfRef`

Contributor

heueristik Feb 25, 2025

Suggested change

      
            1. `resourceNullifier(r, nk) == nfRef`
          
            1. `resourceNullifier(r, nk) == nf`

Why does this return a reference? This appears again later. Am I missing something? An explanation would be great.

Contributor Author

AHartNtkn Feb 26, 2025

Hmm... the relevant page is compliance_proof.juvix.md. The actual constraint there is

r.nullifier(nullifierKey) is in consumedResourceTagSet

I think I may have also been looking at

r.nullifier(nullifierKey) = nullifierHash(nullifierKey, r)

from nullifier.juvix.md which seems to identify a nullifier with its hash.

I decided to leave these unfinished since I realized I was wasting time thinking about constraints when my job was to make sure the types make sense. Really, these lines should have all been deleted before I pushed.

docs/arch/system/types/compliance_proving_system.juvix.md Outdated Show resolved Hide resolved

docs/arch/system/types/compliance_proving_system.juvix.md

+              The doc’s constraints for each consumed resource:
+. `resourceNullifier(r, nk) == nfRef`
+. `resourceCommitment(r) == cm`

Contributor

heueristik Feb 25, 2025

Why is this needed? More explanation would be helpful.
Is this check making sure that the consumed resource has existed before being consumed?
We should also explain what happens in the case of ephemeral resources.

Contributor Author

AHartNtkn Feb 26, 2025

It's copy/pasted from somewhere in the docs, with slight modification. Specifically, it comes from this line from compliance_proof.juvix.md

2. Consumed commitment integrity: `r.commitment() = cm`

Why is it there? I don't know. You shouldn't be asking me, because I had no input on it in the first place. It was something I was given.

docs/arch/system/types/compliance_proving_system.juvix.md

+                        case nfRefAndRootRef of {
+                        | (nfRef, rootRf) :=
+                          let
+                            passNF     : Bool := nfRef == resourceNullifier r nk;

Contributor

heueristik Feb 25, 2025 •

edited

Loading

Suggested change

      
                          passNF     : Bool := nfRef == resourceNullifier r nk;
          
                          passNF     : Bool := nf == resourceNullifier r nk;

I am also in favour of longer, more explicit naming.
The time being lost on misinterpretations by different teams outweighs the time to write slightly longer names by orders of magnitude.

IMO nullifierDerivationCheck would be a much better name than passNF.
It also makes things more searchable.

AHartNtkn and others added 6 commits

February 25, 2025 19:07


          Add warnings to constraint sections

4447f4a


          Merge branch 'anthony/types_1' of https://github.com/anoma/nspec into…

709dd23

… anthony/types_1


          Clarify what doc is being mentioned

e592730


          Update docs/arch/system/types/compliance_proving_system.juvix.md

f4cb605

Co-authored-by: Michael <[email protected]>


          fix/update github actions (#351)

998aa2d

- fix github workflow error due to deprecated action versions
- all workflows: use latest major versions of actions
- PR: mkdocs builds in parallel as separate jobs to reduce build time
(to 20min from 30min)
- PR: do not trigger workflow when PR is edited or marked ready for
review

## Error when buildings PRs

> Error: This request has been automatically failed because it uses a
deprecated version of `actions/cache: v4.0.2`.
> Please update your workflow to use v3/v4 of actions/cache to avoid
interruptions.
> Learn more:
https://github.blog/changelog/2024-12-05-notice-of-upcoming-releases-and-breaking-changes-for-github-actions/#actions-cache-v1-v2-and-actions-toolkit-cache-package-closing-down

## PR Todo List

- **Type of Change**: Mark the relevant option(s) with 'x':
  - [ ] System Architecture Change
  - [ ] Node Architecture Change
  - [ ] Tutorial Enhancement
  - [ ] Juvix Types/Package Update
  - [ ] Repository Maintenance
- **PR Management**:
  - [ ] Provide a clear and concise description of the changes.
  - [ ] Link to important pages of the PR preview if available.
- [ ] Add the changelog entry by running the `unclog` command, after
creating
    the PR so that the PR number is taken into account.
  - [ ] Add the appropriate labels to the PR.
  - [ ] Assign the PR to the correct person, typically the author.
- [ ] Set the milestone for the PR, ensuring it aligns with the next
release.
- [ ] Confirm if the PR is ready for review; if not, mark it as a draft.
  - [ ] Ensure the PR title and description are clear and concise.
- [ ] Verify that changes are closely related to the PR title and
description,
    focusing on a single change topic per PR.
- **Grammar Checks**: Ensure that all text in the PR is grammatically
correct.
- **Whitespace**: Verify that there are no unnecessary whitespaces in
the
code. Although, this is may be done automatically by the CI/CD pipeline.


          Merge remote-tracking branch 'origin/main' into anthony/types_1

b33990d

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

resource-machine