NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library bbs_triple

Require Import ssreflect ssrbool eqtype.
Require Import Arith_ext ZArith_ext Lists_ext.
Require Import machine_int multi_int.
Import MachineInt.
Require Import mips_seplog mips_frame mips_contrib mips_tactics mapstos.
Require Import mont_mul_strict_prg bbs_prg.
Require Import mont_mul_strict_init_triple mont_square_strict_init_triple.

Local Open Scope machine_int_scope.
Local Open Scope eqmod_scope.
Local Open Scope zarith_ext_scope.
Local Open Scope heap_scope.
Import expr_m.
Local Open Scope mips_expr_scope.
Import assert_m.
Local Open Scope mips_assert_scope.
Local Open Scope mips_cmd_scope.
Local Open Scope mips_hoare_scope.

Lemma Zodd_bool_multi : forall n (X : list (int 32)), length X = n ->
  Zodd_bool (Sum n X) = Zodd_bool (u2Z (nth O X zero32)).

Require Import listbit.

Lemma firstn_bits : forall n (a : int n) m, (m < n)%nat ->
  firstn m (bits ((a [.&] Z2u n 1) [.<<] m)) = ListBit.zeros m.

Lemma nth_bits : forall n (a : int n) k, (k < n)%nat ->
  nth k (bits ((a [.&] Z2u n 1) [.<<] k)) true = Zodd_bool (u2Z a).

Lemma skipn_bits : forall n (a : int n) k, (k < n)%nat ->
  skipn (S k) (bits ((a [.&] Z2u n 1) [.<<] k)) = ListBit.zeros (n - S k).

Local Open Scope nodup_scope.

Lemma bbs_triple :
  forall 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 : reg,
    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) ->
  forall nk valpha M, u2Z (nth 0 M zero32) * u2Z valpha =m -1 {{ Zbeta 1 }} ->
  forall nn L, length L = nn ->
  forall X0 Y B2K, length X0 = nk -> length B2K = nk -> length M = nk -> length Y = nk ->
  forall vx vy vm vb2k vl,
  u2Z vy + 4 * Z_of_nat (S nk) < Zbeta 1 -> u2Z vx + 4 * Z_of_nat (S nk) < Zbeta 1 ->
  u2Z vl + 4 * Z_of_nat nn < Zbeta 1 -> Sum nk X0 < Sum nk M -> Sum nk B2K < Sum nk M ->
  Sum nk B2K =m Zbeta nk ^^ 2 {{ Sum nk M }} -> Zodd (Sum nk M) ->
{{ fun s h => u2Z [k]_s = Z_of_nat nk /\ u2Z [n]_s = Z_of_nat nn /\ [x]_s = vx /\
  [y]_s = vy /\ [m]_s = vm /\ [b2k]_s = vb2k /\ [alpha]_s = valpha /\
  [l]_s = vl /\ u2Z [thirtytwo]_s = Z_of_nat 32 /\
  (var_e x |--> X0 ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil ** var_e l |--> L ** var_e y |--> Y ++ zero32 :: nil ** var_e b2k |--> B2K) s h }}
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
{{ fun s h => exists L, exists X, exists Y, length L = nn /\ length X = nk /\ length Y = nk /\
  u2Z [k]_s = Z_of_nat nk /\ u2Z [n]_s = Z_of_nat nn /\ [x]_s = vx /\
  [y]_s = vy /\ [m]_s = vm /\ [b2k]_s = vb2k /\ [alpha]_s = valpha /\
  [l]_s = vl /\ u2Z [thirtytwo]_s = Z_of_nat 32 /\
  (var_e x |--> X ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil ** var_e l |--> L ** var_e y |--> Y ++ zero32 :: nil ** var_e b2k |--> B2K) s h /\
  list_flat (map (@bits 32) L) = bbs_fun_rec (nn * 32) (Sum nk X0 ^^ 2 mod (Sum nk M)) (Sum nk M) }}.
Proof.
move=> 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
  Hset nk valpha M Halpha nn L HlenL X0 Y B2K HlenX0 HlenB2K HlenM HlenY vx
  vy vm vb2k vl Hny Hnx Hnl HSumX0
  HSumB2K HSumB2K1 HoddM.
rewrite /bbs.

addiu i r0 zero16 ;

NextAddiu.
move=> s h [Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [Hr32 Hmem]]]]]]]]].
rewrite /wp_addiu; repeat reg_upd; repeat (split; trivial).
by Assert_upd.

addiu L l zero16 ;

NextAddiu.
move=> s h [[Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [Hr32 Hmem]]]]]]]]] Hri].
rewrite /wp_addiu; repeat reg_upd; repeat (split; trivial).
by Assert_upd.

while (bne i n) (

apply hoare_prop_m.hoare_while_invariant with (fun s h => exists ni, exists L, exists X, exists Y,
 u2Z [i]_s = Z_of_nat ni /\ length L = nn /\ length X = nk /\ length Y = nk /\
 u2Z [k]_s = Z_of_nat nk /\ u2Z [n]_s = Z_of_nat nn /\ [x]_s = vx /\
 [y]_s = vy /\ [m]_s = vm /\ [b2k]_s = vb2k /\ [alpha]_s = valpha /\
 [l]_s = vl /\ u2Z [L_]_s = u2Z vl + 4 * Z_of_nat ni /\
 u2Z [thirtytwo]_s = Z_of_nat 32 /\ (ni <= nn)%nat /\
 (var_e x |--> X ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil ** var_e l |--> L ** var_e y |--> Y ++ zero32 :: nil ** var_e b2k |--> B2K) s h /\
 list_flat (map (@bits 32) (firstn ni L)) = bbs_fun_rec (ni * 32) (Sum nk X0 ^^ 2 mod Sum nk M) (Sum nk M) /\
 Sum nk X =m Sum nk X0 ^^ power 2 (ni * 32) {{ Sum nk M }} /\ Sum nk X < Sum nk M).

move=> s h [[[Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [Hr32 Hmem]]]]]]]]] Hri] HrL_].
exists O, L, X0, Y; repeat (split; trivial).
by rewrite Hri store.get_r0 sext_Z2u // add_0 u2Z_Z2u.
rewrite HrL_ sext_Z2u // add_0 Hrl; ring.
by apply le_O_n.
rewrite mult_0_l /= Zmult_1_r; by apply eqmod_refl.

move=> {L HlenL Y HlenY} s h [[ni [L [X [Y [Hri [HlenL [HlenX [HlenY [Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [HrL_ [Hr32 [Hninn [Hmem [Hbbs [Sum_X X_M]]]]]]]]]]]]]]]]]]]]]] Heqni].
rewrite /= in Heqni; move/negPn : Heqni; move/Zeq_boolP; move/u2Z_inj => Heqni.
exists L, X, Y; repeat (split; trivial).
have : ni = nn by rewrite Heqni Hrn in Hri; apply Z_of_nat_inj in Hri.
move=> ?; subst ni.
rewrite firstn_all // in Hbbs; by rewrite HlenL.

addiu j r0 zero16 ;

clear L HlenL Y HlenY.

NextAddiu.

move=> s h [[ni [L [X [Y [Hri [HlenL [HlenX [HlenY [Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [HrL_ [Hr32 [Hninn [Hmem [Hbbs [Sum_X X_M]]]]]]]]]]]]]]]]]]]]]] Hneqin].
rewrite /= in Hneqin.
rewrite /wp_addiu.
repeat reg_upd; repeat (split; trivial).
exists ni, L, X, Y; repeat (split; trivial).
by Assert_upd.
by rewrite /=; repeat reg_upd; trivial.

