Library Loop_Assertions


Loop example --- "program assertions" version

@author Patryk Czarnik
Example "program with loop". In fact, a single method is analysed and verified here.
In this version we use a bit generalised framework from ProgramAssertions to organise state specifications (those "assertions") and infer partial program correctness from properties of single state transitions.
Require Import Common.
Require Import Semantics.
Require Import ArithOps.
Require Import Numeric.
Require Import ProgramStructures.
Require Import ProgramAssertions.

Require Import Relations.
Require Import List.
Require Import ZArith.

Modules used

We take an instance of SEMATICS module. All other modules result from it.
Declare Module PASSERT : PROGRAM_ASSERTIONS_W_CONSTRUCTORS.
Module SF := PASSERT.M_Sem_Frame.
Module AllStr := SF.M_AllStructures.
Module P := AllStr.M_Program.
Module PS := P.M_ProgramStructures.
Module PSF := P.M_ProgramStructuresFacts.
Module VAT := PS.M_ValuesAndTypes.
Module RS := AllStr.M_RuntimeStructures.
Module SSOP := SF.M_Sem_Stackop.
Module SVAR := SF.M_Sem_Var.
Module SCOND := SF.M_Sem_Cond.
Module ARS := AllStr.M_Arithmetics.
Module RSF := SF.M_AllStructures.M_RuntimeStructuresFacts.
Module H := RS.M_Heap.
Module HF := SF.M_AllStructures.M_HeapFacts.
Module INum := VAT.M_Numeric_Int.

Import VAT.
Import PS.
Import PSF.
Import P.
Import RS.
Import ARS.
Import ArithmeticOperators.

Open Local Scope Z_scope.
Import ListNotations.

Load "Tactics.v".

Definition intArith := ARS.arithmeticForKind KInt.

Module M_IntNumProperties := NumericProperties M_Numeric_Int.

Section LoopExample.
Local Open Scope Z_scope.
Import List.ListNotations.

The program and the properties to verify

Parameter n

Parameter n: Z.
Definition max := 2147483648%Z.
Hypothesis n_positive: n > 0.
Hypothesis n2_small: n × n < INum.half_base.
Hypothesis n_small: n < max.

Program

Method to be verified as printed by javap -v: 
 0: iconst_0      
 1: istore_0      
 2: bipush        50
 4: istore_1      
 5: iconst_0      
 6: istore_2      
 7: iload_0       
 8: iload_1       
 9: if_icmpge     26
12: iload_0       
13: iload_2       
14: iadd          
15: istore_2      
16: iinc          0, 1
19: iload_0       
20: iload_2       
21: iadd          
22: istore_2      
23: goto          7
26: iload_2       
27: ireturn
Method code translated to CoJaq (positions recalculated to consecutive numbers, 50 generalised to n).
Definition code: P.TCode := P.codeFromList
  [ I_Frame (FI_Stackop (SI_Const KInt (VInt (INum.zero))));
    I_Frame (FI_Var (VI_Store VIKInt var0));
    I_Frame (FI_Stackop (SI_Const KInt (VInt (INum.const n))));
    I_Frame (FI_Var (VI_Store VIKInt var1));
    I_Frame (FI_Stackop (SI_Const KInt (VInt (INum.zero))));
    I_Frame (FI_Var (VI_Store VIKInt var2));
    I_Frame (FI_Var (VI_Load VIKInt var0));
    I_Frame (FI_Var (VI_Load VIKInt var1));
    I_Frame (FI_Cond (CI_Cmp KInt ArithmeticOperators.CmpOp_ge (offsetFromPosition 19%nat)));
    I_Frame (FI_Var (VI_Load VIKInt var0));
    I_Frame (FI_Var (VI_Load VIKInt var2));
    I_Frame (FI_Stackop (SI_Binop KInt ArithmeticOperators.BinOp_add));
    I_Frame (FI_Var (VI_Store VIKInt var2));
    I_Frame (FI_Var (VI_Inc var0 (INum.const 1)));
    I_Frame (FI_Var (VI_Load VIKInt var0));
    I_Frame (FI_Var (VI_Load VIKInt var2));
    I_Frame (FI_Stackop (SI_Binop KInt ArithmeticOperators.BinOp_add));
    I_Frame (FI_Var (VI_Store VIKInt var2));
    I_Frame (FI_Cond (CI_Goto (offsetFromPosition 6%nat)));
    I_Frame (FI_Var (VI_Load VIKInt var2));
    I_Return (Some KInt)
  ].

The initial state


Definition pc0: TPC := pcFromPosition 0.
Definition vars0: TVars := varsEmpty.
Definition sk0: TLocalStack := [].
Definition frame0: TFrame := frameMake vars0 sk0 pc0.

The method will compute n^2. We are going to prove the partial correctness of the method expressed: if the program goes to the last instruction, the value n^2 must be at the top of the stack. In details: 
forall frameF,
  pcToPosition (frameGetPC frameF) = 20%nat ->
  SF.stepsFrame code frame0 frameF ->
  exists res,
  frameGetLocalStack frameF = [(VInt res)] /\ INum.toZ res = (n * n).

Basic lemmas and auxiliary definitions

Lemmas related to arithmetics


Lemma half_base_max: INum.half_base = max.
Proof.
  unfold INum.half_base.
  unfold INum.power.
  simpl.
  unfold Z.pow_pos.
  simpl.
  reflexivity.
Qed.

Lemma base_max: INum.base = max + max.
Proof.
  unfold INum.base.
  rewrite half_base_max.
  ring.
Qed.

Lemma add1_small: ∀ i,
  0 ≤ i →
  i < n →
  i + 1 < INum.half_base.
Proof.
  rewrite half_base_max.
  intros.
  omega.
Qed.

