Apply resugarings also to pre- and postconditions

[abentkamp]

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::new in 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 LinkedItemGraph is what's printed.

Maybe we can apply the resugarings earlier?

[abentkamp]

The issue remains, but the example above had been fixed by #1950.

Here is a different example:

#[hax_lib::requires({let x = a; a == 0})]
fn mktuple(a: i32) -> bool {
    {let x = a; a == 0}
}

Open this code snippet in the playground

The same expression is translated as let x : i32 := a; in the function body and as let x : i32 ← (pure a); in the precondition because the LetPure resugaring is only applied to the function body.