Add type files for proving system, compliance proving system, delta, and kind. by AHartNtkn · Pull Request #344 · anoma/nspec

AHartNtkn · 2025-02-21T04:22:27Z

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.

github-actions · 2025-02-21T04:24:38Z

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

heueristik

Review Part 1

heueristik · 2025-02-25T13:58:48Z

+
+### Consumed Resource Witness
+
+The doc states that each consumed resource has five data points in the witness:


Which doc? This sentence sounds like a leftover

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

compliance_proof.juvix.md

heueristik · 2025-02-25T14:01:05Z

+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


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

heueristik · 2025-02-25T14:01:25Z

+
+### ComplianceWitness
+
+The doc merges all consumed resource witness data and created resource witness


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

compliance_proof.juvix.md

heueristik · 2025-02-25T14:03:56Z

+2. `nullifierKey`
+3. `CTreePath`
+4. `commitment`
+5. opening of `logicRefHash` (stored as `ByteString` below)


What's an opening?

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

heueristik · 2025-02-25T14:07:32Z

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


Suggested change

axiom dereferenceNullifier : LogicRef -> Nullifier;

axiom dereferenceNullifier : NullifierRef -> Nullifier;

heueristik · 2025-02-25T14:20:44Z

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


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.

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.

heueristik · 2025-02-25T14:21:28Z

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


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.

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.

heueristik · 2025-02-25T14:24:29Z

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


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.

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.

heueristik · 2025-02-25T14:35:11Z

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


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.

… anthony/types_1

Co-authored-by: Michael <20623991+heueristik@users.noreply.github.com>

- 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.

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 Feb 21, 2025

AHartNtkn requested a review from jonaprieto February 21, 2025 04:22

AHartNtkn self-assigned this Feb 21, 2025

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 Feb 25, 2025

View reviewed changes

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 <20623991+heueristik@users.noreply.github.com>

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

b33990d


		### Consumed Resource Witness

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


		### ComplianceWitness

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

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

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


		The doc’s constraints for each consumed resource:

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

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

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

Uh oh!

Conversation

AHartNtkn commented Feb 21, 2025

PR Todo List

Uh oh!

github-actions Bot commented Feb 21, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

heueristik left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

AHartNtkn Feb 25, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

AHartNtkn Feb 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

heueristik Feb 25, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

github-actions Bot commented Feb 21, 2025 •

edited

Loading

AHartNtkn Feb 25, 2025 •

edited

Loading

AHartNtkn Feb 26, 2025 •

edited

Loading

heueristik Feb 25, 2025 •

edited

Loading