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
`just install` now builds the optimized binary by default.
use `just disableOptimized=yes install` to build the non-optimized
binary (with faster build time).
This pr refactors the `Input` effect. It is now meant to be used with
finite input lists.
It also introduces the `StreamOf` effect, which is meant to be used for
infinite supplies.
Both have static implementations so they should add negligible overhead
when used.
* 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
```
This PR updates the Anoma nockma stdlib to the version in Anoma 0.13.0
obtained from:
*
1bbaf664ad/lib/nock.ex (L433)
NB: As is documented in the code, the standard library paths are
obtained by running commands in the urbit dojo against the loaded
stdlib. For example to find the path to the `dec` function in the stdlib
run:
```
~zod:dojo> => anoma !=(dec)
[9 342 0 31]
```
Part of:
* https://github.com/anoma/juvix/issues/2764
- 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
The numParallelJobs option on the `justfile` is used to control the
total amount of concurrency when running build commands. This PR adds
this number to the test runner command: `+RTS -N$numParallelJobs -RTS`.
This means that `$numParallelJobs` threads will be used by the test
runner.
NB: ``+RTS -N -RTS` means that tests will use the number of threads
equal to the number of CPUs on the machine.
This PR delays running of the pipeline `MCache` (renamed to
`ModuleInfoCache`) to allow this cache to be shared between pipeline
runs in `processRecursiveUpToTyped`. `processRecursiveUpToTyped` is used
by the `juvix html` command to recursively build HTML for modules in a
project.
* Closes https://github.com/anoma/juvix/issues/2744
## Performance
The docs build is now much faster and takes much less memory:
Before:
```
$ /usr/bin/time -lh juvix html docs/index.juvix.md
1m17.41s real 35.39s user 11.42s sys
5918703616 maximum resident set size
0 average shared memory size
0 average unshared data size
0 average unshared stack size
3665213 page reclaims
697 page faults
0 swaps
0 block input operations
0 block output operations
0 messages sent
0 messages received
0 signals received
114533 voluntary context switches
81450 involuntary context switches
595152097097 instructions retired
143688878963 cycles elapsed
19323983744 peak memory footprint
```
After:
```
$ /usr/bin/time -lh juvix html docs/index.juvix.md
8.35s real 5.76s user 0.62s sys
2992160768 maximum resident set size
0 average shared memory size
0 average unshared data size
0 average unshared stack size
221870 page reclaims
719 page faults
0 swaps
0 block input operations
0 block output operations
0 messages sent
0 messages received
0 signals received
1965 voluntary context switches
1962 involuntary context switches
93909891240 instructions retired
19317129226 cycles elapsed
2963053632 peak memory footprint
```
## Notes
* `MCache` is renamed to `ModuleInfoCache`
* `ModuleInfoCache` must be defined in a separate module instead of
being defined in `Compiler.Pipeline.Driver` to avoid a cyclic
dependency. `ModuleInfoCache` is now used used in
`Juvix.Compiler.Pipeline` (in `PipelineEff`) and this module is imported
by `Juvix.Compiler.Pipeline.Driver`).
This PR updates the macOS CI build to use the `macos-14` build agent.
This uses the M series aarch64 chips.
* The M1 macOS agent does not have stack preinstalled so we must install
it using brew before building anything.
* The cache keys must have the `runner.arch` prefix to avoid building
with the x86_64 cache.
The macOS build / test run in about the same time as the linux build /
test, i.e significantly faster than on the x86 macOS agents.
## Notes
* We use the x86_64 binary of vamp-ir because the vamp-ir aarch64
releases do not have names that are compatible with the GitHub action we
are using to download the binary releases. The x86_64 binary works fine
for the purposes of testing.
- 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.
The judoc examples feature is currently unused. This feature was added
in https://github.com/anoma/juvix/pull/1442
Keeping support for this feature adds a cost to HTML generation. We are
removing this to improve the performance of `juvix html`.
To just render the HTML documentation we only require the scoper result
from the pipeline. To support the examples we need the type checking
result. The cost is significant in larger projects as the pipeline is
run for each import.
Part of https://github.com/anoma/juvix/issues/2744
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>
This PR changes the CI build to use the justfile instead of the Makefile
to run builds and tests. CI builds now take advantage of parallel module
builds from https://github.com/anoma/juvix/pull/2729.
In order support this the runtime build target in the justfile now
supports `runtimeCcArg` and `runtimeLibtoolArg` so that the `CC` and
`LIBTOOL` Makefile argument can be set. This is required for the macOS
build.
In addition this PR upgrades the stack setup step action. Previously the
stack build flags included `--fast` which meant the whole project was
rebuilt in the `test` step, this has also been fixed.
Overall this speeds up the CI:
* Linux now takes 30mins (from 40mins)
* macOS now takes 60mins (from 80mins)
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
- 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.
Thanks to @janmasrovira for figuring out that the stack
`--ghc-options=-j` flag enables [parallel module compilation in
GHC](https://downloads.haskell.org/ghc/latest/docs/users_guide/using.html#using-ghc-make).
This PR adds support for this in the project justfile.
You can configure the argument to `-j` using the `numParallelJobs`
option, for example:
```
just numParallelJobs=24 build
+ stack build --fast -j24 --ghc-options=-j24
```
If `numParallelJobs` is not set then `-j` is passed with no arguments in
`--ghc-options` (this is equivalent to passing the number of cpus of the
machine.) and is passed with the number of cpus of the machine for the
stack `-j` option (the stack `-j` option requires an argument).
The `numParallelJobs` option also sets the argument to the [stack `-j`
option](https://docs.haskellstack.org/en/stable/global_flags/#-jobs-or-j-option).
To disable build parallelism set the `disableParallel` flag:
```
just disableParallel=yes build
+ stack build --fast
```
Implements a disassembler which converts Cairo bytecode into textual
CASM representation. Useful for debugging the Cairo backend.
* Adds the `juvix dev casm from-cairo` command
The `--target` flag was replaced by subcommands in
https://github.com/anoma/juvix/pull/2700
This PR fixes the benchmark suite to use `juvix compile native` and
`juvix compile wasi`.
In addition this PR adds as `compile-only` target to `juvix-bench`
The compile-only target only compiles the executable for each variant of
each suite. It doesn't actually run the benchmarks. This is useful when
checking that the variant build steps are correct before committing.
Example to run with stack:
```
stack bench --ba 'compile-only'
```
In the nockma compilation backend we compile functions with a an atom
with hint `functionsPlaceholder` where the functions library is expected
to be. After the module is compiled we now have the functions library to
substitute.
The __first substitution__ replaces the `functionsPlaceholder` in the
main function with the functions library.
This PR introduces a __second substitution__ that replaces the
`functionsPlaceholder` atoms in the functions library that were
introduced in the __first subsitution__.
This fix is sufficient to get the [transaction
example](https://github.com/anoma/juvix-anoma/blob/main/examples/CounterTransaction.juvix)
running in the Anoma system.
Each commit in this PR is a separate improvement.
* Tag any Term with a string instead of just cells using `@`. e.g
`"myTag" @ opCall ...`
* `:dump FILE` in the nockma REPL to dump the last REPL result to a
file.
* More tagging in the pretty nockma output.
# 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
The purpose of this PR is to wrap the compiled main function with Nockma
code that captures the argument tuple for use when compiling `anomaGet`
calls.
* The [Anoma system
expects](c7f2d69d1e/lib/anoma/node/executor/worker.ex (L20))
to receive a function of type `ScryId -> Transaction`
* The ScryId is only used to construct the argument to the Scry
operation (i.e the anomaGet builtin in the Juvix frontend),
* When the Juvix developer writes a function to submit to Anoma they use
type `() -> Transaction`, the main function wrapper is used to capture
the ScryId argument into the subject which is then used to construct
OpScry arguments when anomaGet is compiled.
* If the Anoma system expectation changes then the wrapper code must be
changed.
We could add a transformation that checks that the main function in the
Anoma target has no arguments. However it is convenient to be able to
write functions with arguments for testing and debugging (for example
compiling directly to a logic function).
---------
Co-authored-by: Jan Mas Rovira <janmasrovira@gmail.com>
This PR modifies the CI manifest to cache the `cairo-vm-cli` executable
so we don't have to rebuild it on each run.
The ref of the cairo-vm repo is pinned to
`42e04161de82d7e5381258def4b65087c8944660` which is currently the HEAD
ref of the repository. This can be changed in the CI manifest by editing
the `CAIRO_VM_VERSION` variable. Doing so will trigger a rebuild of
`cairo-vm-cli`.
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
