Built with Alectryon, running Coq+SerAPI v8.12.0+0.12.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

Require Import Helpers.Helpers.
Require Import Proc.
Require Import Abstraction.
Require Import List.
Import ListNotations.

Looping combinators.

Reasoning about loops in code requires special handling because it is not just a matter of stepping through the code in sequence: the number of loop iterations might not be known ahead of time! For instance, the loop body might be iterated N times:

    loop body iteration 0
    loop body iteration 1
    ..
    loop body iteration N-1

The typical approach for reasoning about loops is to define a loop invariant: a predicate that holds before and after each iteration of the loop. This invariant holds at the boundaries of the loop iterations in the above diagram, including just before the first loop iteration, and just after the last loop iteration. To make the loop invariant useful, the invariant itself is a function of how far along we are in the loop. Annotating the above diagram with the loop invariant, we get the following:

     * starting state: loop invariant holds for 0 iterations
    loop body iteration 0
     * intermediate state: loop invariant holds for 1 iterations
    loop body iteration 1
     * intermediate state: loop invariant holds for 2 iterations
    ..
     * intermediate state: loop invariant holds for N-1 iterations
    loop body iteration N-1
     * final state: loop invariant holds for N iterations

Once we have defined such a loop invariant, we can reason about an arbitrary number of iterations of the loop, by proving just three facts: that the starting state satisfies the loop invariant (at 0 iterations); that the loop invariant after N iterations implies whatever final state we are looking for; and that each execution of the loop body moves the loop invariant from K iterations to K+1 iterations. In diagram form:

    Starting state
          |
          V
    Loop invariant(0)

         ...

    Loop invariant(K)
          |
     [loop body]
          |
          V
    Loop invariant(K+1)

         ...

    Loop invariant(N)
          |
          V
     Final state

Combinator for list iteration.

The first combinator we will define in the above style is for iterating over a list, which we call foreach. The foreach combinator takes a list of items, l, to iterate over, and a body procedure to invoke on each list element.

In some cases, we will want to accumulate results as we execute. This is done by passing an accumulator value, of type T here, through each iteration of the body. The foreach combinator takes the initial value of this accumulator, acc, and the overall combinator returns the final value of this accumulator after all loop iterations are done.

Fixpoint foreach `(l: list V) `(body: V -> T -> proc T) (acc: T) : proc T :=
  match l with
  | nil =>
    Ret acc
  | v :: l' =>
    acc <- body v acc;
    foreach l' body acc
  end.

In the case of list iteration, our loop invariant, loop_inv, is a function of the list we have processed so far, the accumulated value of type T, the ghost state A, and the current state of the system, State. A common pattern will be to store the starting state for the entire loop in the ghost state, if the loop invariant wants to relate the starting state to the current state.

Given a loop invariant, we can synthesize a spec for the entire invocation of foreach, defined by foreach_spec below. It captures the intuition that was laid out at the top of this file: the precondition for foreach is that the loop invariant holds with an initial prefix (which will be nil in the common case), and the postcondition is that the loop invariant now holds with the entire list l being processed. The recovered condition says that, when we crash, we executed some number of iterations of the loop body.

