This PR updates the version of `cargo-risczero` in the CI. Ultimately,
we should figure out how to properly pin a fixed version, but apparently
that's not easy - it seems some dependencies need to be pinned and it's
not clear which ones, how, and to which versions. The problem is that to
execute the Rust code generated for RISC0 we need to compile it, and the
generated code depends on some RISC0-related libraries. Having the
correct version of the RISC0 Rust toolchain installed locally doesn't
fully solve the problem (doesn't seem to automatically select the right
versions of dependencies).
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.
This pr modifies the `HasExpressions` class to allow traversing direct
subexpressions rather than only leaf expressions. I've added the `lens`
library as a dependency to have access to generic traversals defined in
[Control.Lens.Plated](https://hackage.haskell.org/package/lens-5.3.2/docs/Control-Lens-Plated.html).
- 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.
This PR updates the juvix-stdlib submodule ref to point to the current
main ref of the juvix-stdlib repository.
Previously it was pointing to the ref of a branch.
Currently formatting a project is equivalent to running `juvix format`
on each individual file. Hence, the performance is quadratic wrt the
number of modules in the project. This pr fixes that and we now we only
process each module once.
# Benchmark (1236% faster 🚀)
Checking the standard library
```
hyperfine --warmup 1 'juvix format --check' 'juvix-main format --check'
Benchmark 1: juvix format --check
Time (mean ± σ): 450.6 ms ± 33.7 ms [User: 707.2 ms, System: 178.7 ms]
Range (min … max): 396.0 ms … 497.0 ms 10 runs
Benchmark 2: juvix-main format --check
Time (mean ± σ): 6.019 s ± 0.267 s [User: 9.333 s, System: 1.512 s]
Range (min … max): 5.598 s … 6.524 s 10 runs
Summary
juvix format --check ran
13.36 ± 1.16 times faster than juvix-main format --check
```
# Other changes:
1. The `EntryPoint` field `entryPointModulePath` is now optional.
2. I've introduced a new type `TopModulePathKey` which is analogous to
`TopModulePath` but wihout location information. It is used in hashmap
keys where the location in the key is never used. This is useful as we
can now get a `TopModulePathKey` from a `Path Rel File`.
3. I've refactored the `_formatInput` field in `FormatOptions` so that
it doesn't need to be a special case anymore.
4. I've introduced a new effect `Forcing` that allows to individually
force fields of a record type with a convenient syntax.
5. I've refactored some of the constraints in scoping so that they only
require `Reader Package` instead of `Reader EntryPoint`.
6. I've introduced a new type family so that local modules are no longer
required to have `ModuleId` from their type. Before, they were assigned
one, but it was never used.
# Future work:
1. For project-wise formatting, the compilation is done in parallel, but
the formatting is still done sequentially. That should be improved.
* Closes#2394
* Removes the use of Uniplate in `letFunctionDefs` altogether, in favour
of handwritten traversal accumulating let definitions (implemented via
the new `HasLetDefs` typeclass).
Benchmark results
------------------
Using Uniplate:
```
heliax@imac bench % hyperfine --prepare 'juvix clean --global' -w 1 'juvix typecheck bench.juvix -N 1'
Benchmark 1: juvix typecheck bench.juvix -N 1
Time (mean ± σ): 1.399 s ± 0.023 s [User: 1.346 s, System: 0.041 s]
Range (min … max): 1.374 s … 1.452 s 10 runs
```
Using `HasLetDefs`:
```
heliax@imac bench % hyperfine --prepare 'juvix clean --global' -w 1 'juvix typecheck bench.juvix -N 1'
Benchmark 1: juvix typecheck bench.juvix -N 1
Time (mean ± σ): 1.098 s ± 0.015 s [User: 1.047 s, System: 0.040 s]
Range (min … max): 1.074 s … 1.120 s 10 runs
```
So it's roughly 1.1s vs. 1.4s, faster by 0.2s. About 14% improvement.
The benchmark file just imports the standard library:
```
module bench;
import Stdlib.Prelude open;
main : Nat := 0;
```
Both `juvix` binaries were compiled with optimizations, using `just
install`.
* 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#2745
* Adds inlining of immediate values, i.e., values that don't require
computation or memory allocation.
* Non-immediate zero-argument functions / values should not be inlined,
because when not inlined they can be computed only once.
The stdlib composition function `∘` has fixity `composition` which means
it is right associative.
We will rename `∘` to `<<` in the stdlib and add a new function:
```
>> {a b c} : (a -> b) -> (b -> c) -> a -> c
```
for consistency with `<<` this should be left associative.
This is not a breaking change to package-base so we don't need to
increment the version number.
* 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).
- Closes#2800
I've added a field `_nameKindPretty :: NameKind` that is used to store
the nameKind which should be used when highlighting and printing.
There is no need for pragmas as we can set a color for each builtin
axiom statically in the haskell code.
I've also removed the fields `_infoHighlightDoc :: DocTable` and
`_infoHighlightNames :: [S.AName]` from the
`Store/Scoped/Data/InfoTable` as they were never being read.
* 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`.
I didn't release 0.6.2 last week, but we can do it now. I've updated the
CHANGELOG with the work we did last week.
Other release changes for 0.6.2 were done in
https://github.com/anoma/juvix/pull/2795
It's failing because of rate limits exceeded when installing RISC0 VM.
We should disable the macOS CI until we figure out how to reliably get
around this problem.
* 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).
* Closes#2689
* Adds the command `juvix isabelle program.juvix` which translates a
given file to an Isabelle/HOL theory.
* Currently, only a single module is translated.
* By default translates types and function signatures. Translating
function signatures can be disabled with the `--only-types` option.
Blocked by:
- https://github.com/anoma/juvix/issues/2763
---------
Co-authored-by: Jonathan Cubides <jonathan.cubides@uib.no>
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.