addiu w r0 zero16 ;

NextAddiu.

move=> s h [[[ni [L [X [Y [Hri [HlenL [HlenX [HlenY [Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [HrL_ [Hr32 [Hninn [Hmem [Hbbs [Sum_X X_M]]]]]]]]]]]]]]]]]]]]]] Hneqin] Hrw].
rewrite /= in Hneqin.
rewrite /wp_addiu.
repeat reg_upd; repeat (split; trivial).
exists ni, L, X, Y; repeat (split; trivial).
by Assert_upd.
by rewrite /=; repeat reg_upd.

while (bne j thirtytwo) (

apply hoare_prop_m.hoare_stren with (fun s h => exists ni, exists L, length L = nn /\
 exists X, exists Y, u2Z [i]_s = Z_of_nat ni /\ length X = nk /\ length Y = nk /\
  u2Z [k]_s = Z_of_nat nk /\ u2Z [n]_s = Z_of_nat nn /\ [x]_s = vx /\
  [y]_s = vy /\ [m]_s = vm /\ [b2k]_s = vb2k /\ [alpha]_s = valpha /\
  [l]_s = vl /\ u2Z [L_]_s = u2Z vl + 4 * Z_of_nat ni /\
  u2Z [thirtytwo]_s = Z_of_nat 32 /\ (ni < nn)%nat /\ u2Z [j]_s = 0 /\
  [w]_s = zero32 /\
  (var_e x |--> X ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil ** var_e l |--> L ** var_e y |--> Y ++ zero32 :: nil ** var_e b2k |--> B2K) s h /\
  list_flat (map (@bits 32) (firstn ni L)) = bbs_fun_rec (ni * 32) (Sum nk X0 ^^ 2 mod (Sum nk M)) (Sum nk M) /\
  Sum nk X =m Sum nk X0 ^^ power 2 (ni * 32) {{ Sum nk M }} /\ Sum nk X < Sum nk M).

move=> s h [[[[ni [L [X [Y [Hregi [HlenL [HlenX [HlenY [Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [HrL_ [Hr32 [Hninn [Hmem [Hbbs [Sum_X Sum_M]]]]]]]]]]]]]]]]]]]]]] Hneqni] Hrj] Hrw].
rewrite /= in Hneqni; move/Zeq_boolP : Hneqni => Hneqni.

exists ni, L; repeat (split; trivial).
exists X, Y; repeat (split; trivial).
rewrite Hregi Hrn in Hneqni.
apply Z_of_nat_inj_neq in Hneqni.
by apply le_neq_lt.
by rewrite Hrj store.get_r0 // add_com add_0 (@u2Z_sext 16) u2Z_Z2u.
move: Hrw; rewrite sext_Z2u // add_0 store.get_r0; by move/u2Z_inj.

apply pull_out_exists => ni; apply pull_out_exists => L.

apply hoare_prop_m.hoare_stren with ((fun s h => length L = nn /\ h = heap.emp) **
 (fun s h => exists X, exists Y, u2Z [i]_s = Z_of_nat ni /\ length X = nk /\ length Y = nk /\
  u2Z [k]_s = Z_of_nat nk /\ u2Z [n]_s = Z_of_nat nn /\
  [x]_s = vx /\ [y]_s = vy /\ [m]_s = vm /\ [b2k]_s = vb2k /\
  [alpha]_s = valpha /\ [l]_s = vl /\ u2Z [L_]_s = u2Z vl + 4 * Z_of_nat ni /\
  u2Z [thirtytwo]_s = Z_of_nat 32 /\ (ni < nn)%nat /\ u2Z [j]_s = 0 /\ [w]_s = zero32 /\
  (var_e x |--> X ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil ** var_e l |--> L ** var_e y |--> Y ++ zero32 :: nil ** var_e b2k |--> B2K) s h /\
  list_flat (map (@bits 32) (firstn ni L)) = bbs_fun_rec (ni * 32) (Sum nk X0 ^^ 2 mod (Sum nk M)) (Sum nk M) /\
  Sum nk X =m Sum nk X0 ^^ power 2 (ni * 32) {{ Sum nk M }} /\ Sum nk X < Sum nk M)).

move=> s h [HlenL [X [Y [Hri [HlenX [HlenY [Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [HrL_ [Hr32 [Hninn [Hregj [Hrw [Hmem [Hbs [Sum_X X_M]]]]]]]]]]]]]]]]]]]]]].

exists heap.emp, h; repeat (split; trivial).
by map_tac_m.Disj.
by map_tac_m.Equal.
by exists X, Y.

apply pull_out_and => HlenL.

apply while.hoare_seq with (fun s h => exists X, exists Y, exists vw,
  u2Z [i]_s = Z_of_nat ni /\ length X = nk /\ length Y = nk /\
  u2Z [k]_s = Z_of_nat nk /\ u2Z [n]_s = Z_of_nat nn /\ [x]_s = vx /\
  [y]_s = vy /\ [m]_s = vm /\ [b2k]_s = vb2k /\
  [alpha]_s = valpha /\ [l]_s = vl /\ u2Z [L_]_s = u2Z vl + 4 * Z_of_nat ni /\
  u2Z [thirtytwo]_s = Z_of_nat 32 /\ u2Z [j]_s = Z_of_nat 32 /\
  (var_e x |--> X ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil ** var_e l |--> L ** var_e y |--> Y ++ zero32 :: nil ** var_e b2k |--> B2K) s h /\
  list_flat (map (@bits 32) (firstn ni L)) = bbs_fun_rec (ni * 32) (Sum nk X0 ^^ 2 mod (Sum nk M)) (Sum nk M) /\
  (ni < nn)%nat /\ [w]_s = vw /\
  bits vw = bbs_fun_rec 32 ((Sum nk X0 ^^ 2 mod (Sum nk M)) ^^ power 2 (ni * 32) mod (Sum nk M)) (Sum nk M) /\
  Sum nk X =m Sum nk X0 ^^ power 2 ((S ni) * 32) {{ Sum nk M }} /\ Sum nk X < Sum nk M).

apply hoare_prop_m.hoare_while_invariant with (fun s h => exists X, exists Y, exists vw, exists nj,
  u2Z [i]_s = Z_of_nat ni /\ length X = nk /\ length Y = nk /\
  u2Z [k]_s = Z_of_nat nk /\ u2Z [n]_s = Z_of_nat nn /\ [x]_s = vx /\ [y]_s = vy /\
  [m]_s = vm /\ [b2k]_s = vb2k /\ [alpha]_s = valpha /\ [l]_s = vl /\
  u2Z [L_]_s = u2Z vl + 4 * Z_of_nat ni /\ u2Z [thirtytwo]_s = Z_of_nat 32 /\
  u2Z [j]_s = Z_of_nat nj /\
  (var_e x |--> X ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil ** var_e l |--> L ** var_e y |--> Y ++ zero32 :: nil ** var_e b2k |--> B2K) s h /\
  list_flat (map (@bits 32) (firstn ni L)) = bbs_fun_rec (ni * 32) (Sum nk X0 ^^ 2 mod (Sum nk M)) (Sum nk M) /\
  (ni < nn)%nat /\ (nj <= 32)%nat /\ [w]_s = vw /\
  firstn nj (bits vw) = bbs_fun_rec nj ((Sum nk X0 ^^ 2 mod (Sum nk M)) ^^ power 2 (ni * 32) mod (Sum nk M)) (Sum nk M) /\
  skipn nj (bits vw) = ListBit.zeros (32 - nj) /\
  Sum nk X =m Sum nk X0 ^^ power 2 (ni * 32 + nj) {{ Sum nk M }} /\ Sum nk X < Sum nk M).

