kani::index example in docs

[bagnalla]

Section 4.5.5 in the Kani book has this example to illustrate the use of the kani::index variable in a loop contract:

#[kani::proof]
fn forloop() {
    let mut sum: u32 = 0;
    let a: [u8; 10] = kani::any();
    kani::assume(kani::forall!(|i in (0,10)| a[i] <= 20));
    #[kani::loop_invariant(sum <= (kani::index as u32 * 20) )]
    for (i, j) in a.iter().enumerate() {
        sum = sum + (i as u32) ;
    }
    assert!(sum <= 200);
}

Since kani::index is multiplied by 20 in the loop invariant, the loop code maybe is intended to be

for (i, j) in a.iter().enumerate() {
    sum = sum + (*j as u32) ;
}

But then it doesn't make sense to use .enumerate(), and the loop could be replaced with something like

for x in a {
    sum = sum + x as u32;
}

Or if the original loop is intended, the invariant and final assertion could be tightened to say kani::index as u32 * 9 and sum <= 90.