Lemma add_i2_i_small: ∀ i,
  0 ≤ i →
  i < n →
  i×i + i < INum.half_base.
Proof.
  rewrite half_base_max.
  intros.
  rewrite <- (Z.mul_1_l i) at 3.
  rewrite <- Z.mul_add_distr_r.
  apply Z.le_lt_trans with (n×n).
  apply Zmult_le_compat.
  omega.
  omega.
  omega.
  assumption.
  assumption.
Qed.

Lemma add2_small: ∀ i,
  0 ≤ i →
  i < n →
  i + 1 + (i × i + i) < INum.half_base.
Proof.
  rewrite half_base_max.
  intros.
  apply Z.le_lt_trans with (n×n).
  replace (i+1+(i×i+i)) with ((i+1)*(i+1)) by ring.
  apply Zmult_le_compat.
  omega.
  omega.
  omega.
  omega.
  assumption.
Qed.

Lemma add_add: ∀ x y,
  INum.toZ x ≥ 0 → INum.toZ y ≥ 0 →
  (INum.toZ x) + (INum.toZ y) < INum.half_base →
  INum.toZ (INum.add x y) = (INum.toZ x) + (INum.toZ y).
Proof.
  intros.
  rewrite INum.add_prop.
  unfold INum.smod.
  rewrite Zmod_small.
  rewrite H1.
  reflexivity.
  rewrite half_base_max in ×.
  rewrite base_max in ×.
  omega.
Qed.

Auxiliary definitions

to make the assertions more compact.
Stack values are all ints and are equal to the given int list.
Inductive stack_values_ind: TLocalStack → list Z → Prop :=
  | stack_values_nil:
    stack_values_ind [] []
  | stack_values_cons: ∀ num vals i is,
    stack_values_ind vals is →
    INum.toZ num = i →
    stack_values_ind ((VInt num)::vals) (i::is)
.

Definition stack_values (frame: TFrame) (is: list Z): Prop :=
  stack_values_ind (frameGetLocalStack frame) is.

Variable holds an int which value is equal to i.
Inductive var_value : TFrame → TVar → Z → Prop :=
  | var_value_def: ∀ vars var sk pc num i,
    varsGet var vars = Some (VVInt num) →
    INum.toZ num = i →
    var_value (frameMake vars sk pc) var i.

Lemmas and tactics


Lemma stack_values_other_fields: ∀ l sk vars1 vars2 pc1 pc2,
  stack_values (frameMake vars1 sk pc1) l →
  stack_values (frameMake vars2 sk pc2) l.
  Proof.
    unfold stack_values.
    simpl.
    intros.
    induction H.
    constructor.
    constructor.
    assumption.
    assumption.
  Qed.

Lemma stack_value_from_var: ∀ i v vv var tl sk vars1 vars2 pc1 pc2,
  varsGet var vars1 = Some vv →
  ValVarMapping v (One vv) →
  var_value (frameMake vars1 sk pc1) var i →
  stack_values (frameMake vars1 sk pc1) tl →
  stack_values (frameMake vars2 (v::sk) pc2) (i::tl).
Proof.
  unfold stack_values.
  simpl.
  intros.
  inversion H1; clear H1.
  rewrite H in H8; clear H.
  injection H8; clear H8; intros.
  subst.
  inversion H0; clear H0; subst.
  constructor.
  assumption.
  reflexivity.
Qed.

Lemma var_value_other_fields:
  ∀ var i vars sk1 sk2 pc1 pc2,
  var_value (frameMake vars sk1 pc1) var i →
  var_value (frameMake vars sk2 pc2) var i.
Proof.
  intros.
  inversion H; subst; clear H.
  econstructor.
  eassumption.
  reflexivity.
Qed.

Lemma var_set_this:
  ∀ var i num vars sk pc,
  (INum.toZ num) = i →
  var_value (frameMake (varsSet var (VVInt num) vars) sk pc) var i.
Proof.
  intros.
  econstructor.
  apply PvarsSetGet.
  apply H.
Qed.

Lemma var_set_other:
  ∀ varA varB i val vars sk1 sk2 pc1 pc2,
  varB ≠ varA →
  var_value (frameMake vars sk1 pc1) varA i →
  var_value (frameMake (varsSet varB val vars) sk2 pc2) varA i.
Proof.
  intros.
  inversion H0; subst; clear H0.
  econstructor.
  rewrite <- PvarsSetGetOther.
  eassumption.
  assumption.
  reflexivity.
Qed.

