Library Loop

Loop example

@author Patryk Czarnik

Example "program with loop". In fact, a single method is analysed and verified here.

In this version we use the semantics definition directly.

Require Import Common.
Require Import Sem_Frame.
Require Import ArithOps.
Require Import Numeric.
Require Import ProgramStructures.

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 SF : 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).

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;
      match goal with
      | [He: (pcToPosition pc = _) |- _] ⇒
        rewrite He in H;
        simpl in H;
        simplify_eq H;
        try (clear H; intros);
        repeat subst
      | _ ⇒ fail
      end
    | _ ⇒ fail
    end
  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;
  intuition.

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 const0: INum.toZ (INum.zero) = 0.
Proof.
  apply INum.PzeroToZ.
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.

Assertion for each position in program

Each position in the method code is described with a specification of a general type TFrame -> Prop.

Definition s0_prop (frame: TFrame) :=
  pcToPosition (frameGetPC frame) = 0%nat
  ∧ frameGetLocalStack frame = [].

Definition s1_prop (frame: TFrame) :=
  pcToPosition (frameGetPC frame) = 1%nat
  ∧ frameGetLocalStack frame = [VInt (INum.zero)].

Definition s2_prop (frame: TFrame) :=
  pcToPosition (frameGetPC frame) = 2%nat
  ∧ frameGetLocalStack frame = []
  ∧ var_value frame var0 0.

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

Definition s4_prop (frame: TFrame) :=
  pcToPosition (frameGetPC frame) = 4%nat
  ∧ frameGetLocalStack frame = []
  ∧ var_value frame var0 0
  ∧ var_value frame var1 n.

Definition s5_prop (frame: TFrame) :=
  pcToPosition (frameGetPC frame) = 5%nat
  ∧ 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: TFrame) :=
  pcToPosition (frameGetPC frame) = 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)

Note here: i = \old(i) + 1

Definition s18_post_prop (frame: TFrame) :=
  pcToPosition (frameGetPC frame) = 6%nat
  ∧ ∃ 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: TFrame) :=
  pcToPosition (frameGetPC frame) = 19%nat
  ∧ ∃ 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 before before the final instruction.

Definition s20_prop (frame: TFrame) :=
  pcToPosition (frameGetPC frame) = 20%nat
  ∧ ∃ r,
    stack_values frame [r ]
    ∧ r = n ×n.

Proofs of single transitions

We prove properties in the style of Hoare triples for all possible transitions in the program.

The initial state obeys s0_prop

Lemma start_0: s0_prop frame0.
Proof.
  unfold s0_prop.
  unfold frame0.
  split; simpl.
  unfold pc0.
  apply PpositionPc.
  reflexivity.
Qed.

A manual proof for each possible transition. const

Lemma trans_0_1: ∀ frame frame',
  s0_prop frame →
  SF.stepFrame code frame frame' →
  s1_prop frame'.
Proof.
  unfold s0_prop, s1_prop.
  intros frame frame' Hprev Hstep.
  decompose [and] Hprev.
  destruct_frame frame.
  de_step2.
  inversion H6; subst; clear H6.
  split.
  do_next.
  doFiniteStack.
  reflexivity.
Qed.

store var0

Lemma trans_1_2: ∀ frame frame',
  s1_prop frame →
  SF.stepFrame code frame frame' →
  s2_prop frame'.
Proof.
  unfold s1_prop, s2_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step2.
  split.
  do_next.
  doInversionStore.
  doFiniteStack.
  intuition.
  inversion H2; clear H2; subst.
  eapply var_set_this.
  apply const0.
Qed.

const n

Lemma trans_2_3: ∀ frame frame',
  s2_prop frame →
  SF.stepFrame code frame frame' →
  s3_prop frame'.
Proof.
  unfold s2_prop, s3_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step2.
  inversion H7; subst; clear H7.
  split.
  do_next.
  decompose [and] H0; clear H0.
  subst.
  doFiniteStack.
  intuition.
  eapply var_value_other_fields.
  eassumption.
