Document that `for` loops need explicit `invariant`

[Lysxia]

I have a loop for m in r but in the resulting Why3 task there is nothing connecting the loop variable m to the iterable r. I may be missing something because examples in the test suite don't have this problem.

Example:

#[requires(forall <i: Int> 0 <= i && i < [email protected]() ==> r[i]@ < 42)]
pub fn f4(r: Vec<usize>) {
    for m in r {
        proof_assert!{ m@ < 42 };
    }
}

In the Why3 task below, field_03 mentioned in the goal is only ever related to other abstract constants that we know nothing about. There is no axiom that relates one of those to the input vector r2.

constant r2 : t_Vec4 usize t_Global4

axiom Assert24 :
  forall i:int.
   0 <= i /\ i < length (shallow_model'04 r2) ->
   to_int (index_logic'04 r2 i) < 42

constant result7 : t_IntoIter4 usize t_Global4

axiom Assert25 : inv'14 result7

axiom Assert26 : into_iter_post'04 r2 result7

constant iter3 : t_IntoIter4 usize t_Global4

constant fin6 : t_IntoIter4 usize t_Global4

constant id3 : int

constant fin7 : t_IntoIter4 usize t_Global4

constant result8 : t_Option4 usize

axiom Assert27 : inv'34 result8

axiom Assert28 :
  match result8 with
  | C_None4 ->
      completed'04
      (borrowed'mk iter3 fin7 (get_id (borrowed'mk iter3 fin6 id3)))
  | C_Some4 v -> produces'04 iter3 (singleton v) fin7
  end

axiom Assert29 : resolve'04 (borrowed'mk fin7 fin6 id3)

constant a3 : usize

axiom Assert30 : result8 = C_Some4 a3

constant field_03 : usize

axiom Assert31 : C_Some4 field_03 = result8

------------------------------- Goal --------------------------------

goal vc_f43 : to_int field_03 < 42

[xldenis]

Unfortunately, this is a tricky limitation, you need to add an invariant, any invariant for the information to be present. For loops are desugared during parsing, so we can't reliably identify them afterwards and instrument them in MIR, so instead we use macros to change their desugaring.

[Lysxia]

Thanks! I didn't know that. At least it works with #[invariant(true)].

[Lysxia]

I'm tempted to classify this as wontfix. Maybe we can also have a list of this kind of corner cases in the documentation, so I'll leave this open to remember to write that doc.