Definition foreach_spec {R} `(loop_inv: list V -> T -> A -> State -> Prop)
                        (wipe: State -> State -> Prop)
                        (prefix: list V) (l: list V) (acc: T) : Specification A T R State :=
  fun (a : A) state => {|
    pre := loop_inv prefix acc a state;
    post := fun r state' => loop_inv (prefix ++ l) r a state';
    recovered := fun _ state' =>
      exists r n pre_wipe,
        loop_inv (prefix ++ (firstn n l)) r a pre_wipe /\
        wipe pre_wipe state'
  |}.

The following theorem, foreach_ok_helper, proves that foreach_spec is correct. It uses induction over the iterations of foreach, but the benefit is that other code that needs to reason about loops no longer needs to do low-level Coq induction. It assumes that the loop body is correct in a particularly induction-friendly way, which we will clean up below.

Theorem foreach_ok_helper :
  forall `(loopinv: list V -> T -> A -> State -> Prop)
         (wipe: State -> State -> Prop)
         body `(recover: proc R) abstr l prefix acc,
    rec_wipe recover abstr wipe ->
    ( forall v acc prefix',
      proc_spec (foreach_spec loopinv wipe (prefix++prefix') [v] acc) (body v acc) recover abstr ) ->
    proc_spec (foreach_spec loopinv wipe prefix l acc) (foreach l body acc) recover abstr.forall (V T A State : Type)
  (loopinv : list V -> T -> A -> State -> Prop)
  (wipe : State -> State -> Prop)
  (body : V -> T -> proc T) (R : Type)
  (recover : proc R) (abstr : Abstraction State)
  (l prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe (prefix ++ prefix') [v]
      acc0) (body v acc0) recover abstr) ->
proc_spec (foreach_spec loopinv wipe prefix l acc)
  (foreach l body acc) recover abstr
Proof.forall (V T A State : Type)
  (loopinv : list V -> T -> A -> State -> Prop)
  (wipe : State -> State -> Prop)
  (body : V -> T -> proc T) (R : Type)
  (recover : proc R) (abstr : Abstraction State)
  (l prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe (prefix ++ prefix') [v]
      acc0) (body v acc0) recover abstr) ->
proc_spec (foreach_spec loopinv wipe prefix l acc)
  (foreach l body acc) recover abstr
  induction l.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
forall (prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe (prefix ++ prefix') [v]
      acc0) (body v acc0) recover abstr) ->
proc_spec (foreach_spec loopinv wipe prefix [] acc)
  (foreach [] body acc) recover abstr
V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l:list V
IHl:forall (prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      (prefix ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe prefix l acc)
  (foreach l body acc) recover abstr
forall (prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe 
      (prefix ++ prefix') [v] acc0) 
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe prefix (a :: l) acc)
  (foreach (a :: l) body acc) recover abstr
  -V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
forall (prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe 
      (prefix ++ prefix') [v] acc0) 
   (body v acc0) recover abstr) ->
proc_spec (foreach_spec loopinv wipe prefix [] acc)
  (foreach [] body acc) recover abstr intros.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
proc_spec (foreach_spec loopinv wipe prefix [] acc)
  (foreach [] body acc) recover abstr
    simpl.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
proc_spec (foreach_spec loopinv wipe prefix [] acc)
  (Ret acc) recover abstr
    step_proc.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a:A
state:State
H1:loopinv prefix acc a state
Lexec:Marker "post" (Ret acc)
loopinv (prefix ++ []) acc a state
V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a:A
state:State
H1:loopinv prefix acc a state
Lexec:Marker "post" (Ret acc)
state':State
H2:wipe state state'
r:R
exists (r : T) (n : nat) 
(pre_wipe : State),
  loopinv (prefix ++ firstn n []) r a pre_wipe /\
  wipe pre_wipe state'
    +V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a:A
state:State
H1:loopinv prefix acc a state
Lexec:Marker "post" (Ret acc)
loopinv (prefix ++ []) acc a state rewrite app_nil_r.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a:A
state:State
H1:loopinv prefix acc a state
Lexec:Marker "post" (Ret acc)
loopinv prefix acc a state
      auto.
    +V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a:A
state:State
H1:loopinv prefix acc a state
Lexec:Marker "post" (Ret acc)
state':State
H2:wipe state state'
r:R
exists (r : T) (n : nat) 
(pre_wipe : State),
  loopinv (prefix ++ firstn n []) r a pre_wipe /\
  wipe pre_wipe state' exists acc, 0, state.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a:A
state:State
H1:loopinv prefix acc a state
Lexec:Marker "post" (Ret acc)
state':State
H2:wipe state state'
r:R
loopinv (prefix ++ firstn 0 []) acc a state /\
wipe state state'
      simpl.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a:A
state:State
H1:loopinv prefix acc a state
Lexec:Marker "post" (Ret acc)
state':State
H2:wipe state state'
r:R
loopinv (prefix ++ []) acc a state /\
wipe state state'
      rewrite app_nil_r.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a:A
state:State
H1:loopinv prefix acc a state
Lexec:Marker "post" (Ret acc)
state':State
H2:wipe state state'
r:R
loopinv prefix acc a state /\ wipe state state'
      auto.

  -V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l:list V
IHl:forall (prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      (prefix ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe prefix l acc)
  (foreach l body acc) recover abstr
forall (prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe 
      (prefix ++ prefix') [v] acc0) 
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe prefix (a :: l) acc)
  (foreach (a :: l) body acc) recover abstr intros.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l:list V
IHl:forall (prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      (prefix ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe prefix l acc)
  (foreach l body acc) recover abstr
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
proc_spec
  (foreach_spec loopinv wipe prefix (a :: l) acc)
  (foreach (a :: l) body acc) recover abstr
    simpl.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l:list V
IHl:forall (prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      (prefix ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe prefix l acc)
  (foreach l body acc) recover abstr
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
proc_spec
  (foreach_spec loopinv wipe prefix (a :: l) acc)
  (acc <- body a acc; foreach l body acc) recover
  abstr
    step_proc.
    exists a'.
    intuition idtac.

    + rewrite app_nil_r.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l:list V
IHl:forall (prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      (prefix ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe prefix l acc)
  (foreach l body acc) recover abstr
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
L:Marker "precondition" (body a acc)
loopinv prefix acc a' state
      auto.

    +V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l:list V
IHl:forall (prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      (prefix ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe prefix l acc)
  (foreach l body acc) recover abstr
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:R
state':State
r0:T
n:nat
pre_wipe:State
H2:loopinv ((prefix ++ []) ++ firstn n [a]) r0 a'
  pre_wipe
H3:wipe pre_wipe state'
L:Marker "recovered condition" (body a acc)
exists (r : T) (n : nat) 
(pre_wipe : State),
  loopinv (prefix ++ firstn n (a :: l)) r a' pre_wipe /\
  wipe pre_wipe state' destruct n.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l:list V
IHl:forall (prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      (prefix ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe prefix l acc)
  (foreach l body acc) recover abstr
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:R
state':State
r0:T
pre_wipe:State
H2:loopinv ((prefix ++ []) ++ firstn 0 [a]) r0 a'
  pre_wipe
H3:wipe pre_wipe state'
L:Marker "recovered condition" (body a acc)
exists (r : T) (n : nat) 
(pre_wipe : State),
  loopinv (prefix ++ firstn n (a :: l)) r a' pre_wipe /\
  wipe pre_wipe state'
V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l:list V
IHl:forall (prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      (prefix ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe prefix l acc)
  (foreach l body acc) recover abstr
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:R
state':State
r0:T
n:nat
pre_wipe:State
H2:loopinv ((prefix ++ []) ++ firstn (S n) [a]) r0
  a' pre_wipe
H3:wipe pre_wipe state'
L:Marker "recovered condition" (body a acc)
exists (r : T) (n : nat) 
(pre_wipe : State),
  loopinv (prefix ++ firstn n (a :: l)) r a' pre_wipe /\
  wipe pre_wipe state'
      *V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l:list V
IHl:forall (prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      (prefix ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe prefix l acc)
  (foreach l body acc) recover abstr
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:R
state':State
r0:T
pre_wipe:State
H2:loopinv ((prefix ++ []) ++ firstn 0 [a]) r0 a'
  pre_wipe
H3:wipe pre_wipe state'
L:Marker "recovered condition" (body a acc)
exists (r : T) (n : nat) 
(pre_wipe : State),
  loopinv (prefix ++ firstn n (a :: l)) r a' pre_wipe /\
  wipe pre_wipe state' exists r0, 0, pre_wipe.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l:list V
IHl:forall (prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      (prefix ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe prefix l acc)
  (foreach l body acc) recover abstr
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:R
state':State
r0:T
pre_wipe:State
H2:loopinv ((prefix ++ []) ++ firstn 0 [a]) r0 a'
  pre_wipe
H3:wipe pre_wipe state'
L:Marker "recovered condition" (body a acc)
loopinv (prefix ++ firstn 0 (a :: l)) r0 a' pre_wipe /\
wipe pre_wipe state'
        simpl in *.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l:list V
IHl:forall (prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      (prefix ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe prefix l acc)
  (foreach l body acc) recover abstr
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:R
state':State
r0:T
pre_wipe:State
H2:loopinv ((prefix ++ []) ++ []) r0 a' pre_wipe
H3:wipe pre_wipe state'
L:Marker "recovered condition" (body a acc)
loopinv (prefix ++ []) r0 a' pre_wipe /\
wipe pre_wipe state'
        repeat rewrite app_nil_r in *.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l:list V
IHl:forall (prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      (prefix ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe prefix l acc)
  (foreach l body acc) recover abstr
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:R
state':State
r0:T
pre_wipe:State
H2:loopinv prefix r0 a' pre_wipe
H3:wipe pre_wipe state'
L:Marker "recovered condition" (body a acc)
loopinv prefix r0 a' pre_wipe /\ wipe pre_wipe state'
        eauto.

      *V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l:list V
IHl:forall (prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      (prefix ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe prefix l acc)
  (foreach l body acc) recover abstr
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:R
state':State
r0:T
n:nat
pre_wipe:State
H2:loopinv ((prefix ++ []) ++ firstn (S n) [a]) r0
  a' pre_wipe
H3:wipe pre_wipe state'
L:Marker "recovered condition" (body a acc)
exists (r : T) (n : nat) 
(pre_wipe : State),
  loopinv (prefix ++ firstn n (a :: l)) r a' pre_wipe /\
  wipe pre_wipe state' exists r0, 1, pre_wipe.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l:list V
IHl:forall (prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      (prefix ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe prefix l acc)
  (foreach l body acc) recover abstr
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:R
state':State
r0:T
n:nat
pre_wipe:State
H2:loopinv ((prefix ++ []) ++ firstn (S n) [a]) r0
  a' pre_wipe
H3:wipe pre_wipe state'
L:Marker "recovered condition" (body a acc)
loopinv (prefix ++ firstn 1 (a :: l)) r0 a' pre_wipe /\
wipe pre_wipe state'
        simpl in *.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l:list V
IHl:forall (prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      (prefix ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe prefix l acc)
  (foreach l body acc) recover abstr
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:R
state':State
r0:T
n:nat
pre_wipe:State
H2:loopinv ((prefix ++ []) ++ a :: firstn n []) r0
  a' pre_wipe
H3:wipe pre_wipe state'
L:Marker "recovered condition" (body a acc)
loopinv (prefix ++ [a]) r0 a' pre_wipe /\
wipe pre_wipe state'
        repeat rewrite app_nil_r in *.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l:list V
IHl:forall (prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      (prefix ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe prefix l acc)
  (foreach l body acc) recover abstr
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:R
state':State
r0:T
n:nat
pre_wipe:State
H2:loopinv (prefix ++ a :: firstn n []) r0 a'
  pre_wipe
H3:wipe pre_wipe state'
L:Marker "recovered condition" (body a acc)
loopinv (prefix ++ [a]) r0 a' pre_wipe /\
wipe pre_wipe state'
        rewrite firstn_nil in *.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l:list V
IHl:forall (prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      (prefix ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe prefix l acc)
  (foreach l body acc) recover abstr
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:R
state':State
r0:T
n:nat
pre_wipe:State
H2:loopinv (prefix ++ [a]) r0 a' pre_wipe
H3:wipe pre_wipe state'
L:Marker "recovered condition" (body a acc)
loopinv (prefix ++ [a]) r0 a' pre_wipe /\
wipe pre_wipe state'
        auto.

    +V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l:list V
IHl:forall (prefix : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      (prefix ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe prefix l acc)
  (foreach l body acc) recover abstr
prefix:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:T
Lexec:Marker "after" (body a acc)
proc_spec
  (fun (_ : unit) (state' : State) =>
   {|
   pre := loopinv ((prefix ++ []) ++ [a]) r a' state';
   post := fun (r' : T) (state'' : State) =>
           loopinv (prefix ++ a :: l) r' a' state'';
   recovered := fun (_ : R) (state'' : State) =>
                exists
                  (r0 : T) 
                (n : nat) 
                (pre_wipe : State),
                  loopinv
                    (prefix ++ firstn n (a :: l)) r0
                    a' pre_wipe /\
                  wipe pre_wipe state'' |})
  (foreach l body r) recover abstr specialize (IHl (prefix ++ [a])).V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l, prefix:list V
IHl:forall acc : T,
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      ((prefix ++ [a]) ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ [a]) l acc) 
  (foreach l body acc) recover abstr
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:T
Lexec:Marker "after" (body a acc)
proc_spec
  (fun (_ : unit) (state' : State) =>
   {|
   pre := loopinv ((prefix ++ []) ++ [a]) r a' state';
   post := fun (r' : T) (state'' : State) =>
           loopinv (prefix ++ a :: l) r' a' state'';
   recovered := fun (_ : R) (state'' : State) =>
                exists
                  (r0 : T) 
                (n : nat) 
                (pre_wipe : State),
                  loopinv
                    (prefix ++ firstn n (a :: l)) r0
                    a' pre_wipe /\
                  wipe pre_wipe state'' |})
  (foreach l body r) recover abstr
      eapply proc_spec_implication; intros.
      { eapply IHl; eauto.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l, prefix:list V
IHl:forall acc : T,
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      ((prefix ++ [a]) ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ [a]) l acc) 
  (foreach l body acc) recover abstr
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:T
Lexec:Marker "after" (body a acc)
L:Marker "using spec for" (foreach l body r)
forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe
     ((prefix ++ [a]) ++ prefix') [v] acc)
  (body v acc) recover abstr
        intros.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l, prefix:list V
IHl:forall acc : T,
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      ((prefix ++ [a]) ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ [a]) l acc) 
  (foreach l body acc) recover abstr
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:T
Lexec:Marker "after" (body a acc)
L:Marker "using spec for" (foreach l body r)
v:V
acc0:T
prefix':list V
proc_spec
  (foreach_spec loopinv wipe
     ((prefix ++ [a]) ++ prefix') [v] acc0)
  (body v acc0) recover abstr
        rewrite <- app_assoc.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l, prefix:list V
IHl:forall acc : T,
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      ((prefix ++ [a]) ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ [a]) l acc) 
  (foreach l body acc) recover abstr
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:T
Lexec:Marker "after" (body a acc)
L:Marker "using spec for" (foreach l body r)
v:V
acc0:T
prefix':list V
proc_spec
  (foreach_spec loopinv wipe
     (prefix ++ [a] ++ prefix') [v] acc0)
  (body v acc0) recover abstr
        eauto.
      }V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l, prefix:list V
IHl:forall acc : T,
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      ((prefix ++ [a]) ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ [a]) l acc) 
  (foreach l body acc) recover abstr
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:T
Lexec:Marker "after" (body a acc)
a0:unit
state0:State
H2:pre
  {|
  pre := loopinv ((prefix ++ []) ++ [a]) r a'
           state0;
  post := fun (r' : T) (state'' : State) =>
          loopinv (prefix ++ a :: l) r' a'
            state'';
  recovered := fun (_ : R) (state'' : State) =>
               exists
                 (r0 : T) 
               (n : nat) 
               (pre_wipe : State),
                 loopinv
                   (prefix ++ firstn n (a :: l))
                   r0 a' pre_wipe /\
                 wipe pre_wipe state'' |}
exists a'0 : A,
  pre
    (foreach_spec loopinv wipe 
       (prefix ++ [a]) l r a'0 state0) /\
  (forall (v : T) (state' : State),
   post
     (foreach_spec loopinv wipe 
        (prefix ++ [a]) l r a'0 state0) v state' ->
   post
     {|
     pre := loopinv ((prefix ++ []) ++ [a]) r a'
              state0;
     post := fun (r' : T) (state'' : State) =>
             loopinv (prefix ++ a :: l) r' a' state'';
     recovered := fun (_ : R) (state'' : State) =>
                  exists
                    (r0 : T) 
                  (n : nat) 
                  (pre_wipe : State),
                    loopinv
                      (prefix ++ firstn n (a :: l)) r0
                      a' pre_wipe /\
                    wipe pre_wipe state'' |} v state') /\
  (forall (rv : R) (state' : State),
   recovered
     (foreach_spec loopinv wipe 
        (prefix ++ [a]) l r a'0 state0) rv state' ->
   recovered
     {|
     pre := loopinv ((prefix ++ []) ++ [a]) r a'
              state0;
     post := fun (r' : T) (state'' : State) =>
             loopinv (prefix ++ a :: l) r' a' state'';
     recovered := fun (_ : R) (state'' : State) =>
                  exists
                    (r0 : T) 
                  (n : nat) 
                  (pre_wipe : State),
                    loopinv
                      (prefix ++ firstn n (a :: l)) r0
                      a' pre_wipe /\
                    wipe pre_wipe state'' |} rv state')

      exists a'.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l, prefix:list V
IHl:forall acc : T,
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      ((prefix ++ [a]) ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ [a]) l acc) 
  (foreach l body acc) recover abstr
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:T
Lexec:Marker "after" (body a acc)
a0:unit
state0:State
H2:pre
  {|
  pre := loopinv ((prefix ++ []) ++ [a]) r a'
           state0;
  post := fun (r' : T) (state'' : State) =>
          loopinv (prefix ++ a :: l) r' a'
            state'';
  recovered := fun (_ : R) (state'' : State) =>
               exists
                 (r0 : T) 
               (n : nat) 
               (pre_wipe : State),
                 loopinv
                   (prefix ++ firstn n (a :: l))
                   r0 a' pre_wipe /\
                 wipe pre_wipe state'' |}
pre
  (foreach_spec loopinv wipe 
     (prefix ++ [a]) l r a' state0) /\
(forall (v : T) (state' : State),
 post
   (foreach_spec loopinv wipe 
      (prefix ++ [a]) l r a' state0) v state' ->
 post
   {|
   pre := loopinv ((prefix ++ []) ++ [a]) r a' state0;
   post := fun (r' : T) (state'' : State) =>
           loopinv (prefix ++ a :: l) r' a' state'';
   recovered := fun (_ : R) (state'' : State) =>
                exists
                  (r0 : T) 
                (n : nat) 
                (pre_wipe : State),
                  loopinv
                    (prefix ++ firstn n (a :: l)) r0
                    a' pre_wipe /\
                  wipe pre_wipe state'' |} v state') /\
(forall (rv : R) (state' : State),
 recovered
   (foreach_spec loopinv wipe 
      (prefix ++ [a]) l r a' state0) rv state' ->
 recovered
   {|
   pre := loopinv ((prefix ++ []) ++ [a]) r a' state0;
   post := fun (r' : T) (state'' : State) =>
           loopinv (prefix ++ a :: l) r' a' state'';
   recovered := fun (_ : R) (state'' : State) =>
                exists
                  (r0 : T) 
                (n : nat) 
                (pre_wipe : State),
                  loopinv
                    (prefix ++ firstn n (a :: l)) r0
                    a' pre_wipe /\
                  wipe pre_wipe state'' |} rv state')
      simpl in *.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l, prefix:list V
IHl:forall acc : T,
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      ((prefix ++ [a]) ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ [a]) l acc) 
  (foreach l body acc) recover abstr
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:T
Lexec:Marker "after" (body a acc)
a0:unit
state0:State
H2:loopinv ((prefix ++ []) ++ [a]) r a' state0
loopinv (prefix ++ [a]) r a' state0 /\
(forall (v : T) (state' : State),
 loopinv ((prefix ++ [a]) ++ l) v a' state' ->
 loopinv (prefix ++ a :: l) v a' state') /\
(R ->
 forall state' : State,
 (exists (r : T) (n : nat) 
  (pre_wipe : State),
    loopinv ((prefix ++ [a]) ++ firstn n l) r a'
      pre_wipe /\ wipe pre_wipe state') ->
 exists (r : T) (n : nat) 
 (pre_wipe : State),
   loopinv (prefix ++ firstn n (a :: l)) r a' pre_wipe /\
   wipe pre_wipe state')
      rewrite app_nil_r in *.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l, prefix:list V
IHl:forall acc : T,
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      ((prefix ++ [a]) ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ [a]) l acc) 
  (foreach l body acc) recover abstr
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:T
Lexec:Marker "after" (body a acc)
a0:unit
state0:State
H2:loopinv (prefix ++ [a]) r a' state0
loopinv (prefix ++ [a]) r a' state0 /\
(forall (v : T) (state' : State),
 loopinv ((prefix ++ [a]) ++ l) v a' state' ->
 loopinv (prefix ++ a :: l) v a' state') /\
(R ->
 forall state' : State,
 (exists (r : T) (n : nat) 
  (pre_wipe : State),
    loopinv ((prefix ++ [a]) ++ firstn n l) r a'
      pre_wipe /\ wipe pre_wipe state') ->
 exists (r : T) (n : nat) 
 (pre_wipe : State),
   loopinv (prefix ++ firstn n (a :: l)) r a' pre_wipe /\
   wipe pre_wipe state')

      intuition eauto.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l, prefix:list V
IHl:forall acc : T,
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      ((prefix ++ [a]) ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ [a]) l acc) 
  (foreach l body acc) recover abstr
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:T
Lexec:Marker "after" (body a acc)
a0:unit
state0:State
H2:loopinv (prefix ++ [a]) r a' state0
v:T
state':State
H3:loopinv ((prefix ++ [a]) ++ l) v a' state'
loopinv (prefix ++ a :: l) v a' state'
V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l, prefix:list V
IHl:forall acc : T,
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      ((prefix ++ [a]) ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ [a]) l acc) 
  (foreach l body acc) recover abstr
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:T
Lexec:Marker "after" (body a acc)
a0:unit
state0:State
H2:loopinv (prefix ++ [a]) r a' state0
rv:R
state':State
r0:T
n:nat
pre_wipe:State
H3:loopinv ((prefix ++ [a]) ++ firstn n l) r0 a'
  pre_wipe
H4:wipe pre_wipe state'
exists (r : T) (n : nat) 
(pre_wipe : State),
  loopinv (prefix ++ firstn n (a :: l)) r a' pre_wipe /\
  wipe pre_wipe state'
      *V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l, prefix:list V
IHl:forall acc : T,
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      ((prefix ++ [a]) ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ [a]) l acc) 
  (foreach l body acc) recover abstr
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:T
Lexec:Marker "after" (body a acc)
a0:unit
state0:State
H2:loopinv (prefix ++ [a]) r a' state0
v:T
state':State
H3:loopinv ((prefix ++ [a]) ++ l) v a' state'
loopinv (prefix ++ a :: l) v a' state' rewrite <- app_assoc in *.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l, prefix:list V
IHl:forall acc : T,
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      ((prefix ++ [a]) ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ [a]) l acc) 
  (foreach l body acc) recover abstr
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:T
Lexec:Marker "after" (body a acc)
a0:unit
state0:State
H2:loopinv (prefix ++ [a]) r a' state0
v:T
state':State
H3:loopinv (prefix ++ [a] ++ l) v a' state'
loopinv (prefix ++ a :: l) v a' state'
        eauto.

      *V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l, prefix:list V
IHl:forall acc : T,
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      ((prefix ++ [a]) ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ [a]) l acc) 
  (foreach l body acc) recover abstr
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:T
Lexec:Marker "after" (body a acc)
a0:unit
state0:State
H2:loopinv (prefix ++ [a]) r a' state0
rv:R
state':State
r0:T
n:nat
pre_wipe:State
H3:loopinv ((prefix ++ [a]) ++ firstn n l) r0 a'
  pre_wipe
H4:wipe pre_wipe state'
exists (r : T) (n : nat) 
(pre_wipe : State),
  loopinv (prefix ++ firstn n (a :: l)) r a' pre_wipe /\
  wipe pre_wipe state' exists r0, (S n), pre_wipe.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l, prefix:list V
IHl:forall acc : T,
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      ((prefix ++ [a]) ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ [a]) l acc) 
  (foreach l body acc) recover abstr
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:T
Lexec:Marker "after" (body a acc)
a0:unit
state0:State
H2:loopinv (prefix ++ [a]) r a' state0
rv:R
state':State
r0:T
n:nat
pre_wipe:State
H3:loopinv ((prefix ++ [a]) ++ firstn n l) r0 a'
  pre_wipe
H4:wipe pre_wipe state'
loopinv (prefix ++ firstn (S n) (a :: l)) r0 a'
  pre_wipe /\ wipe pre_wipe state'
        simpl.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l, prefix:list V
IHl:forall acc : T,
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      ((prefix ++ [a]) ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ [a]) l acc) 
  (foreach l body acc) recover abstr
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:T
Lexec:Marker "after" (body a acc)
a0:unit
state0:State
H2:loopinv (prefix ++ [a]) r a' state0
rv:R
state':State
r0:T
n:nat
pre_wipe:State
H3:loopinv ((prefix ++ [a]) ++ firstn n l) r0 a'
  pre_wipe
H4:wipe pre_wipe state'
loopinv (prefix ++ a :: firstn n l) r0 a' pre_wipe /\
wipe pre_wipe state'
        rewrite <- app_assoc in *.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
a:V
l, prefix:list V
IHl:forall acc : T,
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix' : list V),
 proc_spec
   (foreach_spec loopinv wipe
      ((prefix ++ [a]) ++ prefix') [v] acc0)
   (body v acc0) recover abstr) ->
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ [a]) l acc) 
  (foreach l body acc) recover abstr
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe 
     (prefix ++ prefix') [v] acc) 
  (body v acc) recover abstr
a':A
state:State
H1:loopinv prefix acc a' state
r:T
Lexec:Marker "after" (body a acc)
a0:unit
state0:State
H2:loopinv (prefix ++ [a]) r a' state0
rv:R
state':State
r0:T
n:nat
pre_wipe:State
H3:loopinv (prefix ++ [a] ++ firstn n l) r0 a'
  pre_wipe
H4:wipe pre_wipe state'
loopinv (prefix ++ a :: firstn n l) r0 a' pre_wipe /\
wipe pre_wipe state'
        intuition eauto.
Qed.

In order to reason about foreach, we need to prove that each iteration of the body preserves the loop invariant. The following definition, foreach_body_spec, captures what we expect to be true about a single execution of the loop body: starting with a precondition that the loop invariant holds for some prefix of the list, the postcondition must be that the loop invariant holds with one more element added to the list, and the recovery condition is that either we processed one more element, or we did nothing.

Definition foreach_body_spec {R} `(loop_inv: list V -> T -> A -> State -> Prop)
                             (wipe: State -> State -> Prop)
                             (prefix: list V) (v: V) (acc: T) : Specification A T R State :=
  fun (a : A) state => {|
    pre := loop_inv prefix acc a state;
    post := fun r state' => loop_inv (prefix ++ [v]) r a state';
    recovered := fun _ state' =>
      exists pre_wipe,
        ( loop_inv prefix acc a pre_wipe \/
          exists r', loop_inv (prefix ++ [v]) r' a pre_wipe ) /\
        wipe pre_wipe state'
  |}.