Qed.

store var1

Lemma trans_3_4: ∀ frame frame',
  s3_prop frame →
  SF.stepFrame code frame frame' →
  s4_prop frame'.
Proof.
  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.
  intuition.
  eapply var_set_other.
  auto using distinct_vars_0_1.
  eassumption.
  inversion H4; clear H4; subst.
  eapply var_set_this.
  apply constn.
Qed.

Lemma trans_4_5: ∀ frame frame',
  s4_prop frame →
  SF.stepFrame code frame frame' →
  s5_prop frame'.
Proof.
  unfold s4_prop, s5_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step2.
  split.
  do_next.
  inversion H7; subst; clear H7.
  decompose [and] H0; clear H0.
  doFiniteStack.
  intuition.
  eapply var_value_other_fields.
  eassumption.
  eapply var_value_other_fields.
  eassumption.
Qed.

store var2

Lemma trans_5_post: ∀ frame frame',
  s5_prop frame →
  SF.stepFrame code frame frame' →
  s5_post_prop frame'.
Proof.
  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.
  intuition.
  eapply var_set_other.
  auto using distinct_vars_0_2.
  eassumption.
  eapply var_set_other.
  auto using distinct_vars_1_2.
  eassumption.

  inversion H5; clear H5; subst.
  eapply var_set_this.
  apply const0.
Qed.

An actual state description generalises to loop invariant.

Lemma post5_impl_pre6: ∀ frame,
  s5_post_prop frame → s6_prop frame.
Proof.
  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',
  s6_prop frame →
  SF.stepFrame code frame frame' →
  s7_prop frame'.
Proof.
  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 H0 as [r].
  ∃ i.
  ∃ r.
  decompose [and] H0; clear H0.
  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 var1

Lemma trans_7_8: ∀ frame frame',
  s7_prop frame →
  SF.stepFrame code frame frame' →
  s8_prop frame'.
Proof.
  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 H0 as [r].
  ∃ i.
  ∃ r.
  decompose [and] H0; clear H0.
  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.

cond ge

Lemma trans_8_post8: ∀ frame frame',
  s8_prop frame →
  SF.stepFrame code frame frame' →
  s8_post_prop frame'.
Proof.
  unfold s8_prop, s8_post_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step2.
  destruct H0 as [i].
  destruct H0 as [r].
  ∃ i.
  ∃ r.
  decompose [and] H0; clear H0.
  destruct_stack_values.
  inversion H8; subst; clear H8.   decompose [and] H0; clear H0.

  inversion H7; subst; clear H7;
    simpl in *;
    injection H1; clear H1; 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 H15; subst; clear H15.
  right.
  split.
  apply PmakeOffset.
  apply M_IntNumProperties.is_ge_t_toZ_prop in H5.
  omega.
  inversion H15; subst; clear H15.
  left.
  split.
  do_next.
  apply M_IntNumProperties.is_ge_f_toZ_prop in H5.
  omega.
Qed.

Lemma post8_impl_9_or_19: ∀ frame,
  s8_post_prop frame →
  (s9_prop frame ∨ s19_prop frame).
Proof.
  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',
  s9_prop frame →
  SF.stepFrame code frame frame' →
  s10_prop frame'.
Proof.
  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 H0 as [r].
  ∃ i.
  ∃ r.
  decompose [and] H0; clear H0.
  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_10_11: ∀ frame frame',
  s10_prop frame →
  SF.stepFrame code frame frame' →
  s11_prop frame'.
Proof.
  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 H0 as [r].
  ∃ i.
  ∃ r.
  decompose [and] H0; clear H0.
  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_11_12: ∀ frame frame',
  s11_prop frame →
  SF.stepFrame code frame frame' →
  s12_prop frame'.
