Library mont_square_strict_termination

Require Import ssreflect ssrbool eqtype.
Require Import ZArith_ext Lists_ext.
Require Import machine_int.
Import MachineInt.
Require Import mips_cmd mips_tactics mips_contrib.
Require Import mont_mul_strict_prg.
Require Import mont_square_termination multi_lt_termination multi_sub_termination multi_zero_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_mont_square_strict :
  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) ->
  {si | Some (s, h) --
    mont_mul_strict 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 /mont_mul_strict.
apply exists_seq_P2 with (fun si => True).
- case/(termination_mont_square s h) : (Hset) => si Hsi; by exists si.
- move=> [si hi] Psi.
  + apply exists_ifte.
    * apply exists_seq_P2 with (fun si => True).
      - have : nodup(k, z, m, X_, B2K_, int_, ext, M_, Y_, r0) by Nodup_nodup r0.
        case/(termination_multi_lt si hi) => sj Hsj.
        by exists sj.
      - move=> [sj hj] Psj.
        + apply exists_ifte.
          * have : nodup(k, m, z, ext, int_, quot, C_, M_, B2K_, r0) by Nodup_nodup r0.
            case/(termination_multi_sub sj hj) => sk Hk; by exists sk.
          * apply exists_nop; by move: {Psj}(Psj _ (refl_equal _)).
    * apply exists_addiu_seq.
      exists_sw_new l Hl z0 Hz0.
      repeat reg_upd.
      apply exists_addiu_seq.
      repeat reg_upd.
      have : nodup(ext, m, z, Y_, int_, quot, C_, M_, B2K_, r0) by Nodup_nodup r0.
      case/(termination_multi_sub
        (store.upd ext ([k ]_ si[.+]sext 16 one16) (store.upd t ([t ]_ si[.+]sext 16 four16) si)) (heap.upd l [C_ ]_ si hi)) => sk Hk.
      eexists; by apply Hk.
Qed.

Lemma termination_mont_square_strict_init :
  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) ->
  { si | Some (s, h) --
    mont_mul_strict_init 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 /mont_mul_strict_init.
apply exists_seq_P2 with (fun si => True).
- have : nodup(ext, k, M_, z, r0) by Nodup_nodup r0.
  case/(termination_multi_zero s h) => si Hsi.
  exists si; split; first by tauto.
  done.
- move=> [si hi] Psi.
  + apply exists_seq_P2 with (fun sj => True).
    * by apply exists_mflhxu_seq_P, exists_mthi_seq_P, exists_mtlo_P.
    * move=> [sj hj] Psj.
    - have : nodup(k, alpha, x, z, m, one, ext, int_, X_, B2K_, Y_, M_, quot, C_, t, s_, r0) by Nodup_nodup r0.
      case/(termination_mont_square_strict sj hj) => x0 Hx0; by exists x0.
Qed.