The final theorem, foreach_ok, simply re-states foreach_ok_helper using a more friendly definition for what must be true about the loop body, with the help of the foreach_body_spec.

Theorem foreach_ok :
  forall `(loopinv: list V -> T -> A -> State -> Prop)
         (wipe: State -> State -> Prop)
         body `(recover: proc R) abstr l acc,
    rec_wipe recover abstr wipe ->
    ( forall v acc prefix,
      proc_spec (foreach_body_spec loopinv wipe prefix v acc) (body v acc) recover abstr ) ->
    proc_spec (foreach_spec loopinv wipe nil l acc) (foreach l body acc) recover abstr.forall (V T A State : Type)
  (loopinv : list V -> T -> A -> State -> Prop)
  (wipe : State -> State -> Prop)
  (body : V -> T -> proc T) (R : Type)
  (recover : proc R) (abstr : Abstraction State)
  (l : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix : list V),
 proc_spec
   (foreach_body_spec loopinv wipe prefix v acc0)
   (body v acc0) recover abstr) ->
proc_spec (foreach_spec loopinv wipe [] l acc)
  (foreach l body acc) recover abstr
Proof.forall (V T A State : Type)
  (loopinv : list V -> T -> A -> State -> Prop)
  (wipe : State -> State -> Prop)
  (body : V -> T -> proc T) (R : Type)
  (recover : proc R) (abstr : Abstraction State)
  (l : list V) (acc : T),
