The `anoma-bytearray-{to, from}-anoma-contents` are intended to be used
to convert to/from atoms representing `ByteArrays`. These builtins are
required temporarily until Anoma Node makes ByteArray representation
uniform across all of its APIs.
We represent ByteArrays in nock as a cell:
```
[size contents]
```
Where `size` is the size of the ByteArray and `contents` is an Atom
representing the bytes in LSB ordering.
The `size` is required in general because the encoding of ByteArrays to
Atoms is ambiguous. For example the ByteArrays [0x01; 0x00] and [0x01]
are represented by `1`.
Some Anoma ByteArrays like keys and signatures are represented using on
the `contents` atom because the size is constant.
Users of Anoma APIs have to strip / add size information from ByteArrays
depending on where the data is used. The new builtins provide this
facility.
These builtins are temporary because it's been agreed with Anoma
engineering team to change the Anoma APIs to make the ByteArray
representation uniform, i.e always represent ByteArrays using `[size
content]`. When this is implemented in Anoma Node we can remove these
builtins.
```
builtin anoma-bytearray-to-anoma-contents
axiom toAnomaContents : ByteArray -> Nat;
builtin anoma-bytearray-from-anoma-contents
axiom fromAnomaContents :
-- | The size of the ByteArray
Nat
-- | The contents of the ByteArray
-> Nat
-- | The resulting ByteArray
-> ByteArray;
```
This PR updates:
- [x] Package version
- [x] Smoke test
- [x] Changelog
We can't merge this until the stdlib submodule pointer is fixed-up to
point to stdlib main.
* Specialization has become less effective after recent changes to the
codebase. This PR fixes issues with specialization.
* Closes#2939
* Closes#2945
Checklist
---------
- [X] Preserve pragmas for letrec and lambda in Stored Core
- [x] Remove the assumption that all type variables are at the front
(closes#2945)
- [x] Allow specialization when the argument is a constructor
application
- [x] Make renaming adjust pragmas
- [x] Allow pragmas for fields in record definitions (closes#2939)
- [x] Update standard library pragmas
- [x] Fix JuvixTree printing
This PR adds support for ByteArray in the Anoma cryptographic functions.
```
builtin anoma-sign
axiom anomaSign : {A : Type} -> A -> ByteArray -> ByteArray;
builtin anoma-verify-with-message
axiom anomaVerifyWithMessage : {A : Type} -> ByteArray -> ByteArray -> Maybe A;
builtin anoma-sign-detached
axiom anomaSignDetached : {A : Type} -> A -> ByteArray -> ByteArray;
builtin anoma-verify-detached
axiom anomaVerifyDetached : {A : Type} -> ByteArray -> A -> ByteArray -> Bool;
```
The Anoma / Hoon Stdlib function `length` needs to be exposed as a
StdlibFunction because a ByteArray stores its length and the value
returned by `anomaSign` is not a fixed length.
This PR adds support for a builtin `ByteArray` type and associated
functions for constructing a `ByteArray` from a list of bytes and a
function to query the size of the `ByteArray`. It is only available in
the Anoma backend.
In Core / Tree, ByteArray constant is stored using a Haskell ByteString.
In Anoma the ByteArray is stored as a cell where the head is the length
of the ByteArray and the tail is an integer is an integer formed by
concatenating the bytes in the array using little-endian byte ordering.
The Nock for constructing a `ByteArray` uses the `length`, `add`,
`folder` and `lsh` functions from the Anoma hoon stdlib. See the [code
comment](fa068a30e7/src/Juvix/Compiler/Nockma/StdlibFunction.hs (L37))
for more details.
Example:
```
module test082;
import Stdlib.Prelude open;
import Stdlib.Debug.Trace open;
builtin bytearray
axiom ByteArray : Type;
builtin bytearray-from-list-byte
axiom mkByteArray : List Byte -> ByteArray;
builtin bytearray-size
axiom size : ByteArray -> Nat;
bs0 : ByteArray := mkByteArray [];
bs1 : ByteArray := mkByteArray [0x0; 0x0; 0x0];
bs2 : ByteArray := mkByteArray [0x1; 0x0; 0x0; 0x0];
bs3 : ByteArray := mkByteArray [0x2; 0x1];
bs4 : ByteArray := mkByteArray [0x100];
main : ByteArray :=
trace (size bs0)
>-> trace bs0
>-> trace (size bs1)
>-> trace bs1
>-> trace (size bs2)
>-> trace bs2
>-> trace (size bs3)
>-> trace bs3
>-> trace (size bs4)
>-> bs4;
```
Output using `tests/Anoma/Compilation/positive/test082.juvix`
```
$ juvix compile anoma -g test082.juvix
$ juvix dev nockma run test082.pretty.nockma
0
[0 0]
3
[3 0]
4
[4 1]
2
[2 258]
1
[1 0]
```
1. Refactors css theme to only use variables as source for colors to
make it easier to define themes. In order to define a theme, the
following variables need to be defined (these variables have been taken
mostly from the catppuchin theme):
```
/* Code */
--ju-inductive: var(--ctp-green);
--ju-constructor: var(--ctp-mauve);
--ju-function: var(--ctp-yellow);
--ju-module: var(--ctp-lavender);
--ju-axiom: var(--ctp-red);
--ju-string: var(--ctp-flamingo);
--ju-keyword: var(--ctp-sky);
--ju-delimiter: var(--ctp-overlay2);
--ju-var: var(--ctp-text);
--ju-fixity: var(--ctp-sapphire);
--ju-comment: var(--ctp-rosewater);
--ju-judoc: var(--ctp-teal);
--ju-number: var(--ctp-peach);
/* Text */
--ju-text: var(--ctp-text);
--ju-subtext1: var(--ctp-subtext1);
--ju-subtext0: var(--ctp-subtext0);
/* Overlay */
--ju-overlay0: var(--ctp-overlay0);
--ju-overlay1: var(--ctp-overlay1);
--ju-overlay2: var(--ctp-overlay2);
/* Surface */
--ju-surface0: var(--ctp-surface0);
--ju-surface1: var(--ctp-surface1);
--ju-surface2: var(--ctp-surface2);
/* Panes */
--ju-base: var(--ctp-base);
--ju-mantle: var(--ctp-mantle);
--ju-crust: var(--ctp-mantle);
/* Theme */
--ju-main: var(--ctp-maroon);
--ju-main-link: var(--ctp-maroon);
--ju-main-link-visited: var(--ctp-flamingo);
--ju-warning: var(--ctp-red);
```
2. When changing theme, the judoc documentation will also use that
theme, as opposed to only the source code.
3. Added highlighting for module names.
4. When hovering a juvix code element (axiom, constructor, inductive,
etc.), the underline will be of the correct color for the kind. Before
it was always a fixed color.
This PR adds `Byte` as a builtin with builtin functions for equality,
`byte-from-nat` and `byte-to-nat`. The standard library is updated to
include this definition with instances for `FromNatural`, `Show` and
`Eq` traits.
The `FromNatural` trait means that you can assign `Byte` values using
non-negative numeric literals.
You can use byte literals in jvc files by adding the u8 suffix to a
numeric value. For example, 1u8 represents a byte literal.
Arithmetic is not supported as the intention is for this type to be used
to construct ByteArrays of data where isn't not appropriate to modify
using arithmetic operations. We may add a separate `UInt8` type in the
future which supports arithmetic.
The Byte is supported in the native, rust and Anoma backend. Byte is not
supported in the Cairo backend because `byte-from-nat` cannot be
defined.
The primitive builtin ops for `Byte` are called `OpUInt8ToInt` and
`OpUInt8FromInt`, named because these ops work on integers and in future
we may reuse these for a separate unsigned 8-bit integer type that
supports arithmetic.
Part of:
* https://github.com/anoma/juvix/issues/2865
This PR adds `FromNatural` to package-base. The change is backwards
compatible for existing Juvix code so we don't need to make a new
version of package-base. The new trait is unused, it will be integrated
in subsequent PRs.
### `FromNatural` trait
The `FromNatural` trait has the following definition.
```
trait
type FromNatural A :=
mkFromNatural {
builtin from-nat
fromNat : Nat -> A
};
```
### `Natural` trait changes
The `Natural` trait is changed to remove its `fromNat` field and add a
new instance field for `FromNatural A`.
### juvix-stdlib changes
`FromNatural` instances are added for `Int` and `Field` in the standard
library.
## Rationale
The `FromNatural` trait will be used for the Bytes type.
We want the following properties for Byte:
1. Values of the Bytes type should be assignable from a non-negative
numeric literal.
2. We don't want to implement + and * for Bytes.
Currently, in order for a type to have property 1. it must have an
instance of `Natural` so property 2. can't be satisfied.
To solve this we split the `from-nat` builtin from the `Natural` trait
into a new trait `FromNatural`.
1. When the flatparse scanner fails and we fallback to megaparsec, a
warning is issued.
2. The flatparse scanner has been fixed so it is not confused when a
name starts with `import`.
This PR addresses a bug/missing case present since v0.6.2, introduced
specifically by
- PR #2779,
That PR involves detecting imports in Juvix files before type checking,
and that's the issue.
Detecting/scanning imports is done by running a flat parser (which
ignores the Juvix Markdown structure) and when it fails, it runs a
Megaparser parse. So, for simplicity,
we could just continue using the same Megaparser as before for Juvix
Markdown files.
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
- Closes#2923
This pr fixes a bug where all fields were assigned to be explicit
arguments in the NameSignature Builder. A single line change was enough
to fix it.
```diff
- RecordStatementField RecordField {..} -> addSymbol @s Explicit Nothing _fieldName _fieldType
+ RecordStatementField RecordField {..} -> addSymbol @s (fromIsImplicitField _fieldIsImplicit) Nothing _fieldName _fieldType
```
I've also added a compilation test for instance fields.
1. Adds the `--log-level LOG_LEVEL` flag to the CLI. This flag can be
given `error`, `warn`, `info`, `progress`, `debug` as argument to filter
the logged messages.
2. Removes the `--only-errors` flag.
3. Adds the `--ide-end-error-char CHAR`, which receives a character as
an argument, which is appended to the end of error messages. This is
handy to facilitate parsing of errors messages from the ide. This
functionality was previously embeded in the old `--only-errors` flag.
* Closes#2813
Implements a translation from Juvix functions to Isabelle/HOL functions.
This extends the previous Juvix -> Isabelle translation which could
handle only type signatures.
Checklist
---------
- [x] Basic translation
- [x] Polymorphism
- [x] Arithmetic operators
- [x] Numeric literals
- [x] List literals
- [x] Comparison operators
- [x] Boolean operators
- [x] `if` translated to Isabelle `if`
- [x] `true` and `false` translated to Isabelle `True` and `False`
- [x] `zero` and `suc` translated to Isabelle `0` and `Suc`
- [x] `Maybe` translated to Isabelle `option`
- [x] Pairs translated to Isabelle tuples
- [x] Quote Isabelle identifier names (e.g. cannot begin with `_`)
- [x] Rename variables to avoid clashes (in Isabelle/HOL pattern
variables don't shadow function identifiers)
- [x] Common stdlib functions (`map`, `filter`, etc) translated to
corresponding Isabelle functions
- [x] Multiple assignments in a single `let`
- [x] CLI
- [x] Test
- The test is very fragile, similar to the markdown test. It just
compares the result of translation to Isabelle against a predefined
expected output file.
Limitations
-----------
The translation is not designed to be completely correct under all
circumstances. There are aspects of the Juvix language that cannot be
straightforwardly translated to Isabelle/HOL, and these are not planned
to ever be properly handled. There are other aspects that are difficult
but not impossible to translate, and these are left for future work.
Occasionally, the generated code may need manual adjustments to
type-check in Isabelle/HOL.
In particular:
* Higher-rank polymorphism or functions on types cannot be translated as
these features are not supported by Isabelle/HOL. Juvix programs using
these features will not be correctly translated (the generated output
may need manual adjustment).
* In cases where Juvix termination checking diverges from Isabelle/HOL
termination checking, providing a termination proof manually may be
necessary. Non-terminating Juvix functions cannot be automatically
translated and need to be manually modelled in Isabelle/HOL in a
different way (e.g. as relations).
* Comments (including judoc) are ignored. This is left for future work.
* Traits are not translated to Isabelle/HOL type classes / locales. This
is left for future work.
* Mutually recursive functions are not correctly translated. This is
left for future work.
* Record creation, update, field access and pattern matching are not
correctly translated. This is left for future work.
* Named patterns are not correctly translated. This is left for future
work.
* Side conditions in patterns are not supported. This is left for future
work.
* If a Juvix function in the translated module has the same name as some
function from the Isabelle/HOL standard library, there will be a name
clash in the generated code.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
Since it is common to want to assign a named argument a variable of the
same name, we add special syntax for it. E.g.
```
f (fieldA : A) (fieldB : B) : S :=
mkS@{
fieldC := fieldA; -- normal named argument
fieldA; -- pun
fieldB -- pun
};
```
- Closes#2668
This pr migrates the old named application syntax to the new one. In
order to migrate a juvix file to the new syntax it suffices to run the
formatter.
After the next release, we should completely remove the support for the
old syntax.
## Other changes
I've improved Scope negative tests. Previously, when a negative test
failed, you could only see the title of the test and the message
"Incorrect Error", as well as the Haskell file and line where the test
is defined.
This is extremely incovenient because you have to go to the haskell test
file, go to the line where the error is defined, look at the name of the
file and then visit that file. Moreover, you need to manually run the
scoper on that file to see the error that was returned.
I've fixed that and it now shows all relevant information. Example:
I've implemented this only using the `Generic` instance for the
`ScoperError` type, so doing something similar for the rest of negative
tests should be straightforward.
This pr explores the option to implement error handling in Juvix à la
mtl. It adds the following as a test:
1. `MonadError` trait.
2. `MonadTrans` trait.
3. `ExceptT` monad transformer and its `Functor`, `Monad`, `MonadTrans`,
`MonadError` instances.
- Syntax for #2804.
- ⚠️ Depends on #2869.
This pr introduces:
1. front-end support (parsing, printing, typechecking) for boolean side
conditions for branches of case expressions.
2. Now `if` is a reserved keyword.
3. Multiway `if` is allowed to have only the `else` branch. I've also
refactored the parser to be simpler.
Example:
```
multiCaseBr : Nat :=
case 1 of
| zero
| if 0 < 0 := 3
| else := 4
| suc (suc n)
| if 0 < 0 := 3
| else := n
| suc n if 0 < 0 := 3;
```
The side if branches must satisfy the following.
1. There must be at least one `if` branch.
4. The `else` branch is optional. If present, it must be the last.
Future work:
1. Translate side if conditions to Core and extend the exhaustiveness
algorithm.
5. Add side if conditions to function clauses.
* Closes#2703
* Adds [peephole
optimization](https://en.wikipedia.org/wiki/Peephole_optimization) of
Cairo assembly.
* Adds a transformation framework for the CASM IR.
* Adds `--transforms`, `--run` and `--no-print` options to the `dev casm
read` command.
* Closes#2829
* Adds a transformation which converts `br` to `if` when the variable
branched on was assigned in the previous instruction. The transformation
itself doesn't check liveness and doesn't remove the assignment. Dead
code elimination should be run afterwards to remove the assignment.
* For Cairo, it only makes sense to convert `br` to `if` for equality
comparisons against zero. The assignment before `br` will always become
dead after converting `br` to `if`, because we convert to SSA before.
This PR adds support for the `anoma{encode, decode, sign, verify,
signDetached, verifyDetached}` functions to the Core evaluator.
## Encoding / Decoding
The serialization of values to `ByteString` for `anomaEncode` reuses the
Stored Core serialization. The Stored Core `Node` is extended to include
closures.
Anoma expects encoding of bytes as little-endian integers. In general
`ByteString -> Integer` is ambiguous because two `ByteString`s that
differ only by zero padding will map to the same integer. So we must
encode the length of the ByteString in the encoded integer alongside the
ByteString data so when it is decoded we can pad appropriately. We use
the same length encoding scheme that is used by Nockma jam.
## Verify
The Core evaluator implementation of `anomaVerify` crashes if the
verification fails. This matches the behaviour of Anoma node.
### `jvc` Support
You can now use `anoma-*` functions within `.jvc` core files.
* Closes https://github.com/anoma/juvix/issues/2808
- This PR adds a temporary compiler error for when the bug #2247
happens. We do not have plans to fix this bug until we move the
typechecker to Core, so it makes sense to add a better error message.
* Closes#2827
* Adds an optimization phase to the JuvixReg -> Casm pipeline, which
consists of repeated copy & constant propagation and dead code
elimination.
- Closes#2429
This pr introduces two enchancements to import statements:
1. They can have `using/hiding` list of symbols, with a behaviour
analogous to the open statement.
2. They can be public. When an import is marked as public, a local
module (or a series of nested local modules) is generated like this:
```
import A public;
-- equivalent to
import A;
module A;
open A public;
end;
```
It is easier to understand when there is an alias.
```
import A as X.Y public;
-- equivalent to
import A;
module X;
module Y;
open A public;
end;
end;
```
Public imports are allowed to be combined with `using/hiding` modifier
and open statements with the expected behaviour.
* Closes#2845
* Copy propagation is not correct without subsequent adjusting of live
variables. See the comments in #2845.
* Enables JuvixReg transformations in the test suite, which exposes the
bug.
* Adds a test in JuvixAsm crafted specifically to expose this bug.
* Closes#1614
* Implements the copy propagation transformation in JuvixReg and adds
tests for it.
* For this optimization to give any improvement, we need to run dead
code elimination afterwards (#2827).
* Types of arguments to `main` can now be field elements, numbers,
booleans and (nested) records and lists.
* Type of `main` result can now be a record of field elements, numbers
and booleans. Lists or nested records are not allowed for the result.
* Adds checks for the type of `main` in the Cairo pipeline.
* Requires updating
[juvix-cairo-vm](https://github.com/anoma/juvix-cairo-vm). The input can
be provided in a Json file via the `--program_input` option of
`juvix-cairo-vm`.
* Adds a RISC0 backend which generates Rust code that can be compiled
with the official RISC0 toolchain.
* The RISC0 backend is a wrapper around the Rust backend.
* Adds the `risc0-rust` to the `compile` CLI command, which creates a
directory containing host and guest Rust sources for the RISC0 zkVM. The
generated code can be compiled/run using `cargo` from inside the created
directory (requires having RISC0 installed:
https://dev.risczero.com/api/zkvm/install).
This PR adds support for the Anoma stdlib `sign-detached` API.
```
builtin anoma-sign-detached
axiom anomaSignDetached : {A : Type}
-- message to sign
-> A
-- private key
-> Nat
-- signature
-> Nat;
```
This corresponds to the
[sign_detached](https://hexdocs.pm/enacl/enacl.html#sign_detached-2)
libsodium API.
This is requried to support to new Anoma nullifier format:
d6a61451ae
Previously resource nullifiers were defined using `anomaSign`:
```
nullifier (r : Resource) (secretKey : Nat) : Nat :=
anomaSign (anomaEncode (nullifierHeader, r)) secretKey;
```
They are now defined using `anomaSignDetached`:
```
nullifier (r : Resource) (secretKey : Nat) : Nat :=
let encodedResource : Nat := anomaEncode (nullifierHeader, r) in
anomaEncode (encodedResource , anomaSignDetached encodedResource secretKey);
```
This is so that a logic function can access the nullified resources
directly from the `nullifier` field.
## Evaluator Note
When decoding a public key, private key or signature from an integer
atom to a bytestring it's important to pad the bytestring to the
appropriate number of bytes. For example a private key must be 64 bytes
but the corresponding encoded integer may fit into 63 bytes or fewer
bytes (depending on leading zeros). This PR also fixes this issue by
adding a
[`atomToByteStringLen`](c68c7187b1/src/Juvix/Compiler/Nockma/Encoding/ByteString.hs (L14))
function with also accepts the expected size of the resulting
bytestring.
This pr introduces parallelism in the pipeline to gain performance. I've
included benchmarks at the end.
- Closes#2750.
# Flags:
There are two new global flags:
1. `-N / --threads`. It is used to set the number of capabilities.
According to [GHC
documentation](https://hackage.haskell.org/package/base-4.20.0.0/docs/GHC-Conc.html#v:setNumCapabilities):
_Set the number of Haskell threads that can run truly simultaneously (on
separate physical processors) at any given time_. When compiling in
parallel, we create this many worker threads. The default value is `-N
auto`, which sets `-N` to half the number of logical cores, capped at 8.
2. `--dev-show-thread-ids`. When given, the thread id is printed in the
compilation progress log. E.g.
# Parallel compilation
1. I've added `src/Parallel/ParallelTemplate.hs` which contains all the
concurrency related code. I think it is good to keep this code separated
from the actual compiler code.
2. I've added a progress log (only for the parallel driver) that outputs
a log of the compilation progress, similar to what stack/cabal do.
# Code changes:
1. I've removed the `setup` stage where we were registering
dependencies. Instead, the dependencies are registered when the
`pathResolver` is run for the first time. This way it is safer.
1. Now the `ImportTree` is needed to run the pipeline. Cycles are
detected during the construction of this tree, so I've removed `Reader
ImportParents` from the pipeline.
3. For the package pathresolver, we do not support parallelism yet (we
could add support for it in the future, but the gains will be small).
4. When `-N1`, the pipeline remains unchanged, so performance should be
the same as in the main branch (except there is a small performance
degradation due to adding the `-threaded` flag).
5. I've introduced `PipelineOptions`, which are options that are used to
pass options to the effects in the pipeline.
6. `PathResolver` constraint has been removed from the `upTo*` functions
in the pipeline due to being redundant.
7. I've added a lot of `NFData` instances. They are needed to force the
full evaluation of `Stored.ModuleInfo` in each of the threads.
2. The `Cache` effect uses
[`SharedState`](https://hackage.haskell.org/package/effectful-core-2.3.0.1/docs/Effectful-State-Static-Shared.html)
as opposed to
[`LocalState`](https://hackage.haskell.org/package/effectful-core-2.3.0.1/docs/Effectful-Writer-Static-Local.html).
Perhaps we should provide different versions.
3. I've added a `Cache` handler that accepts a setup function. The setup
is triggered when a miss is detected. It is used to lazily compile the
modules in parallel.
# Tests
1. I've adapted the smoke test suite to ignore the progress log in the
stderr.
5. I've had to adapt `tests/positive/Internal/Lambda.juvix`. Due to
laziness, a crash happening in this file was not being caught. The
problem is that in this file we have a lambda function with different
number of patterns in their clauses, which we currently do not support
(https://github.com/anoma/juvix/issues/1706).
6. I've had to comment out the definition
```
x : Box ((A : Type) → A → A) := box λ {A a := a};
```
From the test as it was causing a crash
(https://github.com/anoma/juvix/issues/2247).
# Future Work
1. It should be investigated how much performance we lose by fully
evaluating the `Stored.ModuleInfo`, since some information in it will be
discarded. It may be possible to be more fine-grained when forcing
evaluation.
8. The scanning of imports to build the import tree is sequential. Now,
we build the import tree from the entry point module and only the
modules that are imported from it are in the tree. However, we have
discussed that at some point we should make a distinction between
`juvix` _the compiler_ and `juvix` _the build tool_. When using `juvix`
as a build tool it makes sense to typecheck/compile (to stored core) all
modules in the project. When/if we do this, scanning imports in all
modules in parallel becomes trivial.
9. The implementation of the `ParallelTemplate` uses low level
primitives such as
[forkIO](https://hackage.haskell.org/package/base-4.20.0.0/docs/Control-Concurrent.html#v:forkIO).
At some point it should be refactored to use safer functions from the
[`Effectful.Concurrent.Async`](https://hackage.haskell.org/package/effectful-2.3.0.0/docs/Effectful-Concurrent-Async.html)
module.
10. The number of cores and worker threads that we spawn is determined
by the command line. Ideally, we could use to import tree to compute an
upper bound to the ideal number of cores to use.
11. We could add an animation that displays which modules are being
compiled in parallel and which have finished being compiled.
# Benchmarks
On some benchmarks, I include the GHC runtime option
[`-A`](https://downloads.haskell.org/ghc/latest/docs/users_guide/runtime_control.html#rts-flag--A%20%E2%9F%A8size%E2%9F%A9),
which sometimes makes a good impact on performance. Thanks to
@paulcadman for pointing this out. I've figured a good combination of
`-N` and `-A` through trial and error (but this oviously depends on the
cpu and juvix projects).
## Typecheck the standard library
### Clean run (88% faster than main):
```
hyperfine --warmup 1 --prepare 'juvix clean' 'juvix -N 4 typecheck Stdlib/Prelude.juvix +RTS -A33554432' 'juvix -N 4 typecheck Stdlib/Prelude.juvix' 'juvix-main typecheck Stdlib/Prelude.juvix'
Benchmark 1: juvix -N 4 typecheck Stdlib/Prelude.juvix +RTS -A33554432
Time (mean ± σ): 444.1 ms ± 6.5 ms [User: 1018.0 ms, System: 77.7 ms]
Range (min … max): 432.6 ms … 455.9 ms 10 runs
Benchmark 2: juvix -N 4 typecheck Stdlib/Prelude.juvix
Time (mean ± σ): 628.3 ms ± 23.9 ms [User: 1227.6 ms, System: 69.5 ms]
Range (min … max): 584.7 ms … 670.6 ms 10 runs
Benchmark 3: juvix-main typecheck Stdlib/Prelude.juvix
Time (mean ± σ): 835.9 ms ± 12.3 ms [User: 788.5 ms, System: 31.9 ms]
Range (min … max): 816.0 ms … 853.6 ms 10 runs
Summary
juvix -N 4 typecheck Stdlib/Prelude.juvix +RTS -A33554432 ran
1.41 ± 0.06 times faster than juvix -N 4 typecheck Stdlib/Prelude.juvix
1.88 ± 0.04 times faster than juvix-main typecheck Stdlib/Prelude.juvix
```
### Cached run (43% faster than main):
```
hyperfine --warmup 1 'juvix -N 4 typecheck Stdlib/Prelude.juvix +RTS -A33554432' 'juvix -N 4 typecheck Stdlib/Prelude.juvix' 'juvix-main typecheck Stdlib/Prelude.juvix'
Benchmark 1: juvix -N 4 typecheck Stdlib/Prelude.juvix +RTS -A33554432
Time (mean ± σ): 241.3 ms ± 7.3 ms [User: 538.6 ms, System: 101.3 ms]
Range (min … max): 231.5 ms … 251.3 ms 11 runs
Benchmark 2: juvix -N 4 typecheck Stdlib/Prelude.juvix
Time (mean ± σ): 235.1 ms ± 12.0 ms [User: 405.3 ms, System: 87.7 ms]
Range (min … max): 216.1 ms … 253.1 ms 12 runs
Benchmark 3: juvix-main typecheck Stdlib/Prelude.juvix
Time (mean ± σ): 336.7 ms ± 13.3 ms [User: 269.5 ms, System: 67.1 ms]
Range (min … max): 316.9 ms … 351.8 ms 10 runs
Summary
juvix -N 4 typecheck Stdlib/Prelude.juvix ran
1.03 ± 0.06 times faster than juvix -N 4 typecheck Stdlib/Prelude.juvix +RTS -A33554432
1.43 ± 0.09 times faster than juvix-main typecheck Stdlib/Prelude.juvix
```
## Typecheck the test suite of the containers library
At the moment this is the biggest juvix project that we have.
### Clean run (105% faster than main)
```
hyperfine --warmup 1 --prepare 'juvix clean' 'juvix -N 6 typecheck Main.juvix +RTS -A67108864' 'juvix -N 4 typecheck Main.juvix' 'juvix-main typecheck Main.juvix'
Benchmark 1: juvix -N 6 typecheck Main.juvix +RTS -A67108864
Time (mean ± σ): 1.006 s ± 0.011 s [User: 2.171 s, System: 0.162 s]
Range (min … max): 0.991 s … 1.023 s 10 runs
Benchmark 2: juvix -N 4 typecheck Main.juvix
Time (mean ± σ): 1.584 s ± 0.046 s [User: 2.934 s, System: 0.149 s]
Range (min … max): 1.535 s … 1.660 s 10 runs
Benchmark 3: juvix-main typecheck Main.juvix
Time (mean ± σ): 2.066 s ± 0.010 s [User: 1.939 s, System: 0.089 s]
Range (min … max): 2.048 s … 2.077 s 10 runs
Summary
juvix -N 6 typecheck Main.juvix +RTS -A67108864 ran
1.57 ± 0.05 times faster than juvix -N 4 typecheck Main.juvix
2.05 ± 0.03 times faster than juvix-main typecheck Main.juvix
```
### Cached run (54% faster than main)
```
hyperfine --warmup 1 'juvix -N 6 typecheck Main.juvix +RTS -A33554432' 'juvix -N 4 typecheck Main.juvix' 'juvix-main typecheck Main.juvix'
Benchmark 1: juvix -N 6 typecheck Main.juvix +RTS -A33554432
Time (mean ± σ): 551.8 ms ± 13.2 ms [User: 1419.8 ms, System: 199.4 ms]
Range (min … max): 535.2 ms … 570.6 ms 10 runs
Benchmark 2: juvix -N 4 typecheck Main.juvix
Time (mean ± σ): 636.7 ms ± 17.3 ms [User: 1006.3 ms, System: 196.3 ms]
Range (min … max): 601.6 ms … 655.3 ms 10 runs
Benchmark 3: juvix-main typecheck Main.juvix
Time (mean ± σ): 847.2 ms ± 58.9 ms [User: 710.1 ms, System: 126.5 ms]
Range (min … max): 731.1 ms … 890.0 ms 10 runs
Summary
juvix -N 6 typecheck Main.juvix +RTS -A33554432 ran
1.15 ± 0.04 times faster than juvix -N 4 typecheck Main.juvix
1.54 ± 0.11 times faster than juvix-main typecheck Main.juvix
```
* Implements code generation through Rust.
* CLI: adds two `dev` compilation targets:
1. `rust` for generating Rust code
2. `native-rust` for generating a native executable via Rust
* Adds end-to-end tests for compilation from Juvix to native executable
via Rust.
* A target for RISC0 needs to be added in a separate PR building on this
one.
This PR adds support for the `String` type, String literals and string
concatenation to the Nockma backend. Support for the builtins `show` and
`intToString` is not supported.
### Example
test079.juvix
```
module test079;
import Stdlib.Prelude open;
main (s : String) : String :=
s ++str " " ++str "✨ héllo" ++str " " ++str "world ✨";
```
args.nockma
```
[quote "Juvix!"]
```
```
$ juvix compile anoma test079.juvix
$ juvix dev nockma run test079.pretty.nockma --args args.nockma
"Juvix! ✨ héllo world ✨"
```
### String representation
A String is a sequence of UTF-8 encoded bytes. We interpret these bytes
as a sequence of bits to represent the string as an integer atom in
nockma.
For example:
The string `"a"` is UTF-8 encoded as `97` which is `0b1100001` in bits.
The string `"ab"` is UTF-8 encoded at the pair of bytes: `97 98` which
is `0b1100001 0b1100010`.
When we combine the bytes into a single sequence of bits we must take
care to pad each binary representation with zeros to each byte boundary.
So the binary representation of `"ab"` as an atom is `0b110000101100010`
or `24930` as an integer atom.
### String concatenation
We use the
[cat](ea25f88cea/hoon/anoma.hoon (L215))
function in the Anoma stdlib to concatenate the bytes representing two
strings.
We need to use the block parameter `3` in the Anoma call because we want
to treat the atoms representing the strings as sequences of bytes (= 2^3
bits).
To find the relevant Nock code to call `cat` with block parameter `3` we
use the urbit dojo as follows:
```
=> anoma !=(~(cat block 3))
[8 [9 10 0 7] 9 4 10 [6 7 [0 3] 1 3] 0 2]
```
### Stdlib intercept in Evaluator
The evaluator has support for strings using `AtomHint`s, so strings can
be printed and traced. The stdlib `cat` call is also intercepted because
evaluating the unjetted hoon version is slow.
### String support in pretty nockma
In a pretty nockma file or `nock` quasi-quote you can write double
quoted string literals, e.g "abc". These are automatically translated to
UTF-8 integer atoms as in the previous section.
This PR adds support for the Anoma stdlib `sign` and `verify` APIs.
```
builtin anoma-sign
axiom anomaSign : {A : Type}
-- message to sign
-> A
-- secret key
-> Nat
-- signed message
-> Nat;
builtin anoma-verify
axiom anomaVerify : {A : Type}
-- signed message to verify
-> Nat
-- public key
-> Nat
-- message with signature removed
-> A;
```
These correspond to the
[`sign`](https://hexdocs.pm/enacl/enacl.html#sign-2) and
[`sign_open`](https://hexdocs.pm/enacl/enacl.html#sign_open-2) APIs from
libsodium respectively.
If signature verification fails in `anomaVerify`, the Anoma program
exits. We copy this behaviour in the evaluator by throwing an error in
this case.
## Notes
The Haskell Ed25519 library does not support `sign_open`. Its
verification function returns Bool, i.e it checks that the signature is
valid. The signed message is simply the concatenation of the signature
(64 bytes) and the original message so I added a function to remove the
signature from a signed message.
This PR adds support for`anomaVerifyDetached` stdlib API via a Juvix
builtin.
It has signature:
```
builtin anoma-verify-detached
axiom anomaVerifyDetached : {A : Type}
--- signature
-> Nat
--- message
-> A
--- public key
-> Nat
-> Bool;
```
The [ed25519](https://hackage.haskell.org/package/ed25519) library is
used in the evaluator becuase Anoma uses ed25519 signatures
(https://hexdocs.pm/enacl/enacl.html).
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
Similarly to how the Cairo operations are handled we add a separate Tree
language Node for Anoma operations instead of handling them as an Unop
Node.
This is necessary because we need to add support for new Anoma
operations that are not unary.
This PR also adds support for `anoma-encode` and `anoma-decode`
functions in `jvt` tree source files which was missed in the previous
PRs.
This PR adds support for the `anoma-decode` builtin
```
builtin anoma-decode
axiom anomaDecode : {A : Type} -> Nat -> A
```
Adds:
* An implementation of the `cue` function in Haskell
* Unit tests for `cue`
* A benchmark for `cue` applied to the Anoma / nockma stdlib
Benchmark results:
```
cue (jam stdlib): OK
36.0 ms ± 2.0 ms
```
Closes:
* https://github.com/anoma/juvix/issues/2764
* Closes#2763.
* Fixes a bug in the scoper, likely introduced in
https://github.com/anoma/juvix/pull/2468 by making later declarations
depend on earlier ones. The problem was that the inductive modules were
always added at the beginning of a section, which resulted in an
incorrect definition dependency graph (an inductive type depended on its
associated projections).
* Now inductive modules are added just after a group of inductive
definitions, before the next function definition. This implies that
inductive type definitions which depend on each other cannot be
separated by function definitions. Existing Juvix code needs to be
adjusted.
* The behaviour is now equivalent to "manually" inserting module
declarations with projections after each group of inductive definitions.
This PR adds support for the `anoma-encode` builtin:
```
builtin anoma-encode
axiom anomaEncode : {A : Type} -> A -> Nat
```
In the backend this is compiled to a call to the Anoma / nockma stdlib
`jam` function.
This PR also contains:
* An implementation of the `jam` function in Haskell. This is used in
the Nockma evaluator.
* Unit tests for `jam`
* A benchmark for `jam` applied to the Anoma / nockma stdlib.
Benchmark results:
```
$ juvixbench -p 'Jam'
All
Nockma
Jam
jam stdlib: OK
109 ms ± 6.2 ms
```
- Contributes to #2750
# New commands:
1. `dev import-tree scan FILE`. Scans a single file and lists all the
imports in it.
2. `dev import-tree print`. Scans all files in the package and its
dependencies. Builds an import dependency tree and prints it to stdin.
If the `--stats` flag is given, it reports the number of scanned
modules, the number of unique imports, and the length of the longest
import chain.
Example: this is the truncated output of `juvix dev import-tree print
--stats` in the `juvix-stdlib` directory.
```
[...]
Stdlib/Trait/Partial.juvix imports Stdlib/Data/String/Base.juvix
Stdlib/Trait/Partial.juvix imports Stdlib/Debug/Fail.juvix
Stdlib/Trait/Show.juvix imports Stdlib/Data/String/Base.juvix
index.juvix imports Stdlib/Cairo/Poseidon.juvix
index.juvix imports Stdlib/Data/Int/Ord.juvix
index.juvix imports Stdlib/Data/Nat/Ord.juvix
index.juvix imports Stdlib/Data/String/Ord.juvix
index.juvix imports Stdlib/Prelude.juvix
Import Tree Statistics:
=======================
• Total number of modules: 56
• Total number of edges: 193
• Height (longest chain of imports): 15
```
Bot commands support the `--scan-strategy` flag, which determines which
parser we use to scan the imports. The possible values are:
1. `flatparse`. It uses the low-level
[FlatParse](https://hackage.haskell.org/package/flatparse-0.5.1.0/docs/FlatParse-Basic.html)
parsing library. This parser is made specifically to only parse imports
and ignores the rest. So we expect this to have a much better
performance. It does not have error messages.
2. `megaparsec`. It uses the normal juvix parser and we simply collect
the imports from it.
4. `flatparse-megaparsec` (default). It uses the flatparse backend and
fallbacks to megaparsec if it fails.
# Internal changes
## Megaparsec Parser (`Concrete.FromSource`)
In order to be able to run the parser during the scanning phase, I've
adjusted some of the effects used in the parser:
1. I've removed the `NameIdGen` and `Files` constraints, which were
unused.
2. I've removed `Reader EntryPoint`. It was used to get the `ModuleId`.
Now the `ModuleId` is generated during scoping.
3. I've replaced `PathResolver` by the `TopModuleNameChecker` effect.
This new effect, as the name suggests, only checks the name of the
module (same rules as we had in the `PathResolver` before). It is also
possible to ignore the effect, which is needed if we want to use this
parser without an entrypoint.
## `PathResolver` effet refactor
1. The `WithPath` command has been removed.
2. New command `ResolvePath :: ImportScan -> PathResolver m
(PackageInfo, FileExt)`. Useful for resolving imports during scanning
phase.
3. New command `WithResolverRoot :: Path Abs Dir -> m a -> PathResolver
m a`. Useful for switching package context.
4. New command `GetPackageInfos :: PathResolver m (HashMap (Path Abs
Dir) PackageInfo)` , which returns a table with all packages. Useful to
scan all dependencies.
The `Package.PathResolver` has been refactored to be more like to normal
`PathResolver`. We've discussed with @paulcadman the possibility to try
to unify both implementations in the near future.
## Misc
1. `Package.juvix` no longer ends up in
`PackageInfo.packageRelativeFiles`.
1. I've introduced string definitions for `--`, `{-` and `-}`.
2. I've fixed a bug were `.juvix.md` was detected as an invalid
extension.
3. I've added `LazyHashMap` to the prelude. I've also added `ordSet` to
create ordered Sets, `ordMap` for ordered maps, etc.
# Benchmarks
I've profiled `juvix dev import-tree --scan-strategy [megaparsec |
flatparse] --stats` with optimization enabled.
In the images below we see that in the megaparsec case, the scanning
takes 54.8% of the total time, whereas in the flatparse case it only
takes 9.6% of the total time.
- **Megaparsec**
- **Flatparse**
## Hyperfine
```
hyperfine --warmup 1 'juvix dev import-tree print --scan-strategy flatparse --stats' 'juvix dev import-tree print --scan-strategy megaparsec --stats' --min-runs 20
Benchmark 1: juvix dev import-tree print --scan-strategy flatparse --stats
Time (mean ± σ): 82.0 ms ± 4.5 ms [User: 64.8 ms, System: 17.3 ms]
Range (min … max): 77.0 ms … 102.4 ms 37 runs
Benchmark 2: juvix dev import-tree print --scan-strategy megaparsec --stats
Time (mean ± σ): 174.1 ms ± 2.7 ms [User: 157.5 ms, System: 16.8 ms]
Range (min … max): 169.7 ms … 181.5 ms 20 runs
Summary
juvix dev import-tree print --scan-strategy flatparse --stats ran
2.12 ± 0.12 times faster than juvix dev import-tree print --scan-strategy megaparsec --stats
```
In order to compare (almost) only the parsing, I've forced the scanning
of each file to be performed 50 times (so that the cost of other parts
get swallowed). Here are the results:
```
hyperfine --warmup 1 'juvix dev import-tree print --scan-strategy flatparse --stats' 'juvix dev import-tree print --scan-strategy megaparsec --stats' --min-runs 10
Benchmark 1: juvix dev import-tree print --scan-strategy flatparse --stats
Time (mean ± σ): 189.5 ms ± 3.6 ms [User: 161.7 ms, System: 27.6 ms]
Range (min … max): 185.1 ms … 197.1 ms 15 runs
Benchmark 2: juvix dev import-tree print --scan-strategy megaparsec --stats
Time (mean ± σ): 5.113 s ± 0.023 s [User: 5.084 s, System: 0.035 s]
Range (min … max): 5.085 s … 5.148 s 10 runs
Summary
juvix dev import-tree print --scan-strategy flatparse --stats ran
26.99 ± 0.52 times faster than juvix dev import-tree print --scan-strategy megaparsec --stats
```
## Goal
The goal of this PR is to deduplicate all dependencies in a Juvix
project.
Two dependencies are __identical__ when:
* For path dependencies, their paths are equal
* For git dependencies, their URL and their resolved revision (i.e the
git revision hash after resolving a tag) are equal
For example in the following dependency tree, where each of the named
dependencies represent identical git dependencies.
```
MyPkg
|
|-- Dep1-hash1
| |
| |-- Dep2-hash2
| | |
| | `-- Stdlib-hash3
| |
| `-- Stdlib-hash3
|
|-- Dep2-hash2
| |
| `-- Stdlib-hash3
|
`-- Stdlib-hash3
```
The project `MyPkg` should just contain the following dependencies:
`Dep1-hash1, Dep2-hash2, Stdlib-hash3`.
## Design
### Storage of transitive dependencies
Currently the transitive dependencies of a project are fetched/stored in
`.juvix-build` directories of the corresponding dependencies. After this
PR all dependencies, including transitive ones are stored in the
`.juvix-build` directory of the root project.
Again, assuming that all the transitive dependencies have the same git
hash, in the file system we label the dependencies with their git hash.
```
MyPkg
|
`- .juvix-build
|- Dep1-hash1
|- Dep2-hash2
`- Stdlib-hash3
```
Say we have two versions of `Dep2` in the transitive dependency graph:
```
MyPkg
|
|-- Dep1-hash1
| |
| |-- Dep2-hash2
| | |
| | `-- Stdlib-hash3
| |
| `-- Stdlib-hash3
|
|-- Dep2-hash4
| |
| `-- Stdlib-hash3
|
`-- Stdlib-hash3
```
we would have two copies of `Dep2` in the `.juvix-build` directory with
different hashes:
```
MyPkg
|
`- .juvix-build
|- Dep1-hash1
|- Dep2-hash2
|- Dep2-hash4
`- Stdlib-hash3
```
### Storage of git clones
As a consequence of this design we cannot store the git clones for each
dependency in the `.juvix-build` directory as we do now.
We now store the git clones in a global directory
`~/.config/juvix/0.6.1/git-cache`.
When a dependency at a particular revision is required, the global git
clone is fetched/checked out at the required revision and copied into
the `.juvix-build` directory of the relevant project.
### Naming of git clones
The requirement for the naming of the global git clones is that they can
be identified by URL.
In this PR the name of a clone is formed by taking the SHA256 hash of
the dependency git URL. This is to avoid issues with file-system safe
escaping of characters.
### Naming of dependency directories
The requirement for the naming of the dependency directories is that
they can be identified by URL.
/ revision in accordance with our definition of identical dependencies.
In this PR the name of a clone is formed by taking the SHA256 hash of
the concatenation of the dependency git URL and git revision. This is to
avoid issues with file-system safe escaping of characters.
The downside of this approach is that it's hard to see which directories
correspond to which dependencies when navigating the filesystem.
However, navigating using the Juvix tooling by using go-to-definition
etc. will continue to work as before.
## Benchmarks
I tested using [`juvix-containers` test
`Main.juvix`](ebe8d2a873/test/Main.juvix).
The following benchmarks show timings excluding the initial clone of
dependencies (which happens in the warmup run).
Before:
```
$ juvix clean && juvix clean -g
$ hyperfine -w 1 'juvix compile native Main.juvix'
Benchmark 1: juvix compile native Main.juvix
Time (mean ± σ): 5.598 s ± 0.410 s [User: 5.020 s, System: 0.586 s]
Range (min … max): 5.106 s … 6.382 s 10 runs
```
After:
```
$ juvix clean && juvix clean -g
$ hyperfine -w 1 'juvix compile native Main.juvix'
Benchmark 1: juvix compile native Main.juvix
Time (mean ± σ): 4.418 s ± 0.241 s [User: 4.083 s, System: 0.343 s]
Range (min … max): 4.237 s … 4.927 s 10 runs
```
The time saved is due to the fact that before the project depends on 2
copies of the stdlib and after the project depends on 1 copy of the
stdlib.
Time is also saved in the initial run because the stdlib is only cloned
once instead of twice. The cached stdlib clone is also shared between
all project which will improve the performance of all projects that use
the stdlib.
Closes
* https://github.com/anoma/juvix/issues/2760
- Closes#2735
Allow integer literals to be expressed in different bases:
1. binary, with prefix `0b`.
2. octal, with prefix `0o`.
3. decimal, with no prefix.
4. hexadecimal, with prefix `0x`. Both capital and lower case letters
are parsed. They are always printed as lower case letters.
This applies to all languages that use integer literals, but only in the
concrete language the base will be preserved when pretty printing.
This PR adds support for the `extract-module-statements` attribute for
Juvix code blocks:
So if you write something like the following block in a Juvix markdown
file:
````
```juvix extract-module-statements
module Foo;
type T := t;
end;
```
````
The statement `type T := t;` from the body of the module is rendered in
the output. The `module Foo;` , and `end;` lines are not rendered in the
output.
A block with the `extract-module-statements` must contain a single local
module statement and nothing else. An error is reported if this is not
the case.
The `extract-module-statements` attribute also takes an optional
argument. It sets the number of statements from the module body to drop
from the output.
In the following example, the output will contain the single line `a : T
:= t;`.
````
```juvix extract-module-statements 1
module Foo;
type T := t;
a : T := t;
end;
```
````
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
- refactor `--target` into subcommands for `dev tree compile`.
- prepend `App` to all `CompileTarget` constructors to avoid name
clashes with `Target`.
- parameterize compile options type with the input kind. The input kind
indicates the expected file extension of the input file. If the input
file is a .juvix file, then it is optional, otherwise it is mandatory.
- Add `AppError MegaparsecError` instance and simplify some related
code.
# Changes
The main goal of this pr is to remove the `--target` flag for `juvix
compile` and use subcommands instead. The targets that are relevant to
normal users are found in `juvix compile --help`. Targets that are
relevant only to developers are found in `juvix dev compile --help`.
Below I list some of the changes in more detail.
## Compile targets for user-facing languages
- `juvix compile native`
- `juvix compile wasi`. I wasn't sure how to call this: `wasm`,
`wasm32-wasi`, etc. In the end I thought `wasi` was short and accurate,
but we can change it.
- `juvix compile vampir`
- `juvix compile anoma`
- `juvix compile cairo`
## *New* compile targets for internal languages
See `juvix dev compile --help`.
1. `dev compile core` has the same behaviour as `dev core
from-concrete`. The `dev core from-concrete` is redundant at the moment.
2. `dev compile tree` compiles to Tree and prints the InfoTable to the
output file wihout any additional checks.
3. `dev compile reg` compiles to Reg and prints the InfoTable to the
output file wihout any additional checks.
4. `dev compile asm` compiles to Asm and prints the InfoTable to the
output file wihout any additional checks.
5. 4. `dev compile casm` compiles to Asm and prints the Result to the
output file wihout any additional checks. TODO: should the Result be
printed or something else? At the moment the Result lacks a pretty
instance.
6.
## Optional input file
1. The input file for commands that expect a .juvix file as input is now
optional. If the argument is ommited, he main file given in the
package.yaml will be used. This applies to the following commands:
1. `juvix compile [native|wasi|geb|vampir|anoma|cairo]`
8. `juvix dev compile [core|reg|tree|casm|asm]`
1. `juvix html`
3. `juvix markdown`.
4. `juvix dev internal [typecheck|pretty]`.
5. `juvix dev [parse|scope]`
7. `juvix compile [native|wasi|geb|vampir|anoma|cairo]`
9. note that `juvix format` has not changed its behaviour.
## Refactor some C-like compiler flags
Both `juvix compile native` and `juvix compile wasi` support `--only-c`
(`-C`), `--only-preprocess` (`-E`), `--only-assemble` (`-S`). I propose
to deviate from the `gcc` style and instead use a flag with a single
argument:
- `--cstage [source|preprocess|assembly|exec(default)]`. I'm open to
suggestions. For now, I've kept the legacy flags but marked them as
deprecated in the help message.
## Remove code duplication
I've tried to reduce code duplication. This is sometimes in tension with
code readability so I've tried to find a good balance. I've tried to
make it so we don't have to jump to many different files to understand
what a single command is doing. I'm sure there is still room for
improvement.
## Other refactors
I've implemented other small refactors that I considered improved the
quality of the code.
## TODO/Future work
We should refactor commands (under `compile dev`) which still use
`module Commands.Extra.Compile` and remove it.
* Closes#2687
* Adds hint support in CASM. The supported hints are `Input(var)` and
`Alloc(size)`. These are the hints currently implemented in
[juvix-cairo-vm](https://github.com/anoma/juvix-cairo-vm).
* Adds the `--program_input` option to the `juvix dev casm run` command.
* Enables private inputs via `main` arguments. In generated CASM/Cairo
code, the arguments to `main` are fetched using the `Input` hint.
* Modifies the CI to use
[juvix-cairo-vm](https://github.com/anoma/juvix-cairo-vm)
This PR implements changes to make the `eval` command and internal
development commands fully Cairo-compatible.
* Change the default field size to Cairo field size
* Change the printing of "negative" field elements to be compatible with
the Cairo VM
* Quote function names in the Reg to CASM translation
Cairo VM imposes restrictions on memory access order stricter than
described in the documentation, which necessitates changing the
compilation concept for local variables.
Summary
-------------
To ensure that memory is accessed sequentially at all times, we divide
instructions into basic blocks. Within each basic block, the `ap` offset
(i.e. how much `ap` increased since the beginning of the block) is known
at each instruction, which allows to statically associate `fp` offsets
to local variables while still generating only sequential assignments to
`[ap]` with increasing `ap`. When the `ap` offset can no longer be
statically determined for new local variables (e.g. due to an
intervening recursive call), we switch to the next basic block by
calling it with the `call` instruction. The arguments of the basic block
call are the variables live at the beginning of the called block. Note
that the `fp` offsets of "old" variables are still statically determined
even after the current `ap` offset becomes unknown -- the arbitrary
increase of `ap` does not influence the previous variable associations.
Hence, we can transfer the needed local variables to the next basic
block.
Example
-----------
The JuvixReg function
```
function f(integer) : integer {
tmp[0] = add arg[0] 1;
tmp[1] = call g(tmp[0]);
tmp[2] = add tmp[1] arg[0];
tmp[3] = mul tmp[2] 2;
tmp[4] = call g(tmp[2]);
tmp[5] = add tmp[4] tmp[3];
ret tmp[5];
}
```
is compiled to
```
f:
-- code for basic block 1
[ap] = [fp - 3] + 1; ap++
-- now [fp] is tmp[0], because fp = ap at function start (ap offset is zero)
-- transfer call argument (in this case, could be optimized away)
[ap] = [fp]; ap++
call g
-- now [ap - 1] contains the result tmp[1] (it is already a call argument now)
-- we additionally transfer arg[0] which is live in the next block
[ap] = [fp - 3]; ap++
call rel 3
ret
nop
-- code for basic block 2
-- the above "call rel" jumps here
-- [fp - 4] is tmp[1]
-- [fp - 3] is arg[0]
[ap] = [fp - 4] + [fp - 3]; ap++
-- now [fp] is tmp[2]
[ap] = [fp] * 2; ap++
-- now [fp + 1] is tmp[3]
[ap] = [fp]; ap++
call g
-- now [ap - 1] is tmp[4]
[ap] = [fp + 1]; ap++
call rel 3
ret
nop
-- code for basic block 3
-- [fp - 4] is tmp[4]
-- [fp - 3] is tmp[3]
[ap] = [fp - 4] + [fp - 3]; ap++
-- now [fp] is tmp[5]
-- the next assignment could be optimized away in this case
[ap] = [fp]; ap++
ret
```
There are three basic blocks separated by the `call` instructions. In
each basic block, we know statically the `ap` offset at each instruction
(i.e. how much `ap` increased since the beginning of the block). We can
therefore associate the temporary variables with `[fp + k]` for
appropriate `k`. At basic block boundaries we transfer live temporary
variables as arguments for the call to the next basic block.
Checklist
------------
- [x] Divide JuvixReg instructions into [basic
blocks](https://en.wikipedia.org/wiki/Basic_block).
- [x] Implement liveness analysis for each basic block.
- [x] Translate transitions between basic blocks into CASM relative
calls with local live variable transfer.
- [x] Tests for the translation from JuvixReg to Cairo bytecode executed
with the Cairo VM
* Closes#2563
Checklist
------------
- [x] Serialization of the Haskell CASM representation to the JSON
format accepted by the Cairo VM.
- [x] Add the `cairo` target to the `compile` commands.
- [x] Output via the Cairo `output` builtin.
- [x] Relativize jumps. Cairo VM doesn't actually support absolute
jumps.
- [x] Test the translation from CASM to Cairo by running the output in
the Cairo VM
- [x] Add Cairo VM to the CI
When we first implemented the Nockma backend we wrongly assumed that the
only entry point for Juvix compiled Nockma modules would be the main
function. Using this assumption we could add a setup step in the main
function that put the Anoma stdlib and compiled functions from the Juvix
module in a static place in the Nockma subject. References to the Anoma
stdlib and functions in the module could then be resolved statically.
However, one of the use cases for Juvix -> Nockma compilation is for
Anoma to run logic functions that are fields of a transaction. So the
user writes a Juvix program with main function that returns a
transaction. The result of the main function is passed to Anoma. When
Anoma calls the logic function on a field of the transaction, the setup
part of the main function is not run so the subject is not in the
required state. In fact, the logic function is not even callable by
Anoma because non-main functions in the Juvix module use a calling
convention that assumes the subject has a particular shape.
This PR solves the problem by making all functions in the Juvix module
use the Anoma calling convention. We make all compiled closures
(including, for example, the logic functions stored on resources in a
transaction) self contained, i.e they contain the functions library and
anoma standard library.
Modules that contain many closures produce large nockma output files
which slows down the evaluator. This will need to be fixed in the future
either with Nockma compression ([jam
serialization](https://developers.urbit.org/reference/hoon/stdlib/2p))
or otherwise. But it does not block the compilation and execution of
Anoma transactions.
Other fixes / additions:
* Extra tracing. You can now annotate output cells with a tag that will
be displayed in the output
* Unittests for listToTuple, appendRights helper functions
* Fixes for the nockma parser when parsing 'pretty nockma', specifically
stdlib calls, tags and functions_library atom.
* Adds `juvix dev nock run` command that can run a program output with
the `anoma` target.
* Remove the `nockma` target. As described above we always use the Anoma
calling convention so there's no need for a separate target for the
'juvix calling convention'
* Adds a `--profile` flag to `juvix dev nock run` which outputs a count
of Nockma ops used in the evaluation
* In tests we no longer serialise the compiled program to force full
evaluation of the compiled code. We added a negative test to check that
strings are not allowed in Nockma/Anoma programs,
it is output in a file `OUTPUT.profile` and has the following form:
```
quote : 15077
apply : 0
isCell : 0
suc : 0
= : 4517
if : 5086
seq : 5086
push : 0
call : 4896
replace : 1
hint : 8
scry : 0
trace : 0
```
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
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](https://github.com/anoma/juvix/issues/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 https://github.com/anoma/juvix/issues/2672
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
* Closes#2562
Checklist
---------
- [x] Translation from JuvixReg to CASM
- [x] CASM runtime
- [x] Juvix to CASM pipeline: combine the right transformations and
check prerequisites
- [x] CLI commands: add target `casm` to the `compile` commands
- [x] Tests:
- [x] Test the translation from JuvixReg to CASM
- [x] Test the entire pipeline from Juvix to CASM
This PR adds some flags to tune the (html/md) output.
For Markdown subcommand:
```
--strip-prefix ARG Strip the given prefix from the input file path for
HTML hyperlinks
--folder-structure Generate HTML following the module's folder structure
```
For HTML subcommand, we have the ones above plus the following:
```
--ext ARG File extension in hyperlinks for the input file
(default: ".html")
```
* Closes#2571
* It is reasonable to finish this PR before tackling #2562, because the
field element type is the primary data type in Cairo.
* Depends on #2653
Checklist
---------
- [x] Add field type and operations to intermediate representations
(JuvixCore, JuvixTree, JuvixAsm, JuvixReg).
- [x] Add CLI option to choose field size.
- [x] Add frontend field builtins.
- [x] Automatic conversion of integer literals to field elements.
- [x] Juvix standard library support for fields.
- [x] Check if field size matches when loading a stored module.
- [x] Update the Cairo Assembly (CASM) interpreter to use the field type
instead of integer type.
- [x] Add field type to VampIR backend.
- [x] Tests
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
Builtin information needs to be propagated from stored modules to REPL
artifacts to avoid "The builtin _ has not been defined" errors.
This PR adds a test suite for the REPL in the Haskell test code. This
means some of the slow smoke tests can be moved to fast haskell unit
tests. In future we should refactor the REPL code by putting in the main
src target and unit testing more features (e.g :doc, :def).
* Closes https://github.com/anoma/juvix/issues/2638
* Closes https://github.com/anoma/juvix/issues/2664
As well as this fix we rename lens scopedIdenName to scopedIdenSrcName.
`scopedIdenSrcName` refers to the name of an identifier from the source
code. The name `scopedIdenName` is confusing because users of
`ScopedIden` may think that this lens refers to the only name associated
with `ScopedIden`, they may want `scopedIdenNameFinal` instead.
This PR adds a `anoma` target to the `juvix compile`. This target
compiles a Juvix `main` function to a Nockma/Anoma "function". Unlike
the native, wasm, and nockma targets the main function may have any type
signature.
## Anoma calling convention
[Anoma calls
functions](6a4e15fe9c/lib/anoma/resource.ex (L122))
by evaluating the formula `[call L replace [RL args] @ S]` against a
subject equal to the function. Here `args` is a Nockma term that
evaluates to a tuple of arguments that should be passed to the function.
The anoma target compiles the `main` function to Nockma in the same way
as the nockma target. The main function is then
[wrapped](9a658465ae/src/Juvix/Compiler/Nockma/Translation/FromTree.hs (L627))
to make it compatible with the Anoma calling convention.
## Testing
The anoma calling convention is [unit
tested](9a658465ae/test/Nockma/Eval/Positive.hs (L117))
and [smoke
tested](9a658465ae/tests/smoke/Commands/compile.smoke.yaml (L159)).
This PR also adds versions of the end-to-end compilation tests. Most
tests are included, tests for builtin IO operations and string builtins
are omitted. Other tests that use Strings have been adapted to use other
types that are compatible with this backend.
## Nockma REPL
To facilitate testing the Nockma REPL can now load a nockma file as an
initial subject.
---------
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
* Closes#2560
* Adds a transformation of JuvixReg into SSA form.
* Adds an "output variable" field to branching instructions (`Case`,
`Branch`) which indicates the output variable to which the result is
assigned in both branches. The output variable corresponds to top of
stack in JuvixAsm after executing the branches. In the SSA
transformation, differently renamed output variables are unified by
inserting assignment instructions at the end of branches.
* Adds tests for the SSA transformation.
* Depends on #2641.
This pr addresses a number of problems.
1. It fixes a bug where paths were annotated as operations rather than
paths in the parser.
2. It fixes a bug that happened when unfolding cells in the pretty
printer in order to minimize delimiters. It caused the stdlibcall hints
to be ignored for the unfolded arguments.
3. In order to properly test this, we can't ignore the hints for the Eq
instance, so I've changed that.
4. I've introduced the class NockmaEq for nockma semantic equality. This
is used in the evaluator as well as in the semantic tests.
5. I've added a bigger test. I found these bugs while working with this
file.
* Closes#2578
* Implements JuvixReg parser and pretty printer.
* Adds the `juvix dev reg read file.jvr` command.
* Adds the `reg` target to the `compile` commands.
* Adds tests for the JuvixReg parser.
This PR replaces the JuvixAsm -> Nockma translation with a JuvixTree ->
Nockma translation.
We can now enable some of the JuvixTree tests that did not work with
JuvixAsm->Nockma because they were too slow.
## Notes
We have changed [test031: temp stack with
branching](22ee87f0e7/tests/Tree/positive/test031.jvt)
to avoid using negative numbers (because negative integers are not
supported in Nockma).
Three tree tests trace/output lists. Lists are serialised differently by
the asm and nockma pretty printers so they cannot share a single test
output file. We have created separate nockma output files for these
tests (see eg.
[test028.nockma.out](22ee87f0e7/tests/Tree/positive/out/test028.nockma.out)).
* Closes https://github.com/anoma/juvix/issues/2606
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
Co-authored-by: Lukasz Czajka <lukasz@heliax.dev>
* Adds negative tests for the JuvixTree evaluator
* Depends on #2600
* Depends on #2599
* Depends on #2598
* Depends on #2597
* Depends on #2596
* Depends on #2595
* Depends on #2594
* Depends on #2590
This PR fixes an issue with importing `syntax alias` and using them from
another module:
Say you have a module defining a syntax alias:
```
module SyntaxAlias;
import Stdlib.Prelude open;
syntax alias MyNat := Nat;
```
and another which imports / uses it:
```
module test073;
import SyntaxAlias open;
main : MyNat := 11;
```
The compiler crashed with the following error:
```
^?!): empty Fold
CallStack (from HasCallStack):
error, called at src/Lens/Micro.hs:711:28 in microlens-0.4.13.1-ARwI8t2x86cAxRs56XPcG1:Lens.Micro
^?!, called at src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs:565:29 in juvix-0.5.5-G7jC6MbkbsJGkMT9u4BkYQ:Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping
```
We fix this by adding the aliases to the store's [scoper info
table](6649209d26/src/Juvix/Compiler/Store/Scoped/Data/InfoTable.hs (L14))
and then use it to initialise the scoper state when scoping a module.
* Adds smoke tests for `juvix dev tree` CLI commands.
* Fixes a bug with printing JuvixAsm.
* Depends on #2597
* Depends on #2596
* Depends on #2595
* Depends on #2594
* Depends on #2590
* Adds the `FilterUnreachable` transformation in JuvixTree.
* Depends on #2596
* Depends on #2595
* Depends on #2594
* Depends on #2590
* Depends on #2589
* Depends on #2587
* Implements a translation from JuvixAsm to JuvixTree. It does not work
in general, but works for all code generated from Juvix and all JuvixAsm
tests.
* Adds the `juvix dev tree from-asm` command.
* Adds tests automatically converted from JuvixAsm tests.
* Depends on #2583
This PR implements:
* JuvixTree parser.
* JuvixTree pretty printer.
* `juvix dev tree read file.jvt` command which reads and pretty prints a
JuvixTree file.
* The `tree` target in the `compile` command.
* Removal of `StackRef` in JuvixAsm. This makes JuvixAsm more consistent
with JuvixTree and simplifies the data structures. `StackRef` is not
needed for compilation from Core.
Tests for the parser will appear in a separate PR, when I implement an
automatic translation of JuvixAsm to JuvixTree files.
---------
Co-authored-by: Paul Cadman <git@paulcadman.dev>
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
