prove --args is DEEPLY FLAWED. Maybe jam and cue as well... IDK

[mariari]

juvix --version
Juvix version 0.6.8-8272ee3
Branch: main
Commit: 8272ee32c12ac53413860165c9bb48d7e6f8256d
Date: Sat Dec 7 17:51:10 2024 +0100

The help message on the prove functionality is wrong, here it is for example

$ juvix dev anoma --config config.yaml prove                           

Usage: juvix dev anoma prove NOCKMA_FILE [--args ARGS_FILE] 
                             [-o|--output OUTPUT_FILE]

  Submit a Nockma program to Anoma.Protobuf.NockService.Prove

Available options:
  NOCKMA_FILE              Path to a .nockma file
  --args ARGS_FILE         Path to a file containing args. The args file should
                           contain a list (i.e. to pass 2 and [1 4] as args, the
                           contents should be [2 [1 4] 0]).
  -o,--output OUTPUT_FILE  Path to output file
  -h,--help                Show this help text

This implies the argument file should be [2 [ 1 4] 0], however in reality this is not the case.

What we found out was that it expected jammed input, and then it would work, for example

iex(anoma@YU-NO)73> Noun.Jam.jam([2, 2  | 0]) |> Noun.atom_binary_to_integer
672545

# File: foo.args
672545

Now if we run it we get success, however the response is very wrong

# File: Foo.juvix

-- Tried with 2 arguments as well
main : List Nat -> List Nat
  | xs := xs;

We get the output of the file with the following hexdump

This is 2 which I believe is incorrect, as I believe this is the jam of 0, not the literal 2 I put in, as I've tested this with greater values like 255 and got back 0c which is 12 which is the jam of 1, which makes 0 sense.

Further if we get into other kinds of arguments we are in for a "fun time" before we even hit the anoma client.

iex(anoma@YU-NO)74> Noun.Jam.jam([5234234 , 5234234  | 0]) |> Noun.atom_binary_to_integer
181256139001601

% juvix dev anoma --config config.yaml prove Foo.nockma --args foo.args
juvix: Nockma lists must have the form [x1 .. xn 0]
CallStack (from HasCallStack):
  error, called at src/Juvix/Prelude/Base/Foundation.hs:511:9 in juvix-0.6.8-KMrPHNRIqMmKp7F6Nz2hfm:Juvix.Prelude.Base.Foundation
  error, called at src/Juvix/Compiler/Nockma/Language.hs:602:15 in juvix-0.6.8-KMrPHNRIqMmKp7F6Nz2hfm:Juvix.Compiler.Nockma.Language

iex(anoma@YU-NO)83> Noun.Jam.jam([[444 | 0] | 888]) |> Noun.atom_binary_to_integer
7630558299653
% juvix dev anoma --config config.yaml prove Foo.nockma --args foo.args
/home/misuzu/Documents/Work/Repo/anoma-apps/foo.args:1:1: error:
Cache miss

which implies the format should be [x1 ... xn 0]

however when trying

iex(anoma@YU-NO)80> Noun.Jam.jam([1 |  2]) |> Noun.atom_binary_to_integer
4657

which works and gives back the same hexdump as before

All of this is very confusing for me

[paulcadman]

I agree the behaviour of prove --args is confusing and the documentation is incorrect and I propose that we simplify things.

But first a few points to get your example to work with the current version.

1. If you want to pass the list [2 2 0] to the main function in Foo.juvix, the args file should contain [[2 2 0] 0]. i.e [2 2 0] is the first argument (to fit the format of a Nock list of arguments: [arg1 0]).
2. You're correct that by default the args file should be jammed, but it should be jammed bytes and not an integer.
3. You can also pass the unjammed nock term as arguments when the argument file has the extension .debug.nockma

Let's see this work with you example:

Test.juvix

main : List Nat -> List Nat
  | xs := xs;

args.debug.nockma

[[2 2 0] 0]

now run:

$ juvix compile anoma Test.juvix
$ juvix dev anoma prove Test.nockma --args args.debug.nockma
$ juvix dev nockma encode --from bytes --to text < Test.proved.nockma
[2 2 0]

To run with jammed arguments, first convert the args.debug.nockma file to jammed bytes:

$ juvix dev nockma encode --from text --to bytes < args.debug.nockma > args.nockma

now run with the jammed file:

$ juvix dev anoma prove Test.nockma --args args.nockma
$ juvix dev nockma encode --from bytes --to text < Test.proved.nockma
[2 2 0]

Proposal

Fix the behaviour of prove --args to match the documentation. i.e the args file should be a Nock term (not jammed) and be of the form [arg1 arg2 ... 0] (the arguments are provided as a Nock list of arguments).