ANF will not descend into if, match, etc

[mtzguido]

fn foo (r : ref int)
  requires r |-> 'v
  ensures r |-> 'v
{
  if (!r = 0) {
    ();
  } else {
    ();
  }
}

fn foo2 (r : ref int)
  requires r |-> 'v
  ensures r |-> 'v
{
  if (if true then !r = 0 else false) {
    ();
  } else {
    ();
  }
}

The second version fails, as the hoisting stage does not detect the condition of the if as a stateful application (rightfully). Descending into the branches is not trivial either, as the condition is an F* expression, but hoisting will produce a Pulse statement. Further, to be accurate, the hoisting must construct a Pulse conditional that only reads r in the proper branch, e.g:

if (
  if (true) { let __anf = !r; (__anf = 0) } else { false } // if a statement was a allowed here
) ....