Skip to content
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.

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

Support Nockma/Anoma scry operation #2672

Closed
paulcadman opened this issue Feb 26, 2024 · 0 comments · Fixed by #2678
Closed

Support Nockma/Anoma scry operation #2672

paulcadman opened this issue Feb 26, 2024 · 0 comments · Fixed by #2678

Comments

@paulcadman
Copy link
Collaborator

paulcadman commented Feb 26, 2024

Anoma Scry Semantics

The scry OP is represented in Nock using the atom 12. It's purpose is to read from a key-value storage.

The following semantics are deduced from the Anoma codebase:

https://github.com/anoma/anoma/blob/6769dafbe8ef9d9cea1056698a23a6d986f777d6/lib/nock.ex#L142

     s * t1 => t1'   s * t2 => t2'
-----------------------------------------
  s * [scry t1 t2] => read_with_id t2'

Explanation from Ray:

[scry looks like]:

[12 type-info path]

[scry's] semantic is "pull magic data from path", where path is a referentially
transparent key (it's a list of atoms) into the magic data store. in urbit, scry
is a virtual operation implemented at higher virtualization levels of the
system; in anoma it's a "real" operation against the interpreter. it's used to
read data

in the current anoma codebase you can see it used in execution; it does a
blocking read against /[some random id]/key

so execution pauses there until the transaction is ordered, even though it
starts immediately in the mempool

The read_with_id function indeed blocks until the value of the path is returned from storage. If the key is not found it returns an error (i.e crashes).

Juvix support

Users will need to use Scry in their Anoma applications so we need to provide a
Juvix front-end function that compiles to Nockma/Anoma Scry. (It's not clear to me how the user would obtain the id associated with a value or what kind of applications would require this)

We could add a builtin function for this:

type AnomaStorageId (Key : Type) := mk { storageId : Nat ; key : Key }
axiom anomaGet : {Value  Key : Type} -> AnomaStorageId Key -> Value;
@paulcadman paulcadman self-assigned this Mar 3, 2024
janmasrovira added a commit that referenced this issue Mar 21, 2024
This PR adds support for Anoma/Nockma scry OP. It is used for obtaining
values from the Anoma storage (key value store). See the [linked
issue](#2672) for details on scry.

This PR adds support for scry to the Nockma language and compilation
from the frontend via a builtin: `anoma-get`:

```
builtin anoma-get
axiom anomaGet : {Value Key : Type} -> Key -> Value
```

In the backend, the `Value` and `Key` types could be anything, they will
depend on choices of Anoma applications. The type of the returned
`Value` is unchecked. It's currently the responsibility of the user to
match the annotated type with the type of data in storage.

We will not put this builtin in the standard library. It will be exposed
in the anoma-juvix library. It's likely that the frontend `anomaGet`
function will evolve as we use it to write Anoma applications and learn
how they work.

* Closes #2672

---------

Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant