search

hacspec / hax

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

regression around `Inconsistent implicit qualifiers (did not expect argument aquals)` #732

Open kaspar030 opened 2 weeks ago

kaspar030 commented 2 weeks ago

Hi,

our CI just broke on unchanged code:

/home/runner/.nix-profile/bin/fstar.exe
fstar.exe --cmi --warn_error -331-321-274 --cache_checked_modules --cache_dir .cache --already_cached "+Prims+FStar+LowStar+C+Spec.Loops+TestLib" --include "/nix/store/18l7w674px4kwazy5ip88yxqskwlcwxc-source"/lib --include "/nix/store/1hnjzj74rsk1g80pkq3jhvs7qg6mkfy2-fstar"/rust_primitives --include "/nix/store/1hnjzj74rsk1g80pkq3jhvs7qg6mkfy2-fstar"/core --include "/nix/store/vss9b7rkwgv7wxk4xxzh3q481iq5vimf-hax-lib"/proofs/fstar/extraction --admit_smt_queries true Riot_rs_runqueue.Runqueue.fst  --hint_file .hints/Riot_rs_runqueue.Runqueue.fst.hints
* Error 92 at Riot_rs_runqueue.Runqueue.fst(17,33-17,38):
  - Inconsistent implicit qualifiers (did not expect argument aquals)

We're using the hax action from "master", so I'm assuming some of the just merged changes here are the cause. Let me know if I can provide more info!

kaspar030 commented 2 weeks ago

I can confirm that pinning hax_reference to d10f891a19f96bcafa9e31b1d78763e4f3cf30b4 makes our CI work again, we'll be temporary doing that.

W95Psp commented 2 weeks ago

Hi, thanks for the report!

I will try to look at before the end of the day, I suspect that it is something easy to fix. We changed a convention and our F* core library may be not entirely updated yet, hence the problem you have here.

W95Psp commented 1 week ago

This issue is related to https://github.com/hacspec/hax/issues/719. One patch we merged for solving #719 yielded this issue, but was not fixing entirely #719. Thus, fixing this issue now would just make it re-appear differently when #719 is fixed. I'm thus waiting for #719 to be fixed before fixing this one.