Proof.
  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 H0 as [old_r].
  ∃ i.
  ∃ (old_r + i).
  decompose [and] H0; clear H0.
  inversion H7; subst; clear H7.
  destruct_stack_values.
  inversion H8; subst; clear H8.   decompose [and] H0; clear H0.
  simpl in ×.
  injection H1; clear H1; intros.
  repeat subst.
  intuition.
  inversion H12; subst; clear H12.   constructor.
  constructor.
  rewrite Z.add_comm at 1.
  rewrite <- H11.
  apply add_add.
  omega.
  rewrite H11.
  apply sqr_pos.
  rewrite H11.
  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',
  s12_prop frame →
  SF.stepFrame code frame frame' →
  s13_prop frame'.
Proof.
  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 H0 as [r].
  ∃ i.
  ∃ r.
  decompose [and] H0; clear H0.
  subst.
  destruct_stack_values.
  doInversionStore.
  doFiniteStack.
  intuition.
  constructor.

  eapply var_set_other.
  auto using distinct_vars_0_2.
  eassumption.

  eapply var_set_other.
  auto using distinct_vars_1_2.
  eassumption.

  inversion H4; clear H4; subst.
  eapply var_set_this.
  assumption.
Qed.

iinc

Lemma trans_13_14: ∀ frame frame',
  s13_prop frame →
  SF.stepFrame code frame frame' →
  s14_prop frame'.
Proof.
  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 H0 as [r].
  ∃ i.
  ∃ r.
  decompose [and] H0; clear H0.
  subst.

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

  inversion H3; clear H3.   rewrite H11 in H13; clear H11.
  injection H13; clear H13; 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.

  eapply var_set_other.
  apply distinct_vars_0_1.
  eassumption.
  eapply var_set_other.
  apply distinct_vars_0_2.
  eassumption.
Qed.

load var0

Lemma trans_14_15: ∀ frame frame',
  s14_prop frame →
  SF.stepFrame code frame frame' →
  s15_prop frame'.
Proof.
  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 H0 as [r].
  ∃ i.
  ∃ r.
  decompose [and] H0; clear H0.
  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_15_16: ∀ frame frame',
  s15_prop frame →
  SF.stepFrame code frame frame' →
  s16_prop frame'.
Proof.
  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 H0 as [r].
  ∃ i.
  ∃ r.
  decompose [and] H0; clear H0.
  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',
  s16_prop frame →
  SF.stepFrame code frame frame' →
  s17_prop frame'.
Proof.
  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 H0 as [old_r].
  ∃ i.
  ∃ (old_r + (i+1)).
  decompose [and] H0; clear H0.
  inversion H7; subst; clear H7.
  destruct_stack_values.
  inversion H8; subst; clear H8.   decompose [and] H0; clear H0.
  simpl in ×.
  injection H1; clear H1; intros.
  repeat subst.
  intuition.
  inversion H12; subst; clear H12.   constructor.
  constructor.
  rewrite Z.add_comm at 1.
  rewrite <- H11.
  rewrite <- H13.
  apply add_add.
  omega.
  rewrite H11.
  apply Z.le_ge.
  apply OMEGA2.
  apply Z.ge_le.
  apply sqr_pos.
  assumption.
  rewrite H11.
  rewrite H13.
  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',
  s17_prop frame →
  SF.stepFrame code frame frame' →
  s18_prop frame'.
Proof.
  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 H0 as [r].
  ∃ i.
  ∃ r.
  decompose [and] H0; clear H0.
  subst.
  destruct_stack_values.
  doInversionStore.
  doFiniteStack.
  intuition.

  constructor.

  eapply var_set_other.
  auto using distinct_vars_0_2.
  eassumption.

  eapply var_set_other.
  auto using distinct_vars_1_2.
  eassumption.

  inversion H4; clear H4; subst.
  eapply var_set_this.
  eassumption.
Qed.

goto

Lemma trans_18_6: ∀ frame frame',
  s18_prop frame →
  SF.stepFrame code frame frame' →
  s6_prop frame'.
