hacspec / hax

A Rust verification tool
https://hacspec.org/blog
Apache License 2.0
197 stars 20 forks source link

Engine crashes on refinement types with wildcard as binder #760

Open W95Psp opened 4 months ago

W95Psp commented 4 months ago
#[hax_lib::refinement_type(|_| true)]
pub struct Empty(usize);

The engine assumes |_| true is a function of arity one with a var pattern, not with a wildcard pattern.

cargo hax into fstar crashes with:

   Compiling literals v0.1.0 (/home/lucas/repos/hax/main/tests/literals)
    Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.21s
Fatal error: exception "Option.value_exn None"
Raised at Base__Error.raise in file "src/error.ml" (inlined), line 9, characters 14-30
Called from Base__Option.value_exn in file "src/option.ml", line 114, characters 4-21
Called from Fstar_backend.Make.pitem_unwrapped in file "backends/fstar/fstar_backend.ml", line 976, characters 16-67
Called from Fstar_backend.Make.pitem in file "backends/fstar/fstar_backend.ml", line 877, characters 12-29
Called from Fstar_backend.strings_of_item in file "backends/fstar/fstar_backend.ml", line 1453, characters 2-18
Called from Base__List.concat_map.aux in file "src/list.ml", line 726, characters 34-40
Called from Fstar_backend.string_of_items in file "backends/fstar/fstar_backend.ml", line 1514, characters 4-73
Called from Fstar_backend.translate.(fun) in file "backends/fstar/fstar_backend.ml", line 1572, characters 11-63
Called from Base__List.concat_map.aux in file "src/list.ml", line 726, characters 34-40
Called from Hax_engine__Diagnostics.Core.try_ in file "lib/diagnostics.ml", line 128, characters 26-32
Called from Lib.run in file "bin/lib.ml", line 115, characters 4-348
Called from Lib.main in file "bin/lib.ml", line 136, characters 11-24
Re-raised at Lib.main in file "bin/lib.ml", line 163, characters 6-42
Called from Dune__exe__Native_driver in file "bin/native_driver.ml", line 23, characters 2-13
error: hax: hax-engine exited with non-zero code 2
github-actions[bot] commented 2 months ago

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

W95Psp commented 1 month ago

Still relevant, but that's a very small issue, it's trivial to fix