Library bbs_termination

Require Import Classical Epsilon.
Require Import ssreflect ssrbool.
Require Import ZArith_ext Lists_ext.
Require Import machine_int.
Import MachineInt.
Require Import mips_cmd mips_tactics mips_contrib.
Require mips_syntax.
Require Import mont_mul_strict_prg bbs_prg.
Require Import mont_mul_strict_termination mont_square_strict_termination.

Local Open Scope machine_int_scope.
Local Open Scope mips_expr_scope.
Local Open Scope mips_cmd_scope.
Local Open Scope nodup_scope.
Import expr_m.

Lemma termination_inner_loop :
  forall s h j32 L_ l j thirtytwo k alpha x y m one ext int_ X_ Y_ M_ quot C_ t s_ b2k B2K_ w' w,
  nodup(L_, l, j, thirtytwo, k, alpha, x, y, m, one, ext, int_, X_, Y_, M_, quot, C_, t, s_, b2k, B2K_, w', w, r0) ->
  u2Z [thirtytwo]_s - u2Z [j]_s = Z_of_nat j32 ->
  { sf | (Some (s, h) --
    while.while (bne j thirtytwo)
    (mont_mul_strict_init k alpha x x y m one ext int_ X_ B2K_ Y_ M_ quot C_ t s_;
      mont_mul_strict_init k alpha y b2k x m one ext int_ Y_ B2K_ X_ M_ quot C_ t s_;
      lw w' zero16 x;
      andi w' w' one16;
      sllv w' w' j;
      cmd_or w w w';
      addiu j j one16) ---> sf) }.

Lemma termination_outer_loop :
  forall s h ni i L_ l n j thirtytwo k alpha x y m one ext int_ X_ Y_ M_ quot C_ t s_ b2k B2K_ w' w,
  nodup(i, L_, l, n, j, thirtytwo, k, alpha, x, y, m, one, ext, int_, X_, Y_, M_, quot, C_, t, s_, b2k, B2K_, w', w, r0) ->
  u2Z [n]_s - u2Z [i]_s = Z_of_nat (S ni) ->
  { sf | (Some (s, h) --
    addiu j r0 zero16;
    addiu w r0 zero16;
    while.while (bne j thirtytwo)
    (mont_mul_strict_init k alpha x x y m one ext int_ X_ B2K_ Y_ M_ quot C_ t s_;
      mont_mul_strict_init k alpha y b2k x m one ext int_ Y_ B2K_ X_ M_ quot C_ t s_;
      lw w' zero16 x;
      andi w' w' one16;
      sllv w' w' j;
      cmd_or w w w';
      addiu j j one16);
    sw w zero16 L_;
    addiu L_ L_ four16;
    addiu i i one16 ---> sf) /\
  (forall st, sf = Some st -> u2Z [n]_(fst st) - u2Z [i]_(fst st) = Z_of_nat ni) }.

Lemma bbs_termination :
  forall s_init h_init i L_ l n j thirtytwo k alpha x y m one ext int_ X_ Y_ M_ quot C_ t s_ b2k B2K_ w' w,
  nodup(i, L_, l, n, j, thirtytwo, k, alpha, x, y, m, one, ext, int_, X_, Y_, M_, quot, C_, t, s_, b2k, B2K_, w', w, r0) ->
  { final_state | Some (s_init, h_init) --
    bbs i L_ l n j thirtytwo k alpha x y m one ext int_ X_ Y_ M_ quot C_ t s_ b2k B2K_ w' w --->
    final_state }.