rec_wipe recover abstr wipe ->
(forall (v : V) (acc0 : T) (prefix : list V),
 proc_spec
   (foreach_body_spec loopinv wipe prefix v acc0)
   (body v acc0) recover abstr) ->
proc_spec (foreach_spec loopinv wipe [] l acc)
  (foreach l body acc) recover abstr
  intros.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
l:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix : list V),
proc_spec
  (foreach_body_spec loopinv wipe prefix v acc)
  (body v acc) recover abstr
proc_spec (foreach_spec loopinv wipe [] l acc)
  (foreach l body acc) recover abstr
  eapply foreach_ok_helper.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
l:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix : list V),
proc_spec
  (foreach_body_spec loopinv wipe prefix v acc)
  (body v acc) recover abstr
rec_wipe recover abstr wipe
V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
l:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix : list V),
proc_spec
  (foreach_body_spec loopinv wipe prefix v acc)
  (body v acc) recover abstr
forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe ([] ++ prefix') [v] acc)
  (body v acc) recover abstr
  {V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
l:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix : list V),
proc_spec
  (foreach_body_spec loopinv wipe prefix v acc)
  (body v acc) recover abstr
rec_wipe recover abstr wipe eauto. }V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
l:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix : list V),
proc_spec
  (foreach_body_spec loopinv wipe prefix v acc)
  (body v acc) recover abstr