move=> s h [X [Y [Hri [HlenX [HlenY [Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [HrL_ [Hr32 [Hninn [Hrj [Hrw [Hmem [Hbbs [Sum_X X_M]]]]]]]]]]]]]]]]]]]]].

exists X, Y, zero32; exists O; repeat (split; trivial).
by apply le_O_n.
rewrite -minus_n_O [ListBit.zeros]lock /= -lock /zero32; by apply bits_zeros.
by rewrite plus_0_r.

move=> s h [[X [Y [vw [nj [Hri [HlenX [HlenY [Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [HrL_ [Hr32 [Hrj [Hmem [Hbbs [Hninn [Hnj32 [Hrw [Hbbs' [Hbbs'' [Sum_X X_M]]]]]]]]]]]]]]]]]]]]]]]]]] Heqj32].
rewrite /= Hr32 Hrj in Heqj32; move/negPn : Heqj32; move/Zeq_boolP; move/Z_of_nat_inj => Heqj32.
exists X, Y, vw.
subst nj.
rewrite mult_succ_l.
repeat (split; trivial).
rewrite firstn_all // in Hbbs'; by rewrite length_bits.


apply hoare_prop_m.hoare_stren with (fun s h => exists vw, exists nj, exists X, exists Y,
  u2Z [i]_s = Z_of_nat ni /\ length X = nk /\ length Y = nk /\
  u2Z [k]_s = Z_of_nat nk /\ u2Z [n]_s = Z_of_nat nn /\ [x]_s = vx /\ [y]_s = vy /\
  [m]_s = vm /\ [b2k]_s = vb2k /\ [alpha]_s = valpha /\ [l]_s = vl /\
  u2Z [L_]_s = u2Z vl + 4 * Z_of_nat ni /\
  u2Z [thirtytwo]_s = Z_of_nat 32 /\ u2Z [j]_s = Z_of_nat nj /\
  (var_e x |--> X ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil ** var_e l |--> L ** var_e y |--> Y ++ zero32 :: nil ** var_e b2k |--> B2K) s h /\
  list_flat (map (@bits 32) (firstn ni L)) = bbs_fun_rec (ni * 32) (Sum nk X0 ^^ 2 mod Sum nk M) (Sum nk M) /\
  (ni < nn)%nat /\ (nj < 32)%nat /\ [w]_s = vw /\
  firstn nj (bits vw) = bbs_fun_rec nj ((Sum nk X0 ^^ 2 mod Sum nk M) ^^ power 2 (ni * 32) mod Sum nk M) (Sum nk M) /\
  skipn nj (bits vw) = ListBit.zeros (32 - nj) /\
  Sum nk X =m Sum nk X0 ^^ power 2 (ni * 32 + nj) {{ Sum nk M }} /\ Sum nk X < Sum nk M).

move=> s h [ [X [Y [vw [nj [Hri [HlenX [HlenY [Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [HrL_ [Hr32 [Hrj [Hmem [Hbbs [Hninn [Hnj32 [Hrw [Hbbs' [Hbbs'' [Sum_X X_M]]]]]]]]]]]]]]]]]]]]]]]]]] Hnej32].
rewrite /= Hrj Hr32 in Hnej32. move/Zeq_boolP : Hnej32;move/Z_of_nat_inj_neq => Hnej32.
exists vw, nj, X, Y; repeat (split; trivial).
by apply le_neq_lt.

apply pull_out_exists => vw; apply pull_out_exists => nj; apply pull_out_exists => X.

apply hoare_prop_m.hoare_stren with ((fun s h => length X = nk /\ h = heap.emp) **
 (fun s h => exists Y, u2Z [i]_s = Z_of_nat ni /\ length X = nk /\ length Y = nk /\
  u2Z [k]_s = Z_of_nat nk /\ u2Z [n]_s = Z_of_nat nn /\ [x]_s = vx /\
  [y]_s = vy /\ [m]_s = vm /\ [b2k]_s = vb2k /\ [alpha]_s = valpha /\
  [l]_s = vl /\ u2Z [L_]_s = u2Z vl + 4 * Z_of_nat ni /\
  u2Z [thirtytwo]_s = Z_of_nat 32 /\ u2Z [j]_s = Z_of_nat nj /\
  (var_e x |--> X ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil ** var_e l |--> L ** var_e y |--> Y ++ zero32 :: nil ** var_e b2k |--> B2K) s h /\
  list_flat (map (@bits 32) (firstn ni L)) = bbs_fun_rec (ni * 32) (Sum nk X0 ^^ 2 mod Sum nk M) (Sum nk M) /\
  (ni < nn)%nat /\ (nj < 32)%nat /\ [w]_s = vw /\
  firstn nj (bits vw) = bbs_fun_rec nj ((Sum nk X0 ^^ 2 mod Sum nk M) ^^ power 2 (ni * 32) mod Sum nk M) (Sum nk M) /\
  skipn nj (bits vw) = ListBit.zeros (32 - nj) /\
  Sum nk X =m Sum nk X0 ^^ power 2 (ni * 32 + nj) {{ Sum nk M }} /\ Sum nk X < Sum nk M)).

move=> s h [Y [Hri [HlenX [HlenY [Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [HrL_ [Hr32 [Hrj [Hmem [Hbbs [Hninn [Hnj32 [Hrw [Hbbs' [Hbbs'' [Sum_X X_M]]]]]]]]]]]]]]]]]]]]]]].

exists heap.emp, h; repeat (split; trivial).
by map_tac_m.Disj.
by map_tac_m.Equal.
by exists Y.

apply pull_out_and => HlenX.

apply while.hoare_seq with (fun s h => exists Y, u2Z [i]_s = Z_of_nat ni /\
 length X = nk /\ length Y = nk /\ u2Z [k]_s = Z_of_nat nk /\
 u2Z [n]_s = Z_of_nat nn /\ [x]_s = vx /\ [y]_s = vy /\
 [m]_s = vm /\ [b2k]_s = vb2k /\ [alpha]_s = valpha /\
 [l]_s = vl /\ u2Z [L_]_s = u2Z vl + 4 * Z_of_nat ni /\
 u2Z [thirtytwo]_s = Z_of_nat 32 /\ u2Z [j]_s = Z_of_nat nj /\
 (var_e x |--> X ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil ** var_e l |--> L ** var_e y |--> Y ++ zero32 :: nil ** var_e b2k |--> B2K) s h /\
 list_flat (map (@bits 32) (firstn ni L)) = bbs_fun_rec (ni * 32) (Sum nk X0 ^^ 2 mod Sum nk M) (Sum nk M) /\
 (ni < nn)%nat /\ (nj < 32)%nat /\ [w]_s = vw /\
 firstn nj (bits vw) = bbs_fun_rec nj ((Sum nk X0 ^^ 2 mod Sum nk M) ^^ power 2 (ni * 32) mod Sum nk M) (Sum nk M) /\
 skipn nj (bits vw) = ListBit.zeros (32 - nj) /\
 Zbeta nk * Sum nk Y =m Sum nk X0 ^^ power 2 (ni * 32 + S nj) {{ Sum nk M }} /\ Sum nk Y < Sum nk M).

apply hoare_prop_m.hoare_stren with ((fun s h => Sum nk X < Sum nk M /\ h = heap.emp) **
((fun s h => exists Y, length Y = nk /\ [x]_s = vx /\ [y]_s = vy /\
  [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e y |--> Y ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil) s h) **
(fun s h => u2Z [i]_s = Z_of_nat ni /\ u2Z [n]_s = Z_of_nat nn /\
  [b2k]_s = vb2k /\ [l]_s = vl /\ u2Z [L_]_s = u2Z vl + 4 * Z_of_nat ni /\
  u2Z [thirtytwo]_s = Z_of_nat 32 /\ u2Z [j]_s = Z_of_nat nj /\
  (add_e (var_e x) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32 ** var_e l |--> L ** var_e b2k |--> B2K) s h /\
  list_flat (map (@bits 32) (firstn ni L)) = bbs_fun_rec (ni * 32) (Sum nk X0 ^^ 2 mod Sum nk M) (Sum nk M) /\
  (ni < nn)%nat /\ (nj < 32)%nat /\ [w]_s = vw /\
  firstn nj (bits vw) = bbs_fun_rec nj ((Sum nk X0 ^^ 2 mod Sum nk M) ^^ power 2 (ni * 32) mod Sum nk M) (Sum nk M) /\
  skipn nj (bits vw)= ListBit.zeros (32 - nj) /\
  Sum nk X =m Sum nk X0 ^^ power 2 (ni * 32 + nj) {{ Sum nk M }}))).

move=> {HlenX} s h [Y [Hregi [HlenX [HlenY [Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [HrL_ [Hr32 [Hrj [Hmem [Hbbs [Hninn [Hnj32 [Hrw [Hbbs' [Hbbs'' [Sum_X X_M]]]]]]]]]]]]]]]]]]]]]]].

exists heap.emp, h; repeat split.
by map_tac_m.Disj.
by map_tac_m.Equal.
exact X_M.

have {Hmem}Hmem : ((var_e x |--> X ** var_e y |--> Y ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil) **
    (add_e (var_e x) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32 ** var_e l |--> L ** var_e b2k |--> B2K)) s h.
  rewrite (decompose_last_equiv _ X) HlenX in Hmem.
  by assoc_comm Hmem.
case: Hmem => h1 [h2 [Hdisj [Hunion [Hmem1 Hmem2]]]].
exists h1, h2; repeat (split; trivial).
by exists Y.

apply pull_out_and => X_M.

apply hoare_prop_m.hoare_weak with ((fun s h => exists Y, length Y = nk /\ [x]_s = vx /\ [y]_s = vy /\
  [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e x |--> X ** var_e y |--> Y ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil) s h /\
  Zbeta nk * Sum nk Y =m Sum nk X * Sum nk X {{ Sum nk M }} /\ Sum nk Y < Sum nk M) **
 (fun s h => u2Z [i]_s = Z_of_nat ni /\ u2Z [n]_s = Z_of_nat nn /\
  [b2k]_s = vb2k /\ [l]_s = vl /\ u2Z [L_]_s = u2Z vl + 4 * Z_of_nat ni /\
  u2Z [thirtytwo]_s = Z_of_nat 32 /\ u2Z [j]_s = Z_of_nat nj /\
  (add_e (var_e x) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32 ** var_e l |--> L ** var_e b2k |--> B2K) s h /\
  list_flat (map (bits (n:=32)) (firstn ni L)) = bbs_fun_rec (ni * 32) (Sum nk X0 ^^ 2 mod Sum nk M) (Sum nk M) /\
  (ni < nn)%nat /\ (nj < 32)%nat /\ [w]_s = vw /\
  firstn nj (bits vw) = bbs_fun_rec nj ((Sum nk X0 ^^ 2 mod Sum nk M) ^^ power 2 (ni * 32) mod Sum nk M) (Sum nk M) /\
  skipn nj (bits vw) = ListBit.zeros (32 - nj) /\
  Sum nk X =m Sum nk X0 ^^ power 2 (ni * 32 + nj) {{ Sum nk M }})).

move=> s h [h1 [h2 [Hdisj [Hunion [
[Y [len_Y [r_x [r_y [r_m [r_k [r_alpha [Hmem1 [Sum_Y Y_M]]]]]]]]]
[r_i [r_n [r_one' [r_l [r_L_ [r_32 [r_j [Hmem2 [Hbbs' [Hninn [Hnj32 [r_w [Hbbs [Hbbs'' Sum_X]]]]]]]]]]]]]]
]]]]].
exists Y; repeat (split; trivial).
rewrite (decompose_last_equiv _ X) HlenX.
move: {Hmem1 Hmem2}(assert_m.con_cons _ _ _ _ _ Hdisj Hmem1 Hmem2).
rewrite -Hunion => Hmem.
by assoc_comm Hmem.
eapply eqmod_trans.
by apply Sum_Y.
eapply eqmod_rewrite.
apply eqmod_sym; by apply Sum_X.
rewrite Zmult_comm.
eapply eqmod_rewrite.
apply eqmod_sym; by apply Sum_X.
rewrite -Zpower_b_is_exp power_plus plus_n_Sm; by apply eqmod_refl.

apply frame_rule.
- eapply mont_square_strict_init_triple => //.
  by abstract Nodup_nodup r0.
- by Inde_frame.
- move=> ?; by Inde_mult.

mont_mul_strict_init k alpha y b2k x m one ext int Y B2K X M quot C t s;

apply pull_out_exists => Y.

apply hoare_prop_m.hoare_stren with ((fun s h => length Y = nk /\ h = heap.emp) **
 (fun s h => u2Z [i]_s = Z_of_nat ni /\ length X = nk /\
  u2Z [k]_s = Z_of_nat nk /\ u2Z [n]_s = Z_of_nat nn /\
  [x]_s = vx /\ [y]_s = vy /\ [m]_s = vm /\ [b2k]_s = vb2k /\
  [alpha]_s = valpha /\ [l]_s = vl /\ u2Z [L_]_s = u2Z vl + 4 * Z_of_nat ni /\
  u2Z [thirtytwo]_s = Z_of_nat 32 /\ u2Z [j]_s = Z_of_nat nj /\
  (var_e x |--> X ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil ** var_e l |--> L ** var_e y |--> Y ++ zero32 :: nil ** var_e b2k |--> B2K) s h /\
  list_flat (map (@bits 32) (firstn ni L)) = bbs_fun_rec (ni * 32) (Sum nk X0 ^^ 2 mod Sum nk M) (Sum nk M) /\
  (ni < nn)%nat /\ (nj < 32)%nat /\ [w]_s = vw /\
  firstn nj (bits vw) = bbs_fun_rec nj ((Sum nk X0 ^^ 2 mod Sum nk M) ^^ power 2 (ni * 32) mod Sum nk M) (Sum nk M) /\
  skipn nj (bits vw) = ListBit.zeros (32 - nj) /\
  Zbeta nk * Sum nk Y =m Sum nk X0 ^^ power 2 (ni * 32 + S nj) {{ Sum nk M }} /\ Sum nk Y < Sum nk M)).

move=> {HlenX} s h [Hri [HlenX [HlenY [Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [HrL_ [Hr32 [Hrj [Hmem [Hbbs' [Hninn [Hnj32 [Hrw [Hbbs [Hbbs'' [Sum_Y HSum_Y']]]]]]]]]]]]]]]]]]]]]].

exists heap.emp, h; repeat (split => //).
by map_tac_m.Disj.
by map_tac_m.Equal.

apply pull_out_and => HlenY.

apply hoare_prop_m.hoare_stren with (fun s h => exists X,
 u2Z [i]_s = Z_of_nat ni /\ length X = nk /\ u2Z [k]_s = Z_of_nat nk /\
 u2Z [n]_s = Z_of_nat nn /\ [x]_s = vx /\ [y]_s = vy /\
 [m]_s = vm /\ [b2k]_s = vb2k /\ [alpha]_s = valpha /\ [l]_s = vl /\
 u2Z [L_]_s = u2Z vl + 4 * Z_of_nat ni /\ u2Z [thirtytwo]_s = Z_of_nat 32 /\
 u2Z [j]_s = Z_of_nat nj /\
 (var_e x |--> X ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil ** var_e l |--> L ** var_e y |--> Y ++ zero32 :: nil ** var_e b2k |--> B2K) s h /\
 list_flat (map (@bits 32) (firstn ni L)) =
 bbs_fun_rec (ni * 32) (Sum nk X0 ^^ 2 mod Sum nk M) (Sum nk M) /\
 (ni < nn)%nat /\ (nj < 32)%nat /\ [w]_s = vw /\
 firstn nj (bits vw) = bbs_fun_rec nj ((Sum nk X0 ^^ 2 mod Sum nk M) ^^ power 2 (ni * 32) mod Sum nk M) (Sum nk M) /\
 skipn nj (bits vw) = ListBit.zeros (32 - nj) /\
 Zbeta nk * Sum nk Y =m Sum nk X0 ^^ power 2 (ni * 32 + S nj) {{ Sum nk M }} /\ Sum nk Y < Sum nk M).

move=> {HlenX} s h [Hri [HlenX [Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [HrL_ [Hr32 [Hrj [Hmem [Hbbs' [Hninn [Hnj32 [Hrw [Hbbs [Hbbs'' [Sum_Y Sum_Y']]]]]]]]]]]]]]]]]]]]].
by exists X.

apply while.hoare_seq with (fun s h => exists X, u2Z [i]_s = Z_of_nat ni /\
 length X = nk /\ u2Z [k]_s = Z_of_nat nk /\
 u2Z [n]_s = Z_of_nat nn /\ [x]_s = vx /\ [y]_s = vy /\
 [m]_s = vm /\ [b2k]_s = vb2k /\ [alpha]_s = valpha /\
 [l]_s = vl /\ u2Z [L_]_s = u2Z vl + 4 * Z_of_nat ni /\
 u2Z [thirtytwo]_s = Z_of_nat 32 /\ u2Z [j]_s = Z_of_nat nj /\
 (var_e x |--> X ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil ** var_e l |--> L ** var_e y |--> Y ++ zero32 :: nil ** var_e b2k |--> B2K) s h /\
 list_flat (map (@bits 32) (firstn ni L)) = bbs_fun_rec (ni * 32) (Sum nk X0 ^^ 2 mod Sum nk M) (Sum nk M) /\
 (ni < nn)%nat /\ (nj < 32)%nat /\ [w]_s = vw /\
 firstn nj (bits vw) = bbs_fun_rec nj ((Sum nk X0 ^^ 2 mod Sum nk M) ^^ power 2 (ni * 32) mod Sum nk M) (Sum nk M) /\
 skipn nj (bits vw) = ListBit.zeros (32 - nj) /\
 Sum nk X =m Sum nk X0 ^^ power 2 (ni * 32 + S nj) {{ Sum nk M }} /\ Sum nk X < Sum nk M).

apply hoare_prop_m.hoare_stren with ((fun s h => Sum nk Y < Sum nk M /\ h = heap.emp) **
((fun s h => exists X, length X = nk /\
  [y]_s = vy /\ [b2k]_s = vb2k /\ [x]_s = vx /\ [m]_s = vm /\
  u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e y |--> Y ** var_e b2k |--> B2K ** var_e x |--> X ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil) s h) **
 (fun s h => u2Z [i]_s = Z_of_nat ni /\ u2Z [n]_s = Z_of_nat nn /\
   [l]_s = vl /\ u2Z [L_]_s = u2Z vl + 4 * Z_of_nat ni /\
  u2Z [thirtytwo]_s = Z_of_nat 32 /\ u2Z [j]_s = Z_of_nat nj /\
  (var_e l |--> L ** add_e (var_e y) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32) s h /\
  list_flat (map (@bits 32) (firstn ni L)) = bbs_fun_rec (ni * 32) (Sum nk X0 ^^ 2 mod Sum nk M) (Sum nk M) /\
  (ni < nn)%nat /\ (nj < 32)%nat /\ [w]_s = vw /\
  firstn nj (bits vw) = bbs_fun_rec nj ((Sum nk X0 ^^ 2 mod Sum nk M) ^^ power 2 (ni * 32) mod Sum nk M) (Sum nk M) /\
  skipn nj (bits vw) = ListBit.zeros (32 - nj) /\
  Zbeta nk * Sum nk Y =m Sum nk X0 ^^ power 2 (ni * 32 + S nj) {{ Sum nk M}} ))).

move=> {X HlenX} s h [X [Hri [HlenX [Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [HrL_ [Hr32 [Hrj [Hmem [Hbbs' [Hninn [Hnj32 [Hrw [Hbbs [Hbbs'' [Sum_Y Y_M]]]]]]]]]]]]]]]]]]]]]].

exists heap.emp, h; repeat (split; trivial).
by map_tac_m.Disj.
by map_tac_m.Equal.

have {Hmem}Hmem : ((var_e y |--> Y ** var_e x |--> X ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil ** var_e b2k |--> B2K) **
    (add_e (var_e y) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32 ** var_e l |--> L)) s h.
  rewrite (decompose_last_equiv _ Y) HlenY in Hmem.
  by assoc_comm Hmem.
case: Hmem => h1 [h2 [Hdisj [Hunion [Hmem1 Hmem2]]]].
exists h1, h2; repeat (split; trivial).
exists X; repeat (split; trivial).
assoc_comm Hmem1.
by assoc_comm Hmem2.

apply pull_out_and => Y_M.

apply hoare_prop_m.hoare_weak with ((fun s h => exists X, length X = nk /\ [y]_s = vy /\ [b2k]_s = vb2k /\
  [x]_s = vx /\ [m]_s = vm /\ u2Z [k]_s = Z_of_nat nk /\ [alpha]_s = valpha /\
  (var_e y |--> Y ** var_e b2k |--> B2K ** var_e x |--> X ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil) s h /\
  Zbeta nk * Sum nk X =m Sum nk Y * Sum nk B2K {{ Sum nk M }} /\ Sum nk X < Sum nk M) **
 (fun s h => u2Z [i]_s = Z_of_nat ni /\ u2Z [n]_s = Z_of_nat nn /\
  [l]_s = vl /\ u2Z [L_]_s = u2Z vl + 4 * Z_of_nat ni /\
  u2Z [thirtytwo]_s = Z_of_nat 32 /\ u2Z [j]_s = Z_of_nat nj /\
  (var_e l |--> L ** add_e (var_e y) (int_e (Z2u 32 (Z_of_nat (4 * nk)))) |~> int_e zero32) s h /\
  list_flat (map (@bits 32) (firstn ni L)) = bbs_fun_rec (ni * 32) (Sum nk X0 ^^ 2 mod Sum nk M) (Sum nk M) /\
  (ni < nn)%nat /\ (nj < 32)%nat /\ [w]_s = vw /\
  firstn nj (bits vw) = bbs_fun_rec nj ((Sum nk X0 ^^ 2 mod Sum nk M) ^^ power 2 (ni * 32) mod Sum nk M) (Sum nk M) /\
  skipn nj (bits vw) = ListBit.zeros (32 - nj) /\
  Zbeta nk * Sum nk Y =m Sum nk X0 ^^ power 2 (ni * 32 + S nj) {{ Sum nk M }})).

move=> {X HlenX} s h [h1 [h2 [Hdisj [Hunion [
[X [HlenX [r_y [r_one' [r_x [r_m [r_k [r_alpha [Hmem1 [Sum_X X_M]]]]]]]]]]
[r_i [r_n [r_l [r_L_ [r_32 [r_j [Hmem2 [Hbbs' [Hninn [Hnj32 [r_w [Hbbs [Hbbs'' Sum_Y]]]]]]]]]]]]]
]]]]].
exists X; repeat (split; trivial).
rewrite (decompose_last_equiv _ Y) HlenY.
move: {Hmem1 Hmem2}(assert_m.con_cons _ _ _ _ _ Hdisj Hmem1 Hmem2).
rewrite -Hunion => Hmem.
by assoc_comm Hmem.
eapply eqmod_trans; last by apply Sum_Y.
apply eqmod_sym in Sum_X.
rewrite Zmult_comm in Sum_X.
move: (eqmod_rewrite _ _ _ _ _ HSumB2K1 Sum_X) => Htmp.
rewrite -Zpower_b_square -Zmult_assoc Zmult_comm in Htmp.
apply eqmod_sym in Htmp.
rewrite Zmult_comm in Htmp.
apply eqmod_reg_mult' in Htmp => //.
rewrite /Zbeta.
by apply Zis_gcd_sym, Zis_gcd_Zpower_odd.

apply frame_rule.
- eapply mont_mul_strict_init_triple; trivial.
  by abstract Nodup_nodup r0.
- by Inde_frame.
- move=> ?; by Inde_mult.

lw w' zero16 x;

apply hoare_lw_back_alt'' with (fun s h => exists X, exists vw, exists nj,
  u2Z [i]_s = Z_of_nat ni /\ length X = nk /\ u2Z [k]_s = Z_of_nat nk /\
  u2Z [n]_s = Z_of_nat nn /\ [x]_s = vx /\ [y]_s = vy /\
  [m]_s = vm /\ [b2k]_s = vb2k /\ [alpha]_s = valpha /\ [l]_s = vl /\
  u2Z [L_]_s = u2Z vl + 4 * Z_of_nat ni /\ u2Z [thirtytwo]_s = Z_of_nat 32 /\
  u2Z [j]_s = Z_of_nat nj /\
  (var_e x |--> X ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil ** var_e l |--> L ** var_e y |--> Y ++ zero32 :: nil ** var_e b2k |--> B2K) s h /\
  list_flat (map (@bits 32) (firstn ni L)) = bbs_fun_rec (ni * 32) (Sum nk X0 ^^ 2 mod Sum nk M) (Sum nk M) /\
  (ni < nn)%nat /\ (nj < 32)%nat /\ [w]_s = vw /\
  firstn nj (bits vw) = bbs_fun_rec nj ((Sum nk X0 ^^ 2 mod Sum nk M) ^^ power 2 (ni * 32) mod Sum nk M) (Sum nk M) /\
  skipn nj (bits vw) = ListBit.zeros (32 - nj) /\
  Sum nk X =m Sum nk X0 ^^ power 2 (ni * 32 + S nj) {{ Sum nk M }} /\ Sum nk X < Sum nk M /\
  [w']_s = nth O X zero32).

move=> {X HlenX} s h [X [Hri [HlenX [Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [HrL_ [Hr32 [Hrj [mem [Hbbs' [Hninn [Hnj32 [Hrw [Hbbs [Hbbs'' [Sum_X Sum_X']]]]]]]]]]]]]]]]]]]]]].

have Htmp : [ add_e (var_e x) (int_e (sext 16 zero16)) ]e_ s = [ var_e x ]e_ s.
  by rewrite /= sext_0 add_0.
destruct X as [|Xhd Xtl]; first by destruct nk.
exists Xhd; split.
rewrite /= !assert_m.con_assoc_equiv in mem.
move: mem; apply monotony => // h'.
by apply mapsto_ext.
rewrite /update_store_lw.
exists (Xhd :: Xtl), vw, nj.
repeat reg_upd; repeat (split; trivial).
by Assert_upd.

andi w' w' one16 ;

apply hoare_andi with (fun s h => exists X, exists vw, exists nj,
  u2Z [i]_s = Z_of_nat ni /\ length X = nk /\ u2Z [k]_s = Z_of_nat nk /\
  u2Z [n]_s = Z_of_nat nn /\ [x]_s = vx /\ [y]_s = vy /\
  [m]_s = vm /\ [b2k]_s = vb2k /\ [alpha]_s = valpha /\
  [l]_s = vl /\ u2Z [L_]_s = u2Z vl + 4 * Z_of_nat ni /\
  u2Z [thirtytwo]_s = Z_of_nat 32 /\ u2Z [j]_s = Z_of_nat nj /\
  (var_e x |--> X ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil ** var_e l |--> L ** var_e y |--> Y ++ zero32 :: nil ** var_e b2k |--> B2K) s h /\
  list_flat (map (@bits 32) (firstn ni L)) = bbs_fun_rec (ni * 32) (Sum nk X0 ^^ 2 mod Sum nk M) (Sum nk M) /\
  (ni < nn)%nat /\ (nj < 32)%nat /\ [w]_s = vw /\
  firstn nj (bits vw) = bbs_fun_rec nj ((Sum nk X0 ^^ 2 mod Sum nk M) ^^ power 2 (ni * 32) mod Sum nk M) (Sum nk M) /\
  skipn nj (bits vw) = ListBit.zeros (32 - nj) /\
  Sum nk X =m Sum nk X0 ^^ power 2 (ni * 32 + S nj) {{ Sum nk M }} /\ Sum nk X < Sum nk M /\
  [w']_s = nth O X zero32 [.&] one32).

move=> {X HlenX vw nj} s h [X [vw [nj [Hri [HlenX [Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [HrL_ [Hr32 [Hrj [Hmem [Hbbs' [Hninn [Hnj32 [Hrw [Hbbs [Hbbs'' [Sum_X [Sum_X' r_w']]]]]]]]]]]]]]]]]]]]]]]]].
rewrite /wp_andi.
repeat reg_upd.
exists X, vw, nj; repeat (split; trivial).
by Assert_upd.
by rewrite r_w' zext_Z2u.


apply hoare_sllv with (fun s h => exists X, exists vw, exists nj,
  u2Z [i]_s = Z_of_nat ni /\ length X = nk /\ u2Z [k]_s = Z_of_nat nk /\
  u2Z [n]_s = Z_of_nat nn /\ [x]_s = vx /\ [y]_s = vy /\
  [m]_s = vm /\ [b2k]_s = vb2k /\ [alpha]_s = valpha /\
  [l]_s = vl /\ u2Z [L_]_s = u2Z vl + 4 * Z_of_nat ni /\
  u2Z [thirtytwo]_s = Z_of_nat 32 /\ u2Z [j]_s = Z_of_nat nj /\
  (var_e x |--> X ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil ** var_e l |--> L ** var_e y |--> Y ++ zero32 :: nil ** var_e b2k |--> B2K) s h /\
  list_flat (map (@bits 32) (firstn ni L)) = bbs_fun_rec (ni * 32) (Sum nk X0 ^^ 2 mod Sum nk M) (Sum nk M) /\
  (ni < nn)%nat /\ (nj < 32)%nat /\ [w]_s = vw /\
  firstn nj (bits vw) = bbs_fun_rec nj ((Sum nk X0 ^^ 2 mod Sum nk M) ^^ power 2 (ni * 32) mod Sum nk M) (Sum nk M) /\
  skipn nj (bits vw) = ListBit.zeros (32 - nj) /\
  Sum nk X =m Sum nk X0 ^^ power 2 (ni * 32 + S nj) {{ Sum nk M }} /\ Sum nk X < Sum nk M /\
  [w']_s = (nth O X zero32 [.&] one32) [.<<] nj).

move=> {X HlenX vw nj} s h [X [vw [nj [Hri [HlenX [Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [HrL_ [Hr32 [Hrj [Hmem [Hbbs' [Hninn [Hnj32 [Hrw [Hbbs [Hbbs'' [Sum_X [Sum_X' Hrw']]]]]]]]]]]]]]]]]]]]]]]]].
rewrite /wp_sllv.
repeat reg_upd.
exists X, vw, nj; repeat (split; trivial).
by Assert_upd.
have -> : u2Z ([j]_s [.%] 5) = Z_of_nat nj.
  rewrite u2Z_rem' //= Hrj (_ : 32 = Z_of_nat 32) //; by apply inj_lt.
by rewrite Hrw' Zabs_nat_Z_of_nat.

cmd_or w w w' ;

apply hoare_or with (fun s h => exists X, exists vw, exists nj,
  u2Z [i]_s = Z_of_nat ni /\ length X = nk /\ u2Z [k]_s = Z_of_nat nk /\
  u2Z [n]_s = Z_of_nat nn /\ [x]_s = vx /\ [y]_s = vy /\
  [m]_s = vm /\ [b2k]_s = vb2k /\ [alpha]_s = valpha /\
  [l]_s = vl /\ u2Z [L_]_s = u2Z vl + 4 * Z_of_nat ni /\
  u2Z [thirtytwo]_s = Z_of_nat 32 /\ u2Z [j]_s = Z_of_nat nj /\
  (var_e x |--> X ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil ** var_e l |--> L ** var_e y |--> Y ++ zero32 :: nil ** var_e b2k |--> B2K) s h /\
  list_flat (map (@bits 32) (firstn ni L)) = bbs_fun_rec (ni * 32) (Sum nk X0 ^^ 2 mod Sum nk M) (Sum nk M) /\
  (ni < nn)%nat /\ (nj < 32)%nat /\
  firstn (S nj) (bits vw) = bbs_fun_rec (S nj) ((Sum nk X0 ^^ 2 mod Sum nk M) ^^ power 2 (ni * 32) mod Sum nk M) (Sum nk M) /\
  skipn (S nj) (bits vw) = ListBit.zeros (32 - S nj) /\
  Sum nk X =m Sum nk X0 ^^ power 2 (ni * 32 + S nj) {{ Sum nk M }} /\ Sum nk X < Sum nk M /\
  [w]_s = vw).

move=> {X HlenX vw nj} s h [X [vw [nj [Hri [HlenX [Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [HrL_ [Hr32 [Hrj [Hmem [Hbbs' [Hninn [Hnj32 [Hrw [Hbbs [Hbbs'' [Sum_X [Sum_X' Hrw']]]]]]]]]]]]]]]]]]]]]]]]].
rewrite /wp_or.
repeat reg_upd.
exists X, (int_or ((nth O X zero32 [.&] one32) [.<<] nj) vw), nj; repeat (split; trivial).
by Assert_upd.

rewrite bbs_fun_rec_app0 -Hbbs [mult]lock [firstn]lock /= -!lock.
rewrite (firstn_S true); last by rewrite length_bits.
rewrite Zpower_exp_mod Zmult_1_r Zpower_b_square -power_is_exp Zpower_exp_mod -power_S plus_n_Sm {1}bits_int_or (ListBit.heads_or_lst 32); last 2 first.
  by rewrite length_bits.
  by rewrite length_bits.
rewrite firstn_bits // (ListBit.or_lst_comm nj); last 2 first.
  by rewrite ListBit.len_zeros.
  rewrite (len_firstn 32) //; last 2 first.
    by apply length_bits.
    by apply lt_le_weak.
rewrite ListBit.or_lst_zeros; last first.
  rewrite (len_firstn 32) //; by [apply length_bits | apply lt_le_weak].
rewrite bits_int_or (ListBit.nth_or_lst 32); last 2 first.
  by apply length_bits.
  by apply length_bits.
rewrite nth_bits //.
rewrite (skipn_S true) in Hbbs''; last by rewrite length_bits.
rewrite (_ : 32 - nj = S (32 - S nj))%nat in Hbbs''; last by rewrite minus_Sn_m.
rewrite [minus]lock /= -lock in Hbbs''.
case: Hbbs'' => -> _.
rewrite ListBit.bit_or_o -(Zodd_bool_multi nk) //.
have Htmp : 0 < Sum nk M by apply Zle_lt_trans with (Sum nk X); [by apply min_Sum | exact Sum_X'].
apply eqmod_mod in Sum_X => //.
apply eqmod_inv in Sum_X; last 2 first.
  split; [by apply min_Sum | done].
  by apply Z_mod_lt, Zlt_gt.
by rewrite Sum_X.

rewrite bits_int_or (ListBit.skipn_or_lst 32); last 2 first.
  by apply length_bits.
  by apply length_bits.
rewrite skipn_bits // (ListBit.or_lst_comm (32 - S nj)); last 2 first.
  by rewrite ListBit.len_zeros.
  by rewrite len_skipn length_bits.
rewrite ListBit.or_lst_zeros //.
- rewrite skipn_tail Hbbs'' ListBit.tail_zeros.
  + by rewrite -ssrnat.minusE // (_ : 32 - nj - 1 = 32 - S nj)%nat // minus_minus plus_comm.
  + rewrite {1}(_ : O = 32 - 32)%nat //; apply minus_lt_compat; [exact Hnj32 | by apply le_refl].
  by rewrite len_skipn length_bits.
- by rewrite -Hrw' Hrw int_or_comm.


apply hoare_addiu'.

move=> {X HlenX vw nj} s h [X [vw [nj [Hri [HlenX [Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [HrL_ [Hr32 [Hrj [Hmem [Hbbs' [Hninn [Hnj32 [Hbbs [Hbbs'' [Sum_X [Sum_X' Hrw]]]]]]]]]]]]]]]]]]]]]]]].
rewrite /wp_addiu.
repeat reg_upd.
exists X, Y, vw, (S nj).
repeat (split; trivial).
rewrite sext_Z2u // u2Z_add_Z2u // Hrj.
rewrite Z_S; ring.
apply Zlt_trans with 33; [idtac | done].
rewrite (_ : 33 = Z_of_nat 32 + 1) //; by apply Zplus_lt_compat_r, inj_lt.
by Assert_upd.

sw w zero16 L ;

apply hoare_sw_back'' with (fun s h => exists X, exists Y, exists vw, exists L,
 u2Z [i]_s = Z_of_nat ni /\ length X = nk /\ length Y = nk /\
 length L = nn /\ u2Z [k]_s = Z_of_nat nk /\ u2Z [n]_s = Z_of_nat nn /\
 [x]_s = vx /\ [y]_s = vy /\ [m]_s = vm /\ [b2k]_s = vb2k /\
 [alpha]_s = valpha /\ [l]_s = vl /\ u2Z [L_]_s = u2Z vl + 4 * Z_of_nat ni /\
 u2Z [thirtytwo]_s = Z_of_nat 32 /\ u2Z [j]_s = Z_of_nat 32 /\
 (var_e x |--> X ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil ** var_e l |--> L ** var_e y |--> Y ++ zero32 :: nil ** var_e b2k |--> B2K) s h /\
 list_flat (map (@bits 32) (firstn (S ni) L)) = bbs_fun_rec ((S ni) * 32) (Sum nk X0 ^^ 2 mod (Sum nk M) mod (Sum nk M)) (Sum nk M) /\
 (ni < nn)%nat /\ [w]_s = vw /\
 Sum nk X =m Sum nk X0 ^^ power 2 ((S ni) * 32) {{ Sum nk M }} /\ Sum nk X < Sum nk M).

move=> s h [X [Y [vw [r_i [len_X [len_Y [r_k [r_n [r_x [r_y [r_m [r_b2k [r_alpha [r_l [r_L_ [r_32 [r_j [mem [Hbbs' [ni_nn [r_w [Hbbs [Sum_X X_M]]]]]]]]]]]]]]]]]]]]]]].

have Htmp : [ add_e (var_e L_) (int_e (sext 16 zero16)) ]e_ s =
  [ add_e (var_e l) (int_e (Z2u 32 (Z_of_nat (4 * ni)))) ]e_ s.
  rewrite [mult]lock /= -lock sext_0 // add_0; apply u2Z_inj.
  rewrite r_L_ u2Z_add_Z2u.
  by rewrite r_l inj_mult.
  by apply Zle_0_nat.
  rewrite r_l inj_mult [Z_of_nat 4]/= -Zbeta1_Zpower2.
  eapply Zlt_trans; last by apply Hnl.
  apply Zplus_lt_compat_l, Zmult_lt_compat_l => //; by apply inj_lt.

exists (int_e (nth ni L zero32)).

Decompose_32 L ni L1 L2 HlenL1 HL'; last by rewrite HlenL.

rewrite HL' (decompose_equiv _ _ _ _ _ HlenL1) !assert_m.con_assoc_equiv assert_m.con_com_equiv !assert_m.con_assoc_equiv assert_m.con_com_equiv !assert_m.con_assoc_equiv assert_m.con_com_equiv !assert_m.con_assoc_equiv in mem.
move: mem; apply monotony => // ht.
by apply mapsto_ext.
apply currying => h' H'; simpl app in H'.
exists X, Y, vw, (update_list L ni vw); repeat (split; trivial).
by apply len_update_list.
rewrite HL' update_list_app HlenL1 // -minus_n_n /= (decompose_equiv _ _ _ _ _ HlenL1).
assoc_comm H'.
move: H'; by apply mapsto_ext.

rewrite (firstn_S zero32); last by rewrite (len_update_list nn).
rewrite nth_update_list; last by rewrite HlenL.
rewrite map_app list_flat_app. simpl list_flat. rewrite {1}(mult_comm (S ni)) bbs_fun_rec_app -(mult_comm ni).
by rewrite -app_nil_end Hbbs firstn_update_list Hbbs' !Zmod_mod.

clear L HlenL.

addiu L L four16 ;

apply hoare_addiu with (fun s h => exists X, exists Y, exists vw, exists L,
 u2Z [i]_s = Z_of_nat ni /\ length X = nk /\ length Y = nk /\
 length L = nn /\ u2Z [k]_s = Z_of_nat nk /\ u2Z [n]_s = Z_of_nat nn /\
 [x]_s = vx /\ [y]_s = vy /\ [m]_s = vm /\ [b2k]_s = vb2k /\
 [alpha]_s = valpha /\ [l]_s = vl /\
 u2Z [L_]_s = u2Z vl + 4 * Z_of_nat (S ni) /\
 u2Z [thirtytwo]_s = Z_of_nat 32 /\ u2Z [j]_s = Z_of_nat 32 /\
 (var_e x |--> X ++ zero32 :: nil ** var_e m |--> M ++ zero32 :: nil ** var_e l |--> L ** var_e y |--> Y ++ zero32 :: nil ** var_e b2k |--> B2K) s h /\
 list_flat (map (@bits 32) (firstn (S ni) L)) = bbs_fun_rec ((S ni) * 32) (Sum nk X0 ^^ 2 mod (Sum nk M)) (Sum nk M) /\
 (ni < nn)%nat /\ [w]_s = vw /\
 Sum nk X =m Sum nk X0 ^^ power 2 ((S ni) * 32) {{Sum nk M}} /\ Sum nk X < Sum nk M).

move=> s h [X [Y [vw [L [Hri [HlenX [HlenY [HlenL [Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [HrL_ [Hr32 [Hrj [Hmem [Hbbs [Hninn [Hrw [Sum_X X_M]]]]]]]]]]]]]]]]]]]]]]]].
rewrite /wp_addiu.
repeat reg_upd.
exists X, Y, vw, L; repeat (split; trivial).

rewrite sext_Z2u // u2Z_add_Z2u // HrL_.
rewrite Z_S; ring.
rewrite -Zbeta1_Zpower2; eapply Zle_lt_trans; last by apply Hnl.
  rewrite -Zplus_assoc; apply Zplus_le_compat_l.
  rewrite -{2}(Zmult_1_r 4) -Zmult_plus_distr_r -Z_S.
  apply Zmult_le_compat => //; by apply inj_le.
by Assert_upd.
by rewrite Zmod_mod in Hbbs.

addiu i i one16).

apply hoare_addiu'.

move=> s h [X [Y [vw [L [Hri [HlenX [HlenY [HlenL [Hrk [Hrn [Hrx [Hry [Hrm [Hrb2k [Hralpha [Hrl [HrL_ [Hr32 [Hrj [Hmem [Hbbs' [Hninn [Hrw [Sum_X X_M]]]]]]]]]]]]]]]]]]]]]]]].
rewrite /wp_addiu.
repeat reg_upd.
exists (S ni), L, X, Y; repeat (split; trivial).
rewrite sext_Z2u // u2Z_add_Z2u // Hri.
by rewrite Z_S.
rewrite -Zbeta1_Zpower2; eapply Zlt_trans; last by apply Hnl.
  rewrite -(Zplus_0_l (Z_of_nat ni + 1)).
  apply Zplus_le_lt_compat; first by apply min_u2Z.
  rewrite -Z_S Zmult_comm -(Zmult_1_r (Z_of_nat (S ni))); apply Zmult_lt_compat2 => //.
  split; by [apply Z_of_nat_lt0, lt_0_Sn | apply inj_le].
by Assert_upd.
Qed.