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.

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

Support random API from the Anoma stdlib #3129

Merged
merged 11 commits into from
Oct 29, 2024
Merged

Support random API from the Anoma stdlib #3129

merged 11 commits into from
Oct 29, 2024

Conversation

paulcadman
Copy link
Collaborator

@paulcadman paulcadman commented Oct 28, 2024 •
edited
Loading

This PR adds frontend support for the Anoma Random API:

The frontend builtin APIs are:

builtin anoma-random-generator
axiom RandomGenerator : Type;

builtin anoma-random-generator-init
axiom randomGeneratorInit : Nat -> RandomGenerator;

builtin anoma-random-generator-split
axiom randomGeneratorSplit : RandomGenerator
  -> Pair RandomGenerator RandomGenerator;

builtin anoma-random-next-bytes
axiom randomNextBytes : Nat
  -> RandomGenerator
  -> Pair ByteArray RandomGenerator;

Nockma Evaluator

The Nockma evaluator intercepts the corresponding Anoma random stdlib calls using the System.Random API. The implementation uses the splitmix generator directly because it has an API to destructure the generator into a pair of integers. We can use this to serialise the generator.

@paulcadman paulcadman self-assigned this Oct 28, 2024
@paulcadman paulcadman marked this pull request as ready for review October 29, 2024 11:32
@paulcadman paulcadman added this to the 0.6.7 milestone Oct 29, 2024
@paulcadman
Add nock definitions of Anoma stdlib random functions
791b2fb
@paulcadman
Implement random functions in the Nockma evaluator
a02e304 
The default System.Random generator from the splitmix package is used
explicitly here so it can be destructured and serialized as a pair of
atoms.
@paulcadman
Do not include length in random output
9b6f491 
The Anoma stdlib does not include the length in the corresponding API.
@paulcadman
Add frontend for Anoma random APIs
7491d76
@paulcadman
Add tests for StdlibRandom{InitGen, NextBytes, Split}
450f24d
@paulcadman
Add primitive RandomGenerator type
a0e8816
@paulcadman
Rename anoma random builtins
462c856
@paulcadman
Fix StdlibRandomNextBytes translation in nockma backend
0008b17
@paulcadman
Add Anoma random API frontend compilation test
c928880
@paulcadman
Improve types for anoma random types
920ddbc
@paulcadman
Do not duplicate the first argument to randomNextBytes
e1ea6f1
@paulcadman paulcadman merged commit 3b34f6e into main Oct 29, 2024
4 checks passed
@paulcadman paulcadman deleted the nock-random branch October 29, 2024 18:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@lukaszcz lukaszcz lukaszcz approved these changes

@janmasrovira janmasrovira Awaiting requested review from janmasrovira

Assignees

@paulcadman paulcadman

Labels
anoma backend:nockma enhancement New feature or request
Projects
None yet
Milestone
0.6.7
Development

Successfully merging this pull request may close these issues.

Add a randomBytes builtin to generate cryptographically secure bytes
2 participants
@paulcadman @lukaszcz