forall (v : V) (acc : T) (prefix' : list V),
proc_spec
  (foreach_spec loopinv wipe ([] ++ prefix') [v] acc)
  (body v acc) recover abstr

  intros.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
l:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix : list V),
proc_spec
  (foreach_body_spec loopinv wipe prefix v acc)
  (body v acc) recover abstr
v:V
acc0:T
prefix':list V
proc_spec
  (foreach_spec loopinv wipe ([] ++ prefix') [v] acc0)
  (body v acc0) recover abstr
  simpl.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
l:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix : list V),
proc_spec
  (foreach_body_spec loopinv wipe prefix v acc)
  (body v acc) recover abstr
v:V
acc0:T
prefix':list V
proc_spec (foreach_spec loopinv wipe prefix' [v] acc0)
  (body v acc0) recover abstr
  eapply proc_spec_implication.
  { intros.
    eauto. }

  intros.
  simpl in *.
  exists a.
  intuition eauto.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
l:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix : list V),
proc_spec
  (foreach_body_spec loopinv wipe prefix v acc)
  (body v acc) recover abstr
v:V
acc0:T
prefix':list V
a:A
state:State
H1:loopinv prefix' acc0 a state
rv:R
state', pre_wipe:State
H2:loopinv prefix' acc0 a pre_wipe
H3:wipe pre_wipe state'
exists (r : T) (n : nat) 
(pre_wipe : State),
  loopinv (prefix' ++ firstn n [v]) r a pre_wipe /\
  wipe pre_wipe state'
V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
l:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix : list V),
proc_spec
  (foreach_body_spec loopinv wipe prefix v acc)
  (body v acc) recover abstr
v:V
acc0:T
prefix':list V
a:A
state:State
H1:loopinv prefix' acc0 a state
rv:R
state', pre_wipe:State
r':T
H2:loopinv (prefix' ++ [v]) r' a pre_wipe
H3:wipe pre_wipe state'
exists (r : T) (n : nat) 
(pre_wipe : State),
  loopinv (prefix' ++ firstn n [v]) r a pre_wipe /\
  wipe pre_wipe state'

  -V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
l:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix : list V),
proc_spec
  (foreach_body_spec loopinv wipe prefix v acc)
  (body v acc) recover abstr
v:V
acc0:T
prefix':list V
a:A
state:State
H1:loopinv prefix' acc0 a state
rv:R
state', pre_wipe:State
H2:loopinv prefix' acc0 a pre_wipe
H3:wipe pre_wipe state'
exists (r : T) (n : nat) 
(pre_wipe : State),
  loopinv (prefix' ++ firstn n [v]) r a pre_wipe /\
  wipe pre_wipe state' exists acc0, 0, pre_wipe.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
l:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix : list V),
proc_spec
  (foreach_body_spec loopinv wipe prefix v acc)
  (body v acc) recover abstr
v:V
acc0:T
prefix':list V
a:A
state:State
H1:loopinv prefix' acc0 a state
rv:R
state', pre_wipe:State
H2:loopinv prefix' acc0 a pre_wipe
H3:wipe pre_wipe state'
loopinv (prefix' ++ firstn 0 [v]) acc0 a pre_wipe /\
wipe pre_wipe state'
    simpl.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
l:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix : list V),
proc_spec
  (foreach_body_spec loopinv wipe prefix v acc)
  (body v acc) recover abstr
v:V
acc0:T
prefix':list V
a:A
state:State
H1:loopinv prefix' acc0 a state
rv:R
state', pre_wipe:State
H2:loopinv prefix' acc0 a pre_wipe
H3:wipe pre_wipe state'
loopinv (prefix' ++ []) acc0 a pre_wipe /\
wipe pre_wipe state'
    rewrite app_nil_r.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
l:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix : list V),
proc_spec
  (foreach_body_spec loopinv wipe prefix v acc)
  (body v acc) recover abstr
v:V
acc0:T
prefix':list V
a:A
state:State
H1:loopinv prefix' acc0 a state
rv:R
state', pre_wipe:State
H2:loopinv prefix' acc0 a pre_wipe
H3:wipe pre_wipe state'
loopinv prefix' acc0 a pre_wipe /\
wipe pre_wipe state'
    intuition eauto.

  -V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
l:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix : list V),
proc_spec
  (foreach_body_spec loopinv wipe prefix v acc)
  (body v acc) recover abstr
v:V
acc0:T
prefix':list V
a:A
state:State
H1:loopinv prefix' acc0 a state
rv:R
state', pre_wipe:State
r':T
H2:loopinv (prefix' ++ [v]) r' a pre_wipe
H3:wipe pre_wipe state'
exists (r : T) (n : nat) 
(pre_wipe : State),
  loopinv (prefix' ++ firstn n [v]) r a pre_wipe /\
  wipe pre_wipe state' exists r', 1, pre_wipe.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
l:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix : list V),
proc_spec
  (foreach_body_spec loopinv wipe prefix v acc)
  (body v acc) recover abstr
v:V
acc0:T
prefix':list V
a:A
state:State
H1:loopinv prefix' acc0 a state
rv:R
state', pre_wipe:State
r':T
H2:loopinv (prefix' ++ [v]) r' a pre_wipe
H3:wipe pre_wipe state'
loopinv (prefix' ++ firstn 1 [v]) r' a pre_wipe /\
wipe pre_wipe state'
    simpl.V, T, A, State:Type
loopinv:list V -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:V -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
l:list V
acc:T
H:rec_wipe recover abstr wipe
H0:forall (v : V) (acc : T) (prefix : list V),
proc_spec
  (foreach_body_spec loopinv wipe prefix v acc)
  (body v acc) recover abstr
v:V
acc0:T
prefix':list V
a:A
state:State
H1:loopinv prefix' acc0 a state
rv:R
state', pre_wipe:State
r':T
H2:loopinv (prefix' ++ [v]) r' a pre_wipe
H3:wipe pre_wipe state'
loopinv (prefix' ++ [v]) r' a pre_wipe /\
wipe pre_wipe state'
    intuition eauto.
Qed.

Combinator for nat iteration.

A second variant of looping construct that you will find useful in the labs is to iterate over nat values in some range. The combinator below, for_range, does exactly that: it invokes the body code for each nat starting with start and going up count from there.

The accumulator support is analogous to what we defined in foreach above.

Fixpoint for_range (start: nat) (count: nat) `(body: nat -> T -> proc T) (acc: T) : proc T :=
  match count with
  | O =>
    Ret acc
  | S count' =>
    acc <- body start acc;
    for_range (start + 1) count' body acc
  end.

The definitions of for_range_spec and for_range_ok mirror the definitions of foreach_spec and foreach_ok above. There is no analogue of foreach_ok_helper and foreach_body_spec, because the for_range_spec is usable enough as-is for the body correctness condition, without re-phrasing it like we did in foreach_body_spec.

Definition for_range_spec {R} `(loop_inv: nat -> T -> A -> State -> Prop)
                          (wipe: State -> State -> Prop)
                          (count: nat) (base: nat) (acc: T) : Specification A T R State :=
  fun (a : A) state => {|
    pre := loop_inv base acc a state;
    post := fun r state' => loop_inv (base+count) r a state';
    recovered := fun _ state' =>
      exists r n pre_wipe,
        loop_inv (base+n) r a pre_wipe /\
        n <= count /\
        wipe pre_wipe state'
  |}.

Theorem for_range_ok :
  forall `(loopinv: nat -> T -> A -> State -> Prop)
         (wipe: State -> State -> Prop)
         body `(recover: proc R) abstr count start acc,
    rec_wipe recover abstr wipe ->
    ( forall n acc,
      n < start+count ->
      proc_spec (for_range_spec loopinv wipe 1 n acc) (body n acc) recover abstr ) ->
    proc_spec (for_range_spec loopinv wipe count start acc) (for_range start count body acc) recover abstr.forall (T A State : Type)
  (loopinv : nat -> T -> A -> State -> Prop)
  (wipe : State -> State -> Prop)
  (body : nat -> T -> proc T) (R : Type)
  (recover : proc R) (abstr : Abstraction State)
  (count start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 n < start + count ->
 proc_spec (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start acc)
  (for_range start count body acc) recover abstr
Proof.forall (T A State : Type)
  (loopinv : nat -> T -> A -> State -> Prop)
  (wipe : State -> State -> Prop)
  (body : nat -> T -> proc T) (R : Type)
  (recover : proc R) (abstr : Abstraction State)
  (count start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 n < start + count ->
 proc_spec (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start acc)
  (for_range start count body acc) recover abstr
  induction count.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 n < start + 0 ->
 proc_spec (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec (for_range_spec loopinv wipe 0 start acc)
  (for_range start 0 body acc) recover abstr
T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 n < start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 n < start + S count ->
 proc_spec (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe (S count) start acc)
  (for_range start (S count) body acc) recover abstr
  -T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 n < start + 0 ->
 proc_spec (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec (for_range_spec loopinv wipe 0 start acc)
  (for_range start 0 body acc) recover abstr intros.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
n < start + 0 ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
proc_spec (for_range_spec loopinv wipe 0 start acc)
  (for_range start 0 body acc) recover abstr
    simpl.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
n < start + 0 ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
proc_spec (for_range_spec loopinv wipe 0 start acc)
  (Ret acc) recover abstr
    step_proc.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + 0 ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
a:A
state:State
H1:loopinv start acc a state
Lexec:Marker "post" (Ret acc)
loopinv (start + 0) acc a state
T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + 0 ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
a:A
state:State
H1:loopinv start acc a state
Lexec:Marker "post" (Ret acc)
state':State
H2:wipe state state'
r:R
exists (r : T) (n : nat) 
(pre_wipe : State),
  loopinv (start + n) r a pre_wipe /\
  n <= 0 /\ wipe pre_wipe state'
    +T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + 0 ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
a:A
state:State
H1:loopinv start acc a state
Lexec:Marker "post" (Ret acc)
loopinv (start + 0) acc a state replace (start + 0) with start by lia.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + 0 ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
a:A
state:State
H1:loopinv start acc a state
Lexec:Marker "post" (Ret acc)
loopinv start acc a state
      eauto.
    +T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + 0 ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
a:A
state:State
H1:loopinv start acc a state
Lexec:Marker "post" (Ret acc)
state':State
H2:wipe state state'
r:R
exists (r : T) (n : nat) 
(pre_wipe : State),
  loopinv (start + n) r a pre_wipe /\
  n <= 0 /\ wipe pre_wipe state' exists acc, 0, state.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + 0 ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
a:A
state:State
H1:loopinv start acc a state
Lexec:Marker "post" (Ret acc)
state':State
H2:wipe state state'
r:R
loopinv (start + 0) acc a state /\
0 <= 0 /\ wipe state state'
      replace (start + 0) with start by lia.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + 0 ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
a:A
state:State
H1:loopinv start acc a state
Lexec:Marker "post" (Ret acc)
state':State
H2:wipe state state'
r:R
loopinv start acc a state /\
0 <= 0 /\ wipe state state'
      intuition eauto.

  -T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 n < start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 n < start + S count ->
 proc_spec (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe (S count) start acc)
  (for_range start (S count) body acc) recover abstr intros.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 n < start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
n < start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
proc_spec
  (for_range_spec loopinv wipe (S count) start acc)
  (for_range start (S count) body acc) recover abstr
    simpl.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 n < start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
n < start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
proc_spec
  (for_range_spec loopinv wipe (S count) start acc)
  (acc <- body start acc;
   for_range (start + 1) count body acc) recover abstr
    specialize (H0 start acc ltac:(lia)) as H0'.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 n < start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
n < start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
proc_spec
  (for_range_spec loopinv wipe (S count) start acc)
  (acc <- body start acc;
   for_range (start + 1) count body acc) recover abstr
    step_proc.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
exists a : A,
  (Marker "precondition" (body start acc) ->
   loopinv start acc a state) /\
  (R ->
   forall state' : State,
   (exists (r0 : T) (n : nat) 
    (pre_wipe : State),
      loopinv (start + n) r0 a pre_wipe /\
      n <= 1 /\ wipe pre_wipe state') ->
   Marker "recovered condition" (body start acc) ->
   exists (r0 : T) (n : nat) 
   (pre_wipe : State),
     loopinv (start + n) r0 a' pre_wipe /\
     n <= S count /\ wipe pre_wipe state') /\
  (forall r : T,
   Marker "after" (body start acc) ->
   proc_spec
     (fun (_ : unit) (state' : State) =>
      {|
      pre := loopinv (start + 1) r a state';
      post := fun (r' : T) (state'' : State) =>
              loopinv (start + S count) r' a' state'';
      recovered := fun (_ : R) (state'' : State) =>
                   exists
                     (r1 : T) 
                   (n : nat) 
                   (pre_wipe : State),
                     loopinv 
                       (start + n) r1 a' pre_wipe /\
                     n <= S count /\
                     wipe pre_wipe state'' |})
     (for_range (start + 1) count body r) recover
     abstr)
    exists a'.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
(Marker "precondition" (body start acc) ->
 loopinv start acc a' state) /\
(R ->
 forall state' : State,
 (exists (r0 : T) (n : nat) 
  (pre_wipe : State),
    loopinv (start + n) r0 a' pre_wipe /\
    n <= 1 /\ wipe pre_wipe state') ->
 Marker "recovered condition" (body start acc) ->
 exists (r0 : T) (n : nat) 
 (pre_wipe : State),
   loopinv (start + n) r0 a' pre_wipe /\
   n <= S count /\ wipe pre_wipe state') /\
(forall r : T,
 Marker "after" (body start acc) ->
 proc_spec
   (fun (_ : unit) (state' : State) =>
    {|
    pre := loopinv (start + 1) r a' state';
    post := fun (r' : T) (state'' : State) =>
            loopinv (start + S count) r' a' state'';
    recovered := fun (_ : R) (state'' : State) =>
                 exists
                   (r1 : T) 
                 (n : nat) 
                 (pre_wipe : State),
                   loopinv (start + n) r1 a' pre_wipe /\
                   n <= S count /\
                   wipe pre_wipe state'' |})
   (for_range (start + 1) count body r) recover abstr)
    intuition idtac.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:R
state':State
r0:T
n:nat
pre_wipe:State
H2:loopinv (start + n) r0 a' pre_wipe
H3:n <= 1
H4:wipe pre_wipe state'
L:Marker "recovered condition" (body start acc)
exists (r : T) (n : nat) 
(pre_wipe : State),
  loopinv (start + n) r a' pre_wipe /\
  n <= S count /\ wipe pre_wipe state'
T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:T
Lexec:Marker "after" (body start acc)
proc_spec
  (fun (_ : unit) (state' : State) =>
   {|
   pre := loopinv (start + 1) r a' state';
   post := fun (r' : T) (state'' : State) =>
           loopinv (start + S count) r' a' state'';
   recovered := fun (_ : R) (state'' : State) =>
                exists
                  (r0 : T) 
                (n : nat) 
                (pre_wipe : State),
                  loopinv (start + n) r0 a' pre_wipe /\
                  n <= S count /\
                  wipe pre_wipe state'' |})
  (for_range (start + 1) count body r) recover abstr

    +T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:R
state':State
r0:T
n:nat
pre_wipe:State
H2:loopinv (start + n) r0 a' pre_wipe
H3:n <= 1
H4:wipe pre_wipe state'
L:Marker "recovered condition" (body start acc)
exists (r : T) (n : nat) 
(pre_wipe : State),
  loopinv (start + n) r a' pre_wipe /\
  n <= S count /\ wipe pre_wipe state' exists r0, n, pre_wipe.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:R
state':State
r0:T
n:nat
pre_wipe:State
H2:loopinv (start + n) r0 a' pre_wipe
H3:n <= 1
H4:wipe pre_wipe state'
L:Marker "recovered condition" (body start acc)
loopinv (start + n) r0 a' pre_wipe /\
n <= S count /\ wipe pre_wipe state'
      intuition eauto.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:R
state':State
r0:T
n:nat
pre_wipe:State
H2:loopinv (start + n) r0 a' pre_wipe
H3:n <= 1
H4:wipe pre_wipe state'
L:Marker "recovered condition" (body start acc)
n <= S count
      lia.

    +T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:T
Lexec:Marker "after" (body start acc)
proc_spec
  (fun (_ : unit) (state' : State) =>
   {|
   pre := loopinv (start + 1) r a' state';
   post := fun (r' : T) (state'' : State) =>
           loopinv (start + S count) r' a' state'';
   recovered := fun (_ : R) (state'' : State) =>
                exists
                  (r0 : T) 
                (n : nat) 
                (pre_wipe : State),
                  loopinv (start + n) r0 a' pre_wipe /\
                  n <= S count /\
                  wipe pre_wipe state'' |})
  (for_range (start + 1) count body r) recover abstr eapply proc_spec_implication.
      { intros. apply IHcount; eauto.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:T
Lexec:Marker "after" (body start acc)
L:Marker "using spec for"
  (for_range (start + 1) count body r)
forall (n : nat) (acc : T),
S n <= start + 1 + count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
        intros.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:T
Lexec:Marker "after" (body start acc)
L:Marker "using spec for"
  (for_range (start + 1) count body r)
n:nat
acc0:T
H2:S n <= start + 1 + count
proc_spec (for_range_spec loopinv wipe 1 n acc0)
  (body n acc0) recover abstr eapply H0.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:T
Lexec:Marker "after" (body start acc)
L:Marker "using spec for"
  (for_range (start + 1) count body r)
n:nat
acc0:T
H2:S n <= start + 1 + count
S n <= start + S count lia. }T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:T
Lexec:Marker "after" (body start acc)
unit ->
forall state : State,
pre
  {|
  pre := loopinv (start + 1) r a' state;
  post := fun (r' : T) (state'' : State) =>
          loopinv (start + S count) r' a' state'';
  recovered := fun (_ : R) (state'' : State) =>
               exists
                 (r0 : T) 
               (n : nat) 
               (pre_wipe : State),
                 loopinv (start + n) r0 a' pre_wipe /\
                 n <= S count /\ wipe pre_wipe state'' |} ->
exists a'0 : A,
  pre
    (for_range_spec loopinv wipe count 
       (start + 1) r a'0 state) /\
  (forall (v : T) (state' : State),
   post
     (for_range_spec loopinv wipe count 
        (start + 1) r a'0 state) v state' ->
   post
     {|
     pre := loopinv (start + 1) r a' state;
     post := fun (r' : T) (state'' : State) =>
             loopinv (start + S count) r' a' state'';
     recovered := fun (_ : R) (state'' : State) =>
                  exists
                    (r0 : T) 
                  (n : nat) 
                  (pre_wipe : State),
                    loopinv (start + n) r0 a' pre_wipe /\
                    n <= S count /\
                    wipe pre_wipe state'' |} v state') /\
  (forall (rv : R) (state' : State),
   recovered
     (for_range_spec loopinv wipe count 
        (start + 1) r a'0 state) rv state' ->
   recovered
     {|
     pre := loopinv (start + 1) r a' state;
     post := fun (r' : T) (state'' : State) =>
             loopinv (start + S count) r' a' state'';
     recovered := fun (_ : R) (state'' : State) =>
                  exists
                    (r0 : T) 
                  (n : nat) 
                  (pre_wipe : State),
                    loopinv (start + n) r0 a' pre_wipe /\
                    n <= S count /\
                    wipe pre_wipe state'' |} rv state')

      intros.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:T
Lexec:Marker "after" (body start acc)
a:unit
state0:State
H2:pre
  {|
  pre := loopinv (start + 1) r a' state0;
  post := fun (r' : T) (state'' : State) =>
          loopinv (start + S count) r' a' state'';
  recovered := fun (_ : R) (state'' : State) =>
               exists
                 (r0 : T) 
               (n : nat) 
               (pre_wipe : State),
                 loopinv 
                   (start + n) r0 a' pre_wipe /\
                 n <= S count /\
                 wipe pre_wipe state'' |}
exists a'0 : A,
  pre
    (for_range_spec loopinv wipe count 
       (start + 1) r a'0 state0) /\
  (forall (v : T) (state' : State),
   post
     (for_range_spec loopinv wipe count 
        (start + 1) r a'0 state0) v state' ->
   post
     {|
     pre := loopinv (start + 1) r a' state0;
     post := fun (r' : T) (state'' : State) =>
             loopinv (start + S count) r' a' state'';
     recovered := fun (_ : R) (state'' : State) =>
                  exists
                    (r0 : T) 
                  (n : nat) 
                  (pre_wipe : State),
                    loopinv (start + n) r0 a' pre_wipe /\
                    n <= S count /\
                    wipe pre_wipe state'' |} v state') /\
  (forall (rv : R) (state' : State),
   recovered
     (for_range_spec loopinv wipe count 
        (start + 1) r a'0 state0) rv state' ->
   recovered
     {|
     pre := loopinv (start + 1) r a' state0;
     post := fun (r' : T) (state'' : State) =>
             loopinv (start + S count) r' a' state'';
     recovered := fun (_ : R) (state'' : State) =>
                  exists
                    (r0 : T) 
                  (n : nat) 
                  (pre_wipe : State),
                    loopinv (start + n) r0 a' pre_wipe /\
                    n <= S count /\
                    wipe pre_wipe state'' |} rv state')
      exists a'.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:T
Lexec:Marker "after" (body start acc)
a:unit
state0:State
H2:pre
  {|
  pre := loopinv (start + 1) r a' state0;
  post := fun (r' : T) (state'' : State) =>
          loopinv (start + S count) r' a' state'';
  recovered := fun (_ : R) (state'' : State) =>
               exists
                 (r0 : T) 
               (n : nat) 
               (pre_wipe : State),
                 loopinv 
                   (start + n) r0 a' pre_wipe /\
                 n <= S count /\
                 wipe pre_wipe state'' |}
pre
  (for_range_spec loopinv wipe count 
     (start + 1) r a' state0) /\
(forall (v : T) (state' : State),
 post
   (for_range_spec loopinv wipe count 
      (start + 1) r a' state0) v state' ->
 post
   {|
   pre := loopinv (start + 1) r a' state0;
   post := fun (r' : T) (state'' : State) =>
           loopinv (start + S count) r' a' state'';
   recovered := fun (_ : R) (state'' : State) =>
                exists
                  (r0 : T) 
                (n : nat) 
                (pre_wipe : State),
                  loopinv (start + n) r0 a' pre_wipe /\
                  n <= S count /\
                  wipe pre_wipe state'' |} v state') /\
(forall (rv : R) (state' : State),
 recovered
   (for_range_spec loopinv wipe count 
      (start + 1) r a' state0) rv state' ->
 recovered
   {|
   pre := loopinv (start + 1) r a' state0;
   post := fun (r' : T) (state'' : State) =>
           loopinv (start + S count) r' a' state'';
   recovered := fun (_ : R) (state'' : State) =>
                exists
                  (r0 : T) 
                (n : nat) 
                (pre_wipe : State),
                  loopinv (start + n) r0 a' pre_wipe /\
                  n <= S count /\
                  wipe pre_wipe state'' |} rv state')
      simpl.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:T
Lexec:Marker "after" (body start acc)
a:unit
state0:State
H2:pre
  {|
  pre := loopinv (start + 1) r a' state0;
  post := fun (r' : T) (state'' : State) =>
          loopinv (start + S count) r' a' state'';
  recovered := fun (_ : R) (state'' : State) =>
               exists
                 (r0 : T) 
               (n : nat) 
               (pre_wipe : State),
                 loopinv 
                   (start + n) r0 a' pre_wipe /\
                 n <= S count /\
                 wipe pre_wipe state'' |}
loopinv (start + 1) r a' state0 /\
(forall (v : T) (state' : State),
 loopinv (start + 1 + count) v a' state' ->
 loopinv (start + S count) v a' state') /\
(R ->
 forall state' : State,
 (exists (r : T) (n : nat) 
  (pre_wipe : State),
    loopinv (start + 1 + n) r a' pre_wipe /\
    n <= count /\ wipe pre_wipe state') ->
 exists (r : T) (n : nat) 
 (pre_wipe : State),
   loopinv (start + n) r a' pre_wipe /\
   n <= S count /\ wipe pre_wipe state')
      intuition eauto.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:T
Lexec:Marker "after" (body start acc)
a:unit
state0:State
H2:pre
  {|
  pre := loopinv (start + 1) r a' state0;
  post := fun (r' : T) (state'' : State) =>
          loopinv (start + S count) r' a' state'';
  recovered := fun (_ : R) (state'' : State) =>
               exists
                 (r0 : T) 
               (n : nat) 
               (pre_wipe : State),
                 loopinv 
                   (start + n) r0 a' pre_wipe /\
                 n <= S count /\
                 wipe pre_wipe state'' |}
v:T
state':State
H3:loopinv (start + 1 + count) v a' state'
loopinv (start + S count) v a' state'
T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:T
Lexec:Marker "after" (body start acc)
a:unit
state0:State
H2:pre
  {|
  pre := loopinv (start + 1) r a' state0;
  post := fun (r' : T) (state'' : State) =>
          loopinv (start + S count) r' a' state'';
  recovered := fun (_ : R) (state'' : State) =>
               exists
                 (r0 : T) 
               (n : nat) 
               (pre_wipe : State),
                 loopinv 
                   (start + n) r0 a' pre_wipe /\
                 n <= S count /\
                 wipe pre_wipe state'' |}
rv:R
state':State
r0:T
n:nat
pre_wipe:State
H3:loopinv (start + 1 + n) r0 a' pre_wipe
H4:n <= count
H5:wipe pre_wipe state'
exists (r : T) (n : nat) 
(pre_wipe : State),
  loopinv (start + n) r a' pre_wipe /\
  n <= S count /\ wipe pre_wipe state'

      *T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:T
Lexec:Marker "after" (body start acc)
a:unit
state0:State
H2:pre
  {|
  pre := loopinv (start + 1) r a' state0;
  post := fun (r' : T) (state'' : State) =>
          loopinv (start + S count) r' a' state'';
  recovered := fun (_ : R) (state'' : State) =>
               exists
                 (r0 : T) 
               (n : nat) 
               (pre_wipe : State),
                 loopinv 
                   (start + n) r0 a' pre_wipe /\
                 n <= S count /\
                 wipe pre_wipe state'' |}
v:T
state':State
H3:loopinv (start + 1 + count) v a' state'
loopinv (start + S count) v a' state' replace (start + S count) with (start + 1 + count) by lia.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:T
Lexec:Marker "after" (body start acc)
a:unit
state0:State
H2:pre
  {|
  pre := loopinv (start + 1) r a' state0;
  post := fun (r' : T) (state'' : State) =>
          loopinv (start + S count) r' a' state'';
  recovered := fun (_ : R) (state'' : State) =>
               exists
                 (r0 : T) 
               (n : nat) 
               (pre_wipe : State),
                 loopinv 
                   (start + n) r0 a' pre_wipe /\
                 n <= S count /\
                 wipe pre_wipe state'' |}
v:T
state':State
H3:loopinv (start + 1 + count) v a' state'
loopinv (start + 1 + count) v a' state'
        eauto.

      *T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:T
Lexec:Marker "after" (body start acc)
a:unit
state0:State
H2:pre
  {|
  pre := loopinv (start + 1) r a' state0;
  post := fun (r' : T) (state'' : State) =>
          loopinv (start + S count) r' a' state'';
  recovered := fun (_ : R) (state'' : State) =>
               exists
                 (r0 : T) 
               (n : nat) 
               (pre_wipe : State),
                 loopinv 
                   (start + n) r0 a' pre_wipe /\
                 n <= S count /\
                 wipe pre_wipe state'' |}
rv:R
state':State
r0:T
n:nat
pre_wipe:State
H3:loopinv (start + 1 + n) r0 a' pre_wipe
H4:n <= count
H5:wipe pre_wipe state'
exists (r : T) (n : nat) 
(pre_wipe : State),
  loopinv (start + n) r a' pre_wipe /\
  n <= S count /\ wipe pre_wipe state' exists r0, (n+1), pre_wipe.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:T
Lexec:Marker "after" (body start acc)
a:unit
state0:State
H2:pre
  {|
  pre := loopinv (start + 1) r a' state0;
  post := fun (r' : T) (state'' : State) =>
          loopinv (start + S count) r' a' state'';
  recovered := fun (_ : R) (state'' : State) =>
               exists
                 (r0 : T) 
               (n : nat) 
               (pre_wipe : State),
                 loopinv 
                   (start + n) r0 a' pre_wipe /\
                 n <= S count /\
                 wipe pre_wipe state'' |}
rv:R
state':State
r0:T
n:nat
pre_wipe:State
H3:loopinv (start + 1 + n) r0 a' pre_wipe
H4:n <= count
H5:wipe pre_wipe state'
loopinv (start + (n + 1)) r0 a' pre_wipe /\
n + 1 <= S count /\ wipe pre_wipe state'
        intuition eauto.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:T
Lexec:Marker "after" (body start acc)
a:unit
state0:State
H2:pre
  {|
  pre := loopinv (start + 1) r a' state0;
  post := fun (r' : T) (state'' : State) =>
          loopinv (start + S count) r' a' state'';
  recovered := fun (_ : R) (state'' : State) =>
               exists
                 (r0 : T) 
               (n : nat) 
               (pre_wipe : State),
                 loopinv 
                   (start + n) r0 a' pre_wipe /\
                 n <= S count /\
                 wipe pre_wipe state'' |}
rv:R
state':State
r0:T
n:nat
pre_wipe:State
H3:loopinv (start + 1 + n) r0 a' pre_wipe
H4:n <= count
H5:wipe pre_wipe state'
loopinv (start + (n + 1)) r0 a' pre_wipe
T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:T
Lexec:Marker "after" (body start acc)
a:unit
state0:State
H2:pre
  {|
  pre := loopinv (start + 1) r a' state0;
  post := fun (r' : T) (state'' : State) =>
          loopinv (start + S count) r' a' state'';
  recovered := fun (_ : R) (state'' : State) =>
               exists
                 (r0 : T) 
               (n : nat) 
               (pre_wipe : State),
                 loopinv 
                   (start + n) r0 a' pre_wipe /\
                 n <= S count /\
                 wipe pre_wipe state'' |}
rv:R
state':State
r0:T
n:nat
pre_wipe:State
H3:loopinv (start + 1 + n) r0 a' pre_wipe
H4:n <= count
H5:wipe pre_wipe state'
n + 1 <= S count
        {T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:T
Lexec:Marker "after" (body start acc)
a:unit
state0:State
H2:pre
  {|
  pre := loopinv (start + 1) r a' state0;
  post := fun (r' : T) (state'' : State) =>
          loopinv (start + S count) r' a' state'';
  recovered := fun (_ : R) (state'' : State) =>
               exists
                 (r0 : T) 
               (n : nat) 
               (pre_wipe : State),
                 loopinv 
                   (start + n) r0 a' pre_wipe /\
                 n <= S count /\
                 wipe pre_wipe state'' |}
rv:R
state':State
r0:T
n:nat
pre_wipe:State
H3:loopinv (start + 1 + n) r0 a' pre_wipe
H4:n <= count
H5:wipe pre_wipe state'
loopinv (start + (n + 1)) r0 a' pre_wipe replace (start + (n+1)) with (start + 1 + n) by lia.T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:T
Lexec:Marker "after" (body start acc)
a:unit
state0:State
H2:pre
  {|
  pre := loopinv (start + 1) r a' state0;
  post := fun (r' : T) (state'' : State) =>
          loopinv (start + S count) r' a' state'';
  recovered := fun (_ : R) (state'' : State) =>
               exists
                 (r0 : T) 
               (n : nat) 
               (pre_wipe : State),
                 loopinv 
                   (start + n) r0 a' pre_wipe /\
                 n <= S count /\
                 wipe pre_wipe state'' |}
rv:R
state':State
r0:T
n:nat
pre_wipe:State
H3:loopinv (start + 1 + n) r0 a' pre_wipe
H4:n <= count
H5:wipe pre_wipe state'
loopinv (start + 1 + n) r0 a' pre_wipe eauto. }T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:T
Lexec:Marker "after" (body start acc)
a:unit
state0:State
H2:pre
  {|
  pre := loopinv (start + 1) r a' state0;
  post := fun (r' : T) (state'' : State) =>
          loopinv (start + S count) r' a' state'';
  recovered := fun (_ : R) (state'' : State) =>
               exists
                 (r0 : T) 
               (n : nat) 
               (pre_wipe : State),
                 loopinv 
                   (start + n) r0 a' pre_wipe /\
                 n <= S count /\
                 wipe pre_wipe state'' |}
rv:R
state':State
r0:T
n:nat
pre_wipe:State
H3:loopinv (start + 1 + n) r0 a' pre_wipe
H4:n <= count
H5:wipe pre_wipe state'
n + 1 <= S count
        {T, A, State:Type
loopinv:nat -> T -> A -> State -> Prop
wipe:State -> State -> Prop
body:nat -> T -> proc T
R:Type
recover:proc R
abstr:Abstraction State
count:nat
IHcount:forall (start : nat) (acc : T),
rec_wipe recover abstr wipe ->
(forall (n : nat) (acc0 : T),
 S n <= start + count ->
 proc_spec
   (for_range_spec loopinv wipe 1 n acc0)
   (body n acc0) recover abstr) ->
proc_spec
  (for_range_spec loopinv wipe count start
     acc) (for_range start count body acc)
  recover abstr
start:nat
acc:T
H:rec_wipe recover abstr wipe
H0:forall (n : nat) (acc : T),
S n <= start + S count ->
proc_spec (for_range_spec loopinv wipe 1 n acc)
  (body n acc) recover abstr
H0':proc_spec
  (for_range_spec loopinv wipe 1 start acc)
  (body start acc) recover abstr
a':A
state:State
H1:loopinv start acc a' state
r:T
Lexec:Marker "after" (body start acc)
a:unit
state0:State
H2:pre
  {|
  pre := loopinv (start + 1) r a' state0;
  post := fun (r' : T) (state'' : State) =>
          loopinv (start + S count) r' a' state'';
  recovered := fun (_ : R) (state'' : State) =>
               exists
                 (r0 : T) 
               (n : nat) 
               (pre_wipe : State),
                 loopinv 
                   (start + n) r0 a' pre_wipe /\
                 n <= S count /\
                 wipe pre_wipe state'' |}
rv:R
state':State
r0:T
n:nat
pre_wipe:State
H3:loopinv (start + 1 + n) r0 a' pre_wipe
H4:n <= count
H5:wipe pre_wipe state'
n + 1 <= S count lia. }
Qed.