Library mont_square_termination

Require Import ssreflect ssrbool.
Require Import ZArith_ext Lists_ext.
Require Import machine_int.
Import MachineInt.
Require Import mips_cmd mips_tactics mips_contrib.
Import mips_bipl.expr_m.
Require Import mont_mul_prg mont_mul_termination.

Local Open Scope machine_int_scope.
Local Open Scope mips_expr_scope.
Local Open Scope mips_cmd_scope.

Lemma termination_mont_square :
  forall s h k alpha x z m one ext int_ X_ B2K_ Y_ M_ quot C_ t s_,
  nodup (k :: alpha :: x :: z :: m :: one :: ext :: int_ :: X_ :: B2K_ :: Y_ :: M_ ::
  quot :: C_ :: t :: s_ :: r0 :: nil) ->
    { si | Some (s, h) -- montgomery k alpha x x z m one ext int_ X_ B2K_ Y_ M_ quot C_ t s_ ---> si }.
Proof.
move=> s h k alpha x z m one ext int_ X_ B2K_ Y_ M_ quot C_ t s_ Hset.
rewrite /montgomery.
apply exists_addiu_seq.
rewrite store.get_r0 add_com add_0 sext_Z2u //.
apply exists_addiu_seq.
repeat reg_upd.
rewrite sext_Z2u // add_0.
apply exists_addiu_seq.
repeat reg_upd.
rewrite sext_Z2u // add_0.
set s0 := store.upd _ _ _.
have [kext Hkext] : { kext | u2Z [k]_s0 - u2Z [ext]_s0 = Z_of_nat kext }.
  have [zext Hkext] : { zext | u2Z [k]_s0 - u2Z [ext]_s0 = zext }.
    eapply exist; reflexivity.
  have : 0 <= zext.
    rewrite -Hkext {2}/s0.
    repeat reg_upd.
    rewrite /zero32 u2Z_Z2u // Zminus_0_r; by apply min_u2Z.
  case/Z_of_nat_complete_inf => next Hzext.
  exists next; by rewrite -Hzext.
move: kext s0 Hkext h.
elim.
- move=> s0 Hkext h.
  eapply exist.
  apply while.exec_while_false.
  rewrite /= in Hkext *; apply/negPn; apply/Zeq_boolP; omega.
- move=> kext IH s0 Hkext h.
  apply exists_while.
  + rewrite /=; apply/negP. apply/negPn. apply/Zeq_boolP.
    rewrite Z_S in Hkext; omega.
  + apply exists_seq_P2 with (fun st, u2Z [k]_(fst st) - u2Z [ext]_(fst st) = Z_of_nat kext).
    * exists_lwxs l_x H_l_x z_x Hz_x.
      exists_lw l_y H_l_y z_y Hz_y.
      exists_lw l_z H_l_z z_z Hz_z.
      apply exists_multu_seq_P.
      exists_lw l_m_ H_l_m z_m_ Hz_m_.
      apply exists_maddu_seq_P.
      repeat reg_upd.
      apply exists_mflo_seq_P.
      repeat reg_upd.
      apply exists_mfhi_seq_P.
      repeat reg_upd.
      apply exists_multu_seq_P.
      repeat reg_upd.
      apply exists_addiu_seq_P.
      repeat reg_upd.
      apply exists_mflo_seq_P.
      repeat reg_upd.
      apply exists_mthi_seq_P.
      repeat reg_upd.
      apply exists_mtlo_seq_P.
      repeat reg_upd.
      apply exists_maddu_seq_P.
      repeat reg_upd.
      apply exists_mflhxu_seq_P.
      repeat reg_upd.
      apply exists_addiu_seq_P.
      repeat reg_upd.
      match goal with
        | |- { s' : option (store.t * heap.t) | (Some (?s0, _) -- _ ---> _) /\ _ } =>
          apply exists_seq_P with (fun x0 => forall st, x0 = Some st ->
            u2Z [k]_(fst st) - u2Z [ext]_(fst st) = Z_of_nat (S kext))
      end.
      - have : nodup (k :: x :: z :: m :: one :: ext :: int_ :: X_ :: B2K_ :: Y_ :: M_ :: quot :: t ::
          r0 :: nil) by Nodup_nodup r0.
        set _s := store.upd _ _ _.
        move/(termination_montgomery_inner_loop _s h (S kext)).
        have X : 0 < u2Z [int_ ]_ _s.
          rewrite /_s.
          repeat reg_upd.
          by rewrite add_com add_0 (@u2Z_sext 16) // u2Z_Z2u.
        move/(_ X) => {X}.
        have X : u2Z [int_ ]_ _s <= u2Z [k ]_ _s.
          rewrite /_s.
          repeat reg_upd.
          rewrite Z_S in Hkext.
          rewrite add_com add_0 (@u2Z_sext 16) // u2Z_Z2u //.
          move: (min_u2Z [ext ]_ s0) => ?; omega.
        move/(_ X) => {X}.
        assert ( X : u2Z [k ]_ _s - u2Z [ext ]_ _s = Z_of_nat (S kext)).
          rewrite /_s.
          repeat reg_upd.
          assumption.
        case/(_ X) => {X} si [Hsi1 Hsi2].
        exists si; split; first by assumption.
        move=> st Hst.
        destruct si as [[si hi]|]; last by done.
        case: Hst => ?; subst st.
        by move: (Hsi2 _ (refl_equal _)) => <-.
      - move=> [[si hi] | ] Hsi.
        + apply exists_maddu_seq_P.
          repeat reg_upd.
          apply exists_mflhxu_seq_P.
          repeat reg_upd.
          apply exists_addiu_seq_P.
          repeat reg_upd.
          exists_sw_P l_t H_l_t z_t H_z_t.
          apply exists_mflhxu_P.
          simpl fst.
          repeat reg_upd.
          move: {Hsi}(Hsi _ (refl_equal _)) => //.
          rewrite Z_S.
          simpl fst.
          repeat reg_upd.
          intuition.
          rewrite u2Z_add sext_Z2u // u2Z_Z2u //.
          omega.
          move: (max_u2Z ([k]_si)) => ?; omega.
        + exists None; split; [by apply while.exec_none | done].
    * move=> [ si hi ] Hsi.
      by apply IH.
Qed.