1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-03 09:41:10 +03:00
juvix/test
Paul Cadman 8d03ac2b6c
Add anoma-bytearray-{to, from}-anoma-contents builtins (#2960)
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;
```
2024-08-19 11:19:26 +02:00
..
Anoma Add anoma-bytearray-{to, from}-anoma-contents builtins (#2960) 2024-08-19 11:19:26 +02:00
Asm Refactor pipeline functions for tests (#2864) 2024-06-28 12:15:51 +02:00
BackendMarkdown Improve performance of formatting a project (#2863) 2024-07-01 18:05:24 +02:00
Casm Add precondition to run tests (#2887) 2024-07-15 10:02:48 +02:00
Compilation Fix inference of let and letrec in core (#2953) 2024-08-14 15:15:49 +01:00
Core Fix inference of let and letrec in core (#2953) 2024-08-14 15:15:49 +01:00
Examples Run test suite in parallel (#2507) 2023-11-16 16:19:52 +01:00
Formatter Improve performance of formatting a project (#2863) 2024-07-01 18:05:24 +02:00
Internal Bugfix: modules associated with inductive types should be declared after their inductive types (#2768) 2024-05-14 19:32:22 +02:00
Isabelle Translate function bodies to Isabelle/HOL (#2868) 2024-07-19 08:40:07 +01:00
Nockma Use ByteArray for Anoma cryptographic builtins (#2947) 2024-08-13 13:17:57 +01:00
Package Parallel pipeline (#2779) 2024-05-31 12:41:30 +01:00
Parsing Fix typos (#2573) 2024-01-08 13:27:18 +01:00
Reg Dead code elimination in JuvixReg (#2835) 2024-06-24 13:56:50 +02:00
Repl Improve performance of formatting a project (#2863) 2024-07-01 18:05:24 +02:00
Resolver Fix typos (#2573) 2024-01-08 13:27:18 +01:00
Runtime Rust backend (#2787) 2024-05-29 13:34:04 +02:00
Rust Add support for unsigned 8-bit integer type Byte (#2918) 2024-08-02 07:43:24 +01:00
Scope Fix scanning of names with import prefix (#2929) 2024-07-31 10:02:38 +02:00
Termination Fix typos (#2573) 2024-01-08 13:27:18 +01:00
Tree Add builtin ByteArray type (#2933) 2024-08-13 11:13:27 +01:00
Typecheck Fixes crash when trying to normalize case expression (#2811) 2024-06-07 15:43:50 +02:00
VampIR Add precondition to run tests (#2887) 2024-07-15 10:02:48 +02:00
Anoma.hs Support compilation to Anoma compatible functions (#2652) 2024-02-23 12:54:22 +00:00
Asm.hs Translation from JuvixAsm to C (#1619) 2022-12-06 11:33:20 +01:00
BackendMarkdown.hs Add MarkdownInfo entry in Module Concrete Decl and proper errors (#2515) 2023-11-16 11:20:34 +01:00
Base.hs Logger (#2908) 2024-07-22 17:14:37 +02:00
Casm.hs Add precondition to run tests (#2887) 2024-07-15 10:02:48 +02:00
Compilation.hs Remove old typechecker (#2545) 2023-12-01 16:50:37 +01:00
Core.hs Implement core transformation let-hoisting (#2076) 2023-05-16 13:42:44 +02:00
Examples.hs Add a test suite for milestone examples (#1920) 2023-03-24 13:16:26 +00:00
Format.hs Improve performance of formatting a project (#2863) 2024-07-01 18:05:24 +02:00
Formatter.hs Add juvix format command (#1886) 2023-03-29 15:51:04 +02:00
Internal.hs Add translation from Internal to Core (#1567) 2022-11-07 14:47:56 +01:00
Isabelle.hs Translate function bodies to Isabelle/HOL (#2868) 2024-07-19 08:40:07 +01:00
Main.hs Translate function bodies to Isabelle/HOL (#2868) 2024-07-19 08:40:07 +01:00
Nockma.hs Nockma compile (#2570) 2024-01-17 11:15:38 +01:00
Package.hs Use JuvixError instead of Text for errors in Package file loading (#2459) 2023-10-23 19:01:36 +01:00
Parsing.hs Disallow tab characters as spaces (#1523) 2022-09-07 13:59:41 +02:00
Reg.hs JuvixReg recursors (#2641) 2024-02-19 08:58:19 +00:00
Repl.hs Update REPL artifacts with builtins from stored modules (#2639) 2024-02-26 16:19:04 +00:00
Resolver.hs Per-module compilation (#2468) 2023-12-30 20:15:35 +01:00
Runtime.hs Juvix C runtime (#1580) 2022-11-03 09:38:09 +01:00
Rust.hs Add precondition to run tests (#2887) 2024-07-15 10:02:48 +02:00
Scope.hs [ CI ] New jobs: ormolu and hlint 2022-04-05 19:57:21 +02:00
Termination.hs Add the termination checker to the pipeline (#111) 2022-05-30 13:40:52 +02:00
Tree.hs JuvixTree recursors and transformation framework (#2594) 2024-01-29 16:43:08 +00:00
Typecheck.hs Remove old typechecker (#2545) 2023-12-01 16:50:37 +01:00
VampIR.hs Add precondition to run tests (#2887) 2024-07-15 10:02:48 +02:00