Ltac de_step :=
  match goal with
  | [Hstep: (SF.stepFrame code ?frame ?frame') |- _] ⇒
    inversion Hstep; clear Hstep; simpl in *; subst;
    try match goal with
    | [H: (getInstruction code ?pc = Some ?instr) |- _] ⇒
      unfold code in H;
      rewrite PgetInstructionIffNth in H;
      rewrite PpositionPc in H;
      simpl in H;
      simplify_eq H;
      try (clear H; intros);
      repeat subst
    | _ ⇒ fail
    end
  | _ ⇒ fail
  end.

Ltac de_step2 :=
  de_step;
  match goal with
  | [HsemFrame: (SF.semFrame code ?instr ?frame ?frame') |- _] ⇒
    inversion HsemFrame; subst; clear HsemFrame
  | _ ⇒ fail
  end.

Ltac do_next :=
  unfold code;
  simpl;
  rewrite PcodeFromList_next_pc;
  reflexivity.

Ltac destruct_frame f :=
  destruct f as [vars sk pc];
  simpl in *;
  subst.

Ltac destruct_stack_values :=
  repeat
    match goal with
    | [Hfold: (stack_values ?frame ?is) |- _] ⇒
      unfold stack_values in Hfold; simpl in Hfold
    | [Hind: (stack_values_ind ?vals ?is) |- _] ⇒
      inversion Hind; clear Hind; subst
    end.

Ltac doInversionLoad :=
  match goal with
  | [HsemVar: SF.M_Sem_Var.semVar
      (VI_Load VIKInt ?var) (?vs1, ?vars1) (?vs2, ?vars2)
    |- _] ⇒
      apply SVAR.PSemVarInversion_load_1 in HsemVar;
      [destruct HsemVar as [v HsemVar];
       destruct HsemVar as [vv HsemVar];
       decompose [and] HsemVar; clear HsemVar; subst
      | constructor]
  | _ ⇒ fail
  end.

Ltac doInversionStore :=
  match goal with
  | [HsemVar: SF.M_Sem_Var.semVar
      (VI_Store VIKInt ?var1) (?vs1, ?vars) (?vs2, ?vars2)
    |- _] ⇒
      apply SVAR.PSemVarInversion_store_1 in HsemVar;
      [destruct HsemVar as [v HsemVar];
       destruct HsemVar as [vv HsemVar];
       decompose [and] HsemVar; clear HsemVar; subst
      | constructor]
  | _ ⇒ fail
  end.

Ltac doFiniteStack :=
  match goal with
  | [HstackTop: RSF.stackTopValues ?vs1 ?vs2 ?sk1 ?sk2
    |- _] ⇒
      inversion HstackTop; clear HstackTop; subst
  | _ ⇒ fail
  end;
  match goal with
  | [Happ: _ ++ _ = _ ∧ _ ++ _ = _
    |- _] ⇒
      decompose [and] Happ; clear Happ;
      simpl in *;
      subst
  | _ ⇒ idtac
  end;
  repeat match goal with
  | [Hcons: _ :: _ = _ :: _
    |- _] ⇒
      injection Hcons; clear Hcons; intros;
      subst
  | _ ⇒ idtac
  end.

Lemma range_pos: ∀ i,
  i ≥ 0 →
  i < max →
  INum.range i.
Proof.
  unfold INum.range.
  unfold max.
  intros.
  unfold INum.half_base.
  unfold INum.power.
  simpl.
  unfold Z.pow_pos.
  simpl.
  omega.
Qed.

Lemma const1: INum.toZ (INum.const 1) = 1.
Proof.
  apply INum.const_prop.
  apply range_pos.
  omega.
  unfold max.
  omega.
Qed.

Lemma constn: INum.toZ (INum.const n) = n.
Proof.
  apply INum.const_prop.
  apply range_pos.
  omega.
  assumption.
Qed.

Lemma constLemma: ∀ k val vars sk n_pc frame',
  SF.semFrame code (FI_Stackop (SI_Const k val))
     (frameMake vars sk (pcFromPosition n_pc)) frame'
  → frame' = Result (frameMake vars (val::sk) (pcFromPosition (S n_pc))).
Proof.
  intros.
  inversion H; subst; clear H.
  unfold code; rewrite PcodeFromList_next_pc.
  inversion H4; subst; clear H4.
  inversion H6; subst; clear H6.
  decompose [and] H; clear H.
  simpl in ×.
  subst.
  reflexivity.

  inversion H5.
Qed.

Assertion for each position in program

Information about position is now omitted, as it is easily deduced by the assertions framework.
Definition s0_prop (frame: TFrame) :=
  frameGetLocalStack frame = [].

Definition s1_prop (frame: TFrame) :=
  frameGetLocalStack frame = [VInt (INum.zero)].

Definition s2_prop (frame: TFrame) :=
  frameGetLocalStack frame = []
  ∧ var_value frame var0 0.

Definition s3_prop (frame: TFrame) :=
  frameGetLocalStack frame = [VInt (INum.const n)]
  ∧ var_value frame var0 0.

Definition s4_prop frame :=
  frameGetLocalStack frame = []
  ∧ var_value frame var0 0
  ∧ var_value frame var1 n.

Definition s5_prop frame :=
  frameGetLocalStack frame = [VInt (INum.zero)]
  ∧ var_value frame var0 0
  ∧ var_value frame var1 n.

State after execution of instruction 5
Definition s5_post_prop frame :=
  frameGetPC frame = pcFromPosition 6%nat
  ∧ frameGetLocalStack frame = []
  ∧ var_value frame var0 0
  ∧ var_value frame var1 n
  ∧ var_value frame var2 0.

State before instruction 6, (loop invariant)
Definition s6_prop frame :=
  ∃ i, ∃ r,
    stack_values frame []
    ∧ var_value frame var0 i
    ∧ var_value frame var1 n
    ∧ var_value frame var2 r
    ∧ r = i×i
    ∧ 0 ≤ i
    ∧ i ≤ n.

Definition s7_prop frame :=
  ∃ i, ∃ r,
    stack_values frame [i]
    ∧ var_value frame var0 i
    ∧ var_value frame var1 n
    ∧ var_value frame var2 r
    ∧ r = i×i
    ∧ 0 ≤ i
    ∧ i ≤ n.

Definition s8_prop frame :=
  ∃ i, ∃ r,
    stack_values frame [n; i]
    ∧ var_value frame var0 i
    ∧ var_value frame var1 n
    ∧ var_value frame var2 r
    ∧ r = i×i
    ∧ 0 ≤ i
    ∧ i ≤ n.

Definition s8_post_prop frame :=
  ∃ i, ∃ r,
    stack_values frame []
    ∧ var_value frame var0 i
    ∧ var_value frame var1 n
    ∧ var_value frame var2 r
    ∧ r = i×i
    ∧ 0 ≤ i
    ∧ (frameGetPC frame = pcFromPosition 9%nat
         ∧ i < n
      ∨ frameGetPC frame = pcFromPosition 19%nat
         ∧ i = n).

Definition s9_prop frame :=
  ∃ i, ∃ r,
    stack_values frame []
    ∧ var_value frame var0 i
    ∧ var_value frame var1 n
    ∧ var_value frame var2 r
    ∧ r = i×i
    ∧ 0 ≤ i
    ∧ i < n.

Definition s10_prop frame :=
  ∃ i, ∃ r,
    stack_values frame [i]
    ∧ var_value frame var0 i
    ∧ var_value frame var1 n
    ∧ var_value frame var2 r
    ∧ r = i×i
    ∧ 0 ≤ i
    ∧ i < n.

Definition s11_prop frame :=
  ∃ i, ∃ r,
    stack_values frame [r; i]
    ∧ var_value frame var0 i
    ∧ var_value frame var1 n
    ∧ var_value frame var2 r
    ∧ r = i×i
    ∧ 0 ≤ i
    ∧ i < n.

Definition s12_prop frame :=
  ∃ i, ∃ r,
    stack_values frame [r]
    ∧ var_value frame var0 i
    ∧ var_value frame var1 n
    ∧ r = i×i + i
    ∧ 0 ≤ i
    ∧ i < n.

Definition s13_prop frame :=
  ∃ i, ∃ r,
    stack_values frame []
    ∧ var_value frame var0 i
    ∧ var_value frame var1 n
    ∧ var_value frame var2 r
    ∧ r = i×i + i
    ∧ 0 ≤ i
    ∧ i < n.

Definition s14_prop frame :=
  ∃ i, ∃ r,
    stack_values frame []
    ∧ var_value frame var0 (i+1)
    ∧ var_value frame var1 n
    ∧ var_value frame var2 r
    ∧ r = i×i + i
    ∧ 0 ≤ i
    ∧ i < n.

Definition s15_prop frame :=
  ∃ i, ∃ r,
    stack_values frame [i+1]
    ∧ var_value frame var0 (i+1)
    ∧ var_value frame var1 n
    ∧ var_value frame var2 r
    ∧ r = i×i + i
    ∧ 0 ≤ i
    ∧ i < n.

Definition s16_prop frame :=
  ∃ i, ∃ r,
    stack_values frame [r; i+1]
    ∧ var_value frame var0 (i+1)
    ∧ var_value frame var1 n
    ∧ var_value frame var2 r
    ∧ r = i×i + i
    ∧ 0 ≤ i
    ∧ i < n.

Definition s17_prop frame :=
  ∃ i, ∃ r,
    stack_values frame [r]
    ∧ var_value frame var0 (i+1)
    ∧ var_value frame var1 n
    ∧ r = i×i + i + (i + 1)
    ∧ 0 ≤ i
    ∧ i < n.

Definition s18_prop frame :=
  ∃ i, ∃ r,
    stack_values frame []
    ∧ var_value frame var0 (i+1)
    ∧ var_value frame var1 n
    ∧ var_value frame var2 r
    ∧ r = i×i + i + (i + 1)
    ∧ 0 ≤ i
    ∧ i < n.

Definition s18_post_prop frame :=
  ∃ i, ∃ r,
    stack_values frame []
    ∧ var_value frame var0 i
    ∧ var_value frame var1 n
    ∧ var_value frame var2 r
    ∧ r = i×i
    ∧ 0 < i
    ∧ i ≤ n.

State after exitting the loop.
Definition s19_prop frame :=
  ∃ i, ∃ r,
    stack_values frame []
    ∧ var_value frame var0 i
    ∧ var_value frame var1 n
    ∧ var_value frame var2 r
    ∧ r = i×i
    ∧ 0 ≤ i
    ∧ i = n.

Final state of our analysis.
Definition s20_prop frame :=
  ∃ r,
    stack_values frame [r]
    ∧ r = n×n.

Here assertions are assigned to positions in the progra.
Definition lassertions :=
 [ s0_prop; s1_prop; s2_prop; s3_prop; s4_prop;
   s5_prop; s6_prop; s7_prop; s8_prop; s9_prop;
  s10_prop; s11_prop; s12_prop; s13_prop; s14_prop;
  s15_prop; s16_prop; s17_prop; s18_prop; s19_prop;
  s20_prop].

Definition specification := PASSERT.assertionsFromList lassertions.

Ltac get_assertion :=
  unfold PASSERT.getPositionedAssertion;
  unfold specification;
  repeat (rewrite PASSERT.PgetInstructionIffNth);
  repeat (rewrite PpositionPc);
  simpl.

Proofs of single transitions

The initial state obeys the first assertion
Lemma start_0: (PASSERT.getPositionedAssertion specification pc0) frame0.
Proof.
  unfold PASSERT.getPositionedAssertion.
  unfold specification.
  rewrite PASSERT.PgetInstructionIffNth.
  unfold pc0.
  rewrite PpositionPc.
  simpl.

  split.
  reflexivity.
  unfold s0_prop.
  unfold frame0.
  simpl.
  reflexivity.
Qed.

Lemma described_0: PASSERT.frameDescribed specification frame0.
Proof.
  unfold PASSERT.frameDescribed.
  ∃ pc0.
  apply start_0.
Qed.

Manual proof for each possible transition. const
Lemma trans_0_1: ∀ frame frame',
  (PASSERT.getPositionedAssertion specification (pcFromPosition 0)) frame →
  SF.stepFrame code frame frame' →
  (PASSERT.getPositionedAssertion specification (pcFromPosition 1)) frame'.
Proof.
  get_assertion.
  unfold s0_prop, s1_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step.
  apply constLemma in H0.
  injection_clear H0.
  subst frame'.
  simpl.
  intuition trivial.
Qed.

store var0
Lemma trans_1_2: ∀ frame frame',
  (PASSERT.getPositionedAssertion specification (pcFromPosition 1)) frame →
  SF.stepFrame code frame frame' →
  (PASSERT.getPositionedAssertion specification (pcFromPosition 2)) frame'.
Proof.
  get_assertion.
  unfold s1_prop, s2_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step2.
  split.
  do_next.

  doInversionStore.
  doFiniteStack.
  intuition.

  inversion H1; clear H1; subst.
  eapply var_set_this.
  apply INum.PzeroToZ.
Qed.

const
Lemma trans_2_3: ∀ frame frame',
  (PASSERT.getPositionedAssertion specification (pcFromPosition 2)) frame →
  SF.stepFrame code frame frame' →
  (PASSERT.getPositionedAssertion specification (pcFromPosition 3)) frame'.
Proof.
  get_assertion.
  unfold s2_prop, s3_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step.
  apply constLemma in H1.
  injection_clear H1.
  subst frame'.
  simpl.
  intuition.
  subst.
  reflexivity.
  eapply var_value_other_fields.
  eassumption.
Qed.

store
Lemma trans_3_4: ∀ frame frame',
  (PASSERT.getPositionedAssertion specification (pcFromPosition 3)) frame →
  SF.stepFrame code frame frame' →
  (PASSERT.getPositionedAssertion specification (pcFromPosition 4)) frame'.
Proof.
  get_assertion.
  unfold s3_prop, s4_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step2.
  split.
  do_next.
  decompose [and] H0; clear H0.
  doInversionStore.
  doFiniteStack.
  inversion H3; clear H3; subst.
  intuition.
  eapply var_set_other.
  auto using distinct_vars_0_1.
  eassumption.

  subst.
  eapply var_set_this.
  apply constn.
Qed.

const
Lemma trans_4_5: ∀ frame frame',
  (PASSERT.getPositionedAssertion specification (pcFromPosition 4)) frame →
  SF.stepFrame code frame frame' →
  (PASSERT.getPositionedAssertion specification (pcFromPosition 5)) frame'.
Proof.
  get_assertion.
  unfold s4_prop, s5_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step.
  apply constLemma in H1.
  injection_clear H1.
  subst frame'.
  simpl.
  intuition.
  subst.
  reflexivity.

  eapply var_value_other_fields.
  eassumption.
  eapply var_value_other_fields.
  eassumption.
Qed.

store var2
Lemma trans_5_post: ∀ frame frame',
  (PASSERT.getPositionedAssertion specification (pcFromPosition 5)) frame →
  SF.stepFrame code frame frame' →
  s5_post_prop frame'.
Proof.
  get_assertion.
  unfold s5_prop, s5_post_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step2.
  split.
  do_next.
  decompose [and] H0; clear H0.

  doInversionStore.
  doFiniteStack.
  inversion H4; clear H4; subst.
  intuition.

  eapply var_set_other.
  auto using distinct_vars_0_2.
  eassumption.

  eapply var_set_other.
  auto using distinct_vars_1_2.
  eassumption.

  eapply var_set_this.
  apply INum.PzeroToZ.
Qed.

An actual state description generalises to loop invariant.
Lemma post5_impl_pre6: ∀ frame,
  s5_post_prop frame →
  (PASSERT.getPositionedAssertion specification (pcFromPosition 6)) frame.
Proof.
  get_assertion.
  unfold s5_post_prop, s6_prop.
  intros frame Hprev.
  destruct Hprev.
  decompose [and] H0; clear H0.
  split.
  assumption.

  ∃ 0%Z.
  ∃ 0%Z.
  split.
  destruct frame.
  simpl in H1.
  subst.
  apply stack_values_nil.

  split.
  assumption.
  split.
  assumption.
  split.
  assumption.
  omega.
Qed.

load var0
Lemma trans_6_7: ∀ frame frame',
  (PASSERT.getPositionedAssertion specification (pcFromPosition 6)) frame →
  SF.stepFrame code frame frame' →
  (PASSERT.getPositionedAssertion specification (pcFromPosition 7)) frame'.
Proof.
  get_assertion.
  unfold s6_prop, s7_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step2.
  split.
  do_next.
  destruct H0 as [i].
  destruct H as [r].
  ∃ i.
  ∃ r.
  decompose [and] H; clear H.
  subst.
  doInversionLoad.
  doFiniteStack.
  intuition.
  eapply stack_value_from_var.
  eassumption.
  eassumption.
  eassumption.
  eassumption.

  eapply var_value_other_fields.
  eassumption.
  eapply var_value_other_fields.
  eassumption.
  eapply var_value_other_fields.
  eassumption.
Qed.

load var2
Lemma trans_7_8: ∀ frame frame',
  (PASSERT.getPositionedAssertion specification (pcFromPosition 7)) frame →
  SF.stepFrame code frame frame' →
  (PASSERT.getPositionedAssertion specification (pcFromPosition 8)) frame'.
Proof.
  get_assertion.
  unfold s7_prop, s8_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step2.
  split.
  do_next.
  destruct H0 as [i].
  destruct H as [r].
  ∃ i.
  ∃ r.
  decompose [and] H; clear H.
  doInversionLoad.
  doFiniteStack.
  subst.
  intuition.
  eapply stack_value_from_var.
  eassumption.
  eassumption.
  eassumption.
  eassumption.

  eapply var_value_other_fields.
  eassumption.
  eapply var_value_other_fields.
  eassumption.
  eapply var_value_other_fields.
  eassumption.
Qed.

cond ge
Lemma trans_8_post8: ∀ frame frame',
  (PASSERT.getPositionedAssertion specification (pcFromPosition 8)) frame →
  SF.stepFrame code frame frame' →
  s8_post_prop frame'.
Proof.
  get_assertion.
  unfold s8_prop, s8_post_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step2.
  destruct H0 as [i H0].
  destruct H0 as [r].
  ∃ i.
  ∃ r.
  decompose [and] H; clear H.
  destruct_stack_values.
  inversion H7; subst; clear H7.   decompose [and] H; clear H.

  inversion H6; subst; clear H6;
    simpl in *;
    injection H0; clear H0; intros;
    repeat subst;
    (intuition;
   
  [
    constructor
  |
    eapply var_value_other_fields;
    eassumption
  | eapply var_value_other_fields;
    eassumption
  | eapply var_value_other_fields;
    eassumption
  | idtac]).
  inversion H14; subst; clear H14.
  right.
  split.
  apply PmakeOffset_pc.
  apply M_IntNumProperties.is_ge_t_toZ_prop in H4.
  omega.
  inversion H14; subst; clear H14.
  left.
  split.
  do_next.
  apply M_IntNumProperties.is_ge_f_toZ_prop in H4.
  omega.
Qed.

Lemma post8_impl_9_or_19: ∀ frame,
  s8_post_prop frame →
  ((PASSERT.getPositionedAssertion specification (pcFromPosition 9)) frame
   ∨ (PASSERT.getPositionedAssertion specification (pcFromPosition 19)) frame).
Proof.
  get_assertion.
  unfold s8_post_prop.
  intros frame Hprev.
  destruct Hprev as [i Hprev].
  destruct Hprev as [r Hprev].
  decompose [and] Hprev; clear Hprev.
  destruct H6.
  left.
  destruct H5.
  unfold s9_prop.
  split.
  assumption.
  ∃ i.
  ∃ r.
  intuition.

  right.
  destruct H5.
  unfold s19_prop.
  split.
  assumption.
  ∃ i.
  ∃ r.
  intuition.
Qed.

load var0
Lemma trans_9_10: ∀ frame frame',
  (PASSERT.getPositionedAssertion specification (pcFromPosition 9)) frame →
  SF.stepFrame code frame frame' →
  (PASSERT.getPositionedAssertion specification (pcFromPosition 10)) frame'.
Proof.
  get_assertion.
  unfold s9_prop, s10_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step2.
  split.
  do_next.
  destruct H0 as [i].
  destruct H as [r].
  ∃ i.
  ∃ r.
  decompose [and] H; clear H.
  doInversionLoad.
  doFiniteStack.
  subst.
  intuition.
  eapply stack_value_from_var.
  eassumption.
  eassumption.
  eassumption.
  eassumption.

  eapply var_value_other_fields.
  eassumption.
  eapply var_value_other_fields.
  eassumption.
  eapply var_value_other_fields.
  eassumption.
Qed.

load var2
Lemma trans_10_11: ∀ frame frame',
  (PASSERT.getPositionedAssertion specification (pcFromPosition 10)) frame →
  SF.stepFrame code frame frame' →
  (PASSERT.getPositionedAssertion specification (pcFromPosition 11)) frame'.
Proof.
  get_assertion.
  unfold s10_prop, s11_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step2.
  split.
  do_next.
  destruct H0 as [i].
  destruct H as [r].
  ∃ i.
  ∃ r.
  decompose [and] H; clear H.
  doInversionLoad.
  doFiniteStack.
  subst.
  intuition.
  eapply stack_value_from_var.
  eassumption.
  eassumption.
  eassumption.
  eassumption.

  eapply var_value_other_fields.
  eassumption.
  eapply var_value_other_fields.
  eassumption.
  eapply var_value_other_fields.
  eassumption.
Qed.

add
Lemma trans_11_12: ∀ frame frame',
  (PASSERT.getPositionedAssertion specification (pcFromPosition 11)) frame →
  SF.stepFrame code frame frame' →
  (PASSERT.getPositionedAssertion specification (pcFromPosition 12)) frame'.
Proof.
  get_assertion.
  unfold s11_prop, s12_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step2.
  split.
  do_next.
  destruct H0 as [i].
  destruct H as [old_r].
  ∃ i.
  ∃ (old_r + i).
  decompose [and] H; clear H.
  inversion H6; subst; clear H6.
  destruct_stack_values.
  inversion H7; subst; clear H7.   decompose [and] H; clear H.
  simpl in ×.
  injection H0; clear H0; intros.
  repeat subst.
  intuition.
  inversion H11; subst; clear H11.   constructor.
  constructor.
  rewrite Z.add_comm at 1.
  rewrite <- H10.
  apply add_add.
  omega.
  rewrite H10.
  apply sqr_pos.
  rewrite H10.
  rewrite Z.add_comm at 1.
  apply add_i2_i_small.
  assumption.
  assumption.

  eapply var_value_other_fields.
  eassumption.
  eapply var_value_other_fields.
  eassumption.
Qed.

store var2
Lemma trans_12_13: ∀ frame frame',
  (PASSERT.getPositionedAssertion specification (pcFromPosition 12)) frame →
  SF.stepFrame code frame frame' →
  (PASSERT.getPositionedAssertion specification (pcFromPosition 13)) frame'.
Proof.
  get_assertion.
  unfold s12_prop, s13_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step2.
  split.
  do_next.
  destruct H0 as [i].
  destruct H as [r].
  ∃ i.
  ∃ r.
  decompose [and] H; clear H.
  subst.
  destruct_stack_values.
  doInversionStore.
  doFiniteStack.
  inversion H3; clear H3; subst.
  intuition.
  constructor.

  eapply var_set_other.
  auto using distinct_vars_0_2.
  eassumption.

  eapply var_set_other.
  auto using distinct_vars_1_2.
  eassumption.

  eapply var_set_this.
  assumption.
Qed.

iinc
Lemma trans_13_14: ∀ frame frame',
  (PASSERT.getPositionedAssertion specification (pcFromPosition 13)) frame →
  SF.stepFrame code frame frame' →
  (PASSERT.getPositionedAssertion specification (pcFromPosition 14)) frame'.
Proof.
  get_assertion.
  unfold s13_prop, s14_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step2.
  split.
  do_next.
  destruct H0 as [i].
  destruct H as [r].
  ∃ i.
  ∃ r.
  decompose [and] H; clear H.
  subst.

  inversion H6; clear H6; subst.
  doFiniteStack.
  subst sk'.
  intuition.

  inversion H2; clear H2.
  rewrite H10 in H12; clear H10.
  injection H12; clear H12; intros.
  repeat subst.
  eapply var_set_this.
  rewrite <- const1 at 2.
  apply add_add.
  omega.
  rewrite const1.
  omega.
  rewrite const1.
  apply add1_small.
  assumption.
  assumption.

  eauto using var_set_other, distinct_vars_0_1.
  eauto using var_set_other, distinct_vars_0_2.
Qed.

load var0
Lemma trans_14_15: ∀ frame frame',
  (PASSERT.getPositionedAssertion specification (pcFromPosition 14)) frame →
  SF.stepFrame code frame frame' →
  (PASSERT.getPositionedAssertion specification (pcFromPosition 15)) frame'.
Proof.
  get_assertion.
  unfold s14_prop, s15_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step2.
  split.
  do_next.
  destruct H0 as [i].
  destruct H as [r].
  ∃ i.
  ∃ r.
  decompose [and] H; clear H.
  doInversionLoad.
  doFiniteStack.
  subst.
  intuition.
  eapply stack_value_from_var.
  eassumption.
  eassumption.
  eassumption.
  eassumption.

  eapply var_value_other_fields.
  eassumption.
  eapply var_value_other_fields.
  eassumption.
  eapply var_value_other_fields.
  eassumption.
Qed.

load var2
Lemma trans_15_16: ∀ frame frame',
  (PASSERT.getPositionedAssertion specification (pcFromPosition 15)) frame →
  SF.stepFrame code frame frame' →
  (PASSERT.getPositionedAssertion specification (pcFromPosition 16)) frame'.
Proof.
  get_assertion.
  unfold s15_prop, s16_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step2.
  split.
  do_next.
  destruct H0 as [i].
  destruct H as [r].
  ∃ i.
  ∃ r.
  decompose [and] H; clear H.
  subst.
  doInversionLoad.
  doFiniteStack.
  intuition.
  eapply stack_value_from_var.
  eassumption.
  eassumption.
  eassumption.
  eassumption.

  eapply var_value_other_fields.
  eassumption.
  eapply var_value_other_fields.
  eassumption.
  eapply var_value_other_fields.
  eassumption.
Qed.

add
Lemma trans_16_17: ∀ frame frame',
  (PASSERT.getPositionedAssertion specification (pcFromPosition 16)) frame →
  SF.stepFrame code frame frame' →
  (PASSERT.getPositionedAssertion specification (pcFromPosition 17)) frame'.
Proof.
  get_assertion.
  unfold s16_prop, s17_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step2.
  split.
  do_next.
  destruct H0 as [i].
  destruct H as [old_r].
  ∃ i.
  ∃ (old_r + (i+1)).
  decompose [and] H; clear H.
  inversion H6; subst; clear H6.
  destruct_stack_values.
  inversion H7; subst; clear H7.   decompose [and] H; clear H.
  simpl in ×.
  injection H0; clear H0; intros.
  repeat subst.
  intuition.
  inversion H11; subst; clear H11.   constructor.
  constructor.
  rewrite Z.add_comm at 1.
  rewrite <- H10.
  rewrite <- H12.
  apply add_add.
  omega.
  rewrite H10.
  apply Z.le_ge.
  apply OMEGA2.
  apply Z.ge_le.
  apply sqr_pos.
  assumption.
  rewrite H10.
  rewrite H12.
  apply add2_small.
  assumption.
  assumption.

  eapply var_value_other_fields.
  eassumption.
  eapply var_value_other_fields.
  eassumption.
Qed.

store var2
Lemma trans_17_18: ∀ frame frame',
  (PASSERT.getPositionedAssertion specification (pcFromPosition 17)) frame →
  SF.stepFrame code frame frame' →
  (PASSERT.getPositionedAssertion specification (pcFromPosition 18)) frame'.
Proof.
  get_assertion.
  unfold s17_prop, s18_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step2.
  split.
  do_next.
  destruct H0 as [i].
  destruct H as [r].
  ∃ i.
  ∃ r.
  decompose [and] H; clear H.
  subst.
  destruct_stack_values.
  doInversionStore.
  doFiniteStack.
  inversion H3; clear H3; subst.
  intuition.

  constructor.

  eapply var_set_other.
  auto using distinct_vars_0_2.
  eassumption.

  eapply var_set_other.
  auto using distinct_vars_1_2.
  eassumption.

  eapply var_set_this.
  eassumption.
Qed.

goto
Lemma trans_18_6: ∀ frame frame',
  (PASSERT.getPositionedAssertion specification (pcFromPosition 18)) frame →
  SF.stepFrame code frame frame' →
  (PASSERT.getPositionedAssertion specification (pcFromPosition 6)) frame'.
Proof.
  get_assertion.
  unfold s18_prop, s6_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step2.
  inversion H6; clear H6; subst.   inversion H7; clear H7; subst.   decompose [and] H; clear H; simpl in *; repeat subst.

  split.
  apply PmakeOffset_pc.
  destruct H0 as [i].
  destruct H as [r].
  decompose [and] H; clear H.
  subst.
  ∃ (i+1).
  ∃ (Z.mul (i+1) (i+1)).
  intuition.

  eapply var_value_other_fields.
  eassumption.
  eapply var_value_other_fields.
  eassumption.

  replace (i × i + i + (i + 1)) with ((i + 1) × (i + 1)) in H3 by ring.
  eapply var_value_other_fields.
  eassumption.
Qed.

load
Lemma trans_19_20: ∀ frame frame',
  (PASSERT.getPositionedAssertion specification (pcFromPosition 19)) frame →
  SF.stepFrame code frame frame' →
  (PASSERT.getPositionedAssertion specification (pcFromPosition 20)) frame'.
Proof.
  get_assertion.
  unfold s19_prop, s20_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step2.
  split.
  do_next.
  destruct H0 as [i].
  destruct H as [r].
  ∃ r.
  decompose [and] H; clear H.
  subst.
  doInversionLoad.
  doFiniteStack.
  split.

  eapply stack_value_from_var.
  eassumption.
  eassumption.
  eassumption.
  eassumption.

  reflexivity.
Qed.

There is no step from instruction 20 I_Return (within the current frame).
Lemma final_20: ∀ frame frame',
  (PASSERT.getPositionedAssertion specification (pcFromPosition 20)) frame →
  SF.stepFrame code frame frame' →
  False.
Proof.
  get_assertion.
  unfold s20_prop.
  intros frame frame' Hprev Hstep.
  apply proj1 in Hprev.
  unfold code in Hstep.
  inversion Hstep; clear Hstep; subst; simpl in Hprev;
    rewrite PgetInstructionIffNth in H;
    rewrite Hprev in H; clear Hprev;
    rewrite PpositionPc in H;
    simpl in H;
    discriminate H.
Qed.

For each state described by any of the assertions, a step yields always to a state which is also described by an assertion from the given set.
Lemma singles: PASSERT.singleTransitions code specification.
Proof.
  unfold PASSERT.singleTransitions.
  intros frame1 frame2 Hprev Hstep.
  assert (LT := PASSERT.frameDescribed_inRange lassertions frame1 Hprev).
  apply PASSERT.frameDescribed_equiv in Hprev.
  destruct frame1 as [vars1 sk1 pc1].
  simpl in ×.
  rewrite <- (PpcPosition pc1) in Hprev.
  rewrite <- (PpcPosition pc1) in Hstep.
  revert Hprev Hstep LT.
  generalize (pcToPosition pc1).
  unfold PASSERT.frameDescribed.
  intros n Hprev Hstep LT.
  destruct n as [|n].   ∃ (pcFromPosition 1).
  eauto using trans_0_1.

  destruct n as [|n].   ∃ (pcFromPosition 2).
  eauto using trans_1_2.

  destruct n as [|n].   ∃ (pcFromPosition 3).
  eauto using trans_2_3.

  destruct n as [|n].   ∃ (pcFromPosition 4).
  eauto using trans_3_4.

  destruct n as [|n].   ∃ (pcFromPosition 5).
  eauto using trans_4_5.

  destruct n as [|n].   ∃ (pcFromPosition 6).
  eauto using trans_5_post, post5_impl_pre6.

  destruct n as [|n].   ∃ (pcFromPosition 7).
  eauto using trans_6_7.

  destruct n as [|n].   ∃ (pcFromPosition 8).
  eauto using trans_7_8.

  destruct n as [|n].     eapply trans_8_post8 in Hprev.
    apply post8_impl_9_or_19 in Hprev.
    destruct Hprev.     ∃ (pcFromPosition 9); eassumption.
    ∃ (pcFromPosition 19); eassumption.
    eassumption.

  destruct n as [|n].   ∃ (pcFromPosition 10).
  eauto using trans_9_10.

  destruct n as [|n].   ∃ (pcFromPosition 11).
  eauto using trans_10_11.

  destruct n as [|n].   ∃ (pcFromPosition 12).
  eauto using trans_11_12.

  destruct n as [|n].   ∃ (pcFromPosition 13).
  eauto using trans_12_13.

  destruct n as [|n].   ∃ (pcFromPosition 14).
  eauto using trans_13_14.

  destruct n as [|n].   ∃ (pcFromPosition 15).
  eauto using trans_14_15.

  destruct n as [|n].   ∃ (pcFromPosition 16).
  eauto using trans_15_16.

  destruct n as [|n].   ∃ (pcFromPosition 17).
  eauto using trans_16_17.

  destruct n as [|n].   ∃ (pcFromPosition 18).
  eauto using trans_17_18.

  destruct n as [|n].   ∃ (pcFromPosition 6).
  eauto using trans_18_6.

  destruct n as [|n].   ∃ (pcFromPosition 20).
  eauto using trans_19_20.

  destruct n as [|n].   destruct (final_20 _ frame2 Hprev).
    assumption.

  omega.
Qed.

Lemma s20: ∀ frame,
  PASSERT.frameDescribed specification frame →
  pcToPosition (frameGetPC frame) = 20%nat →
  s20_prop frame.
Proof.
  intros.
  apply PASSERT.frameDescribed_equiv in H.
  unfold PASSERT.frameDescribed2 in H.
  unfold PASSERT.getPositionedAssertion in H.
  unfold specification in H.
  rewrite PASSERT.PgetInstructionIffNth in H.
  rewrite H0 in H.
  simpl in H.
  tauto.
Qed.

The final conclusion: if control reaches to the instruction at position 20, the stack will contain integer equal to n×n.
Theorem partial_correctness: ∀ frameF,
  pcToPosition (frameGetPC frameF) = 20%nat →
  SF.stepsFrame code frame0 frameF →
  ∃ res,
  frameGetLocalStack frameF = [(VInt res)] ∧ INum.toZ res = (n × n).
Proof.
  intros.
Here we use the general theorem from ProgramAssertions.
  eapply PASSERT.multiTransitions in H0.
  apply s20 in H0.
  unfold s20_prop in H0.
  destruct H0 as [r].   decompose [and] H0; clear H0.
  inversion H1; clear H1.
  inversion H5; clear H5.
  ∃ num.
  subst.
  intuition assumption.
  assumption.
  apply singles.
  apply described_0.
Qed.
End LoopExample.