Proof.
  unfold s18_prop, s6_prop.
  intros frame frame' Hprev Hstep.
  destruct Hprev.
  destruct_frame frame.
  de_step2.
  inversion H7; clear H7; subst.   inversion H8; clear H8; subst.   decompose [and] H1; simpl in *; repeat subst.

  split.
  apply PmakeOffset.
  destruct H0 as [i].
  destruct H0 as [r].
  decompose [and] H0; clear H0.
  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 H5 by ring.
  eapply var_value_other_fields.
  eassumption.
Qed.

load

Lemma trans_19_20: ∀ frame frame',
  s19_prop frame →
  SF.stepFrame code frame frame' →
  s20_prop frame'.
Proof.
  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 H0 as [r].
  ∃ r.
  decompose [and] H0; clear H0.
  subst.
  doInversionLoad.
  doFiniteStack.
  intuition.

  eapply stack_value_from_var.
  eassumption.
  eassumption.
  eassumption.
  eassumption.
Qed.

There is no step from instruction 20 I_Return (within the current frame).

Lemma final_20: ∀ frame frame',
  s20_prop frame →
  SF.stepFrame code frame frame' →
  False.
Proof.
  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;
    simpl in H;
    discriminate H.
Qed.

Formulation and proof of the main inductive lemma

State is reachable from the starting state.

Main lemma: transitions within closed set of states

Lemma closed_states: ∀ frame,
  reachable frame → described frame.
Proof.
  intros.
  apply clos_rt_rtn1 in H.   induction H.
  apply described_0.
  apply start_0.
  clear H0.   destruct IHclos_refl_trans_n1.

  eauto using described_1, trans_0_1.
  eauto using described_2, trans_1_2.
  eauto using described_3, trans_2_3.
  eauto using described_4, trans_3_4.
  eauto using described_5, trans_4_5.
  eauto using described_6, trans_5_post, post5_impl_pre6.
  eauto using described_7, trans_6_7.
  eauto using described_8, trans_7_8.
    eapply trans_8_post8 in H0.
    apply post8_impl_9_or_19 in H0.
    destruct H0.     apply described_9; eassumption.
    apply described_19; eassumption.
    eassumption.
  eauto using described_10, trans_9_10.
  eauto using described_11, trans_10_11.
  eauto using described_12, trans_11_12.
  eauto using described_13, trans_12_13.
  eauto using described_14, trans_13_14.
  eauto using described_15, trans_14_15.
  eauto using described_16, trans_15_16.
  eauto using described_17, trans_16_17.
  eauto using described_18, trans_17_18.
  eauto using described_6, trans_18_6.
  eauto using described_20, trans_19_20.
  destruct (final_20 frame z).
    assumption.
    assumption.
Qed.

Lemma s20: ∀ frame,
  described frame →
  pcToPosition (frameGetPC frame) = 20%nat →
  s20_prop frame.
Proof.
  intros.
  destruct H;
    [unfold s0_prop in ×
    |unfold s1_prop in ×
    |unfold s2_prop in ×
    |unfold s3_prop in ×
    |unfold s4_prop in ×
    |unfold s5_prop in ×
    |unfold s6_prop in ×
    |unfold s7_prop in ×
    |unfold s8_prop in ×
    |unfold s9_prop in ×
    |unfold s10_prop in ×
    |unfold s11_prop in ×
    |unfold s12_prop in ×
    |unfold s13_prop in ×
    |unfold s14_prop in ×
    |unfold s15_prop in ×
    |unfold s16_prop in ×
    |unfold s17_prop in ×
    |unfold s18_prop in ×
    |unfold s19_prop in ×
    |idtac];
    try (decompose [and] H;
      rewrite H0 in H1;
      discriminate H1).
    assumption.
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.
  apply closed_states in H0.
  apply s20 in H0.
  unfold s20_prop in H0.
  decompose [and] H0; clear H0.
  destruct H2 as [r].   decompose [and] H0; clear H0.
  inversion H2; clear H2.
  inversion H6; clear H6.
  ∃ num.
  subst.
  intuition assumption.
  assumption.
Qed.
End LoopExample.