bug: `--kernel` is silently ignored when running or proving a `.masp` package
- Lingua principale
- Rust
- Stelle
- 772
- Fork
- 352
- Merge medio
- 1g 12h
- PR unite (30g)
- 93
Descrizione
`miden-vm run` and `miden-vm prove` accept `--kernel`, validate it to differing degrees, and then
discard it entirely when the program is a `.masp` package. `miden-vm verify` honours the same flag,
so the two sides of a proof can disagree about the kernel with nothing reported to the user.
### Repro
Build a package and a throwaway kernel file:
```
printf 'pub proc double\n push.2\n mul\nend\n' > lib.masm
miden-vm bundle lib.masm --namespace mylib --output prog.masp
echo "not a kernel" > kernel.txt
```
Run the package three ways:
```
miden-vm run prog.masp --kernel kernel.txt # kernel has an invalid extension
miden-vm run prog.masp --kernel /does/not/exist.masm # kernel does not exist
miden-vm run prog.masp # no kernel at all
```
All three produce byte-identical output: the flag has no effect. The same two bad kernels are
correctly rejected against a `.masm` program:
```
$ miden-vm run prog.masm --kernel kernel.txt
Error: x Kernel file `kernel.txt` must have a .masm or .masp extension
$ miden-vm run prog.masm --kernel /does/not/exist.masm
Error: x Kernel file `/does/not/exist.masm` must be a file.
```
### Current behaviour
| command | program | missing kernel | wrong extension | kernel applied |
|---|---|---|---|---|
| `run` | `.masm` | rejected | rejected | yes |
| `run` | `.masp` | ignored | ignored | **no** |
| `prove` | `.masm` | rejected | rejected | yes |
| `prove` | `.masp` | rejected | ignored | **no** |
| `verify` | (takes a proof, not a program file) | rejected | rejected | yes |
`prove` is the more misleading of the two: `execute` checks the kernel exists
(`miden-vm/src/cli/prove.rs:110-117`) before the extension match, so a bad path is reported and the
user reasonably concludes the kernel was accepted — then `prove.rs:125` loads the package without
it. `run` does not check at all: its only kernel validation lives inside `run_masm_program`
(`run.rs:182`), and the `.masp` arm (`run.rs:80` into `run_masp_program` at `run.rs:138`) never
reads `kernel_file`.
### Why it matters
A package resolves its kernel from its own embedded kernel package (`Package::try_into_program`),
so an external `--kernel` cannot be applied to a `.masp` at all. Accepting and dropping it means
`prove --kernel k.masm` and `verify --kernel k.masm` commit to different `ProgramInfo`, and the
resulting verification failure gives no indication that the kernel was the cause.
The neighbouring `--libraries` flag documents exactly this restriction in its help text ("only used
for assembly files"). `--kernel` carries no such note, and its help text ("Path to a file (.masm or
.masp) containing the kernel to be loaded with the program") implies it always applies.
`--kernel` was added to `run`/`prove` in b74bbe3bb and wired only into the assembly path, so this
looks like an oversight rather than an intentional restriction.
### Suggested fix
Reject `--kernel` for `.masp` programs in both `run` and `prove` with an explicit error rather than
accepting and discarding it, and note the restriction in the flag's help text. Tests can follow the
existing `execute_rejects_bad_kernel_extension_before_touching_other_files` pattern in `verify.rs`.
Verified against `next` @ `031b97056`.
I'd like to fix this — could it be assigned to me before I open the PR, per CONTRIBUTING?
Guida per i contributori
Apri la guida per i contributori
Valutazione
Questa issue non è ancora stata valutata.