Add frontend support for Anoma Resource Machine builtins #3113
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds frontend builtin support for the Anoma Resource machine functions provided in resource-machine.hoon, except for the
prove-logic
function which still needs some discussion.Users must now mark the Anoma
Resource
type withbuiltin-anoma-resource
and the AnomaAction
type withbuiltin-anoma-action
. This is required because the resource machine functions use these types.The compiler does not check that the constructors of
Resource
andAction
match the RM spec. I made this decision because the Anoma types are sill in flux and it's easier to change if correctness is delegated to the RM library for now. We can add the constructor checks when the Anoma RM interface is stable.The test file test085.juvix demonstrates how each builtin should be used.
Core Evaluator
The Core evaluator does not support these builtin functions in normal mode. When used for normalisation (e.g when used in the constant folding pass) the Core evaluator leaves the builtin functions unchanged.
Nock Evaluator
The Nock evaluator does not intercept the Anoma lib functions that the builtins correspond to in the Nock backend. It executes the underlying Nock code instead. This means that several of the functions cannot be tested because they're either too slow (e.g commitment) or do not have an implementation in the Nock code (e.g addDelta).