* 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#2827
* Adds an optimization phase to the JuvixReg -> Casm pipeline, which
consists of repeated copy & constant propagation and dead code
elimination.
* 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`.
* 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 implements generic support for Cairo VM builtins. The calling
convention in the generated CASM code is changed to allow for passing
around the builtin pointers. Appropriate builtin initialization and
finalization code is added. Support for specific builtins (e.g. Poseidon
hash, range check, Elliptic Curve operation) still needs to be
implemented in separate PRs.
* Closes#2683
* 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
See test failure:
https://github.com/anoma/juvix/actions/runs/8466758094/job/23196216342
```
Test030: Ackermann function (higher-order definition): FAIL (7.40s)
Translate to JuvixCore (6.92s)
Translate to CASM (0.06s)
Pretty print (0.15s)
Interpret (0.12s)
Compare expected and actual program output
Check run_cairo_vm.sh is on path
Serialize to Cairo bytecode
Run Cairo VM (0.14s)
/tmp/tmp-60ba562ca9d8f9b5: changeWorkingDirectory: does not exist (No such file or directory)
Use -p '/Juvix to CASM positive tests (no optimization).Test030: Ackermann function (higher-order definition)/' to rerun this test only.
```
`setCurrentDir` cannot be used because tests are run at the same time on
different threads.
This PR removes `setCurrentDir` and instead passes the CWD directly to
the `proc` call.
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
* 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
* 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>
Now the prelude exports this function:
```
readFile :: (MonadIO m) => Path Abs File -> m Text
readFile = liftIO . Utf8.readFile . toFilePath
```
It is more convenient to use because it uses typed `Path` and works in
any `MonadIO`.
This PR contains refactors split out from the Nockma compile PR
https://github.com/anoma/juvix/pull/2570. Each refactor is associated
with a separate commit in this PR.
* Closes#2561
* Defines an extended subset of Cairo Assembly, following Section 5 of
[1].
* Adds the commands `juvix dev casm read file.casm` and `juvix dev casm
run file.casm` to print and run `*.casm` files.
* The tests cover CASM semantics. Some are "manual translations" of
corresponding JuvixAsm tests according to the JuvixAsm -> CASM
compilation concept.
