search

verus-lang / verus

Verified Rust for low-level systems code
MIT License
1.06k stars 58 forks source link

remove tuples from the pool of potential auto triggers #1199

Open JoPolzin opened 1 week ago

JoPolzin commented 1 week ago

Ideally Closes #695 , which fixed itself in the meantime, but raised the problem that tuples are chosen as auto-triggers, as they are handled as functions internally.

Checking if a typeconstructor is a Tuple-constructor and discarding it from the set of possible triggers resolves this.

JoPolzin commented 1 week ago

This is the new output for the issue #695 :)

error: Could not automatically infer triggers for this quantifer.  Use #[trigger] annotations to manually mark trigger terms instead.
 --> tuple.rs:6:12
  |
6 |   requires forall |x| f.requires((x,))
  |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^

error: aborting due to 1 previous error
JoPolzin commented 1 week ago

@utaal @Chris-Hawblitzel can you take a look at the failing tests? It looks like requires and ensures clauses for closures depend on triggering on tuples. Does that change anything?

utaal commented 3 days ago

It does change things. I don't yet know in what way exactly. Perhaps we can allow them just for closures.

@Chris-Hawblitzel are you already looking into it? (I saw you self-assigned as reviewer)

Chris-Hawblitzel commented 2 days ago

@Chris-Hawblitzel are you already looking into it? (I saw you self-assigned as reviewer)

I haven't actually started. I'm happy to work on it, but feel free to take it if you want.