Repository navigation
Apply resugarings also to pre- and postconditions #1945
Description
Consider the following example:
#[hax_lib::requires(a[0]==0)]
fn first(a: &mut [i32; 10]) -> i32 {
a[0]
}Open this code snippet in the playground
The Lean backend produces a[(0 : usize)]_? for the occurrence of a[0] in the function body but core_models.ops.index.Index.index a (0 : usize) for the occurrence of a[0] in the requires-clause.
The reason for this is that:
LinkedItemGraph::newin https://github.com/cryspen/hax/blob/main/rust-engine/src/backends.rs#L113 is cloning all items.- The original copy of the requires clause is then dropped: https://github.com/cryspen/hax/blob/main/rust-engine/src/backends.rs#L123-L133.
- Only after that, the resugarings are applied to the original copy of the items: https://github.com/cryspen/hax/blob/main/rust-engine/src/backends.rs#L139 / https://github.com/cryspen/hax/blob/main/rust-engine/src/printer.rs#L71-L73.
- Finally the copy of the requires-clause in the
LinkedItemGraphis what's printed.
Maybe we can apply the resugarings earlier?
Activity
abentkamp commentedon Feb 18, 2026
The issue remains, but the example above had been fixed by #1950.
Here is a different example:
Open this code snippet in the playground
The same expression is translated as
let x : i32 := a;in the function body and aslet x : i32 ← (pure a);in the precondition because theLetPureresugaring is only applied to the function body.