Library mont_mul_strict_termination

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Require Import ZArith_ext seq_ext machine_int uniq_tac.
Import MachineInt.
Require Import mips_cmd mips_tactics mips_contrib.
Import expr_m.
Require Import mont_mul_strict_prg mont_mul_termination multi_lt_termination.
Require Import multi_sub_u_u_termination multi_zero_u_termination.

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

Lemma mont_mul_strict_termination s h k alpha x y z m one ext int_ X_ B2K_ Y_ M_ quot C_ t s_ :
  uniq(k, alpha, x, y, z, m, one, ext, int_, X_, B2K_, Y_, M_, quot, C_, t, s_, r0) ->
  { si | Some (s, h) -- mont_mul_strict k alpha x y z m one ext int_ X_ B2K_ Y_ M_ quot C_ t s_ ---> si }.
Proof.
move=> Hset; rewrite /mont_mul_strict.
apply exists_seq_P2 with (fun si => True).
- case/(termination_montgomery s h) : Hset => si Hsi; by exists si.
- move=> [si hi] Psi.
  + apply exists_ifte.
    * apply exists_seq_P2 with (fun _ => True).
      - have : uniq(k, z, m, X_, B2K_, int_, ext, M_, Y_, r0) by Uniq_uniq r0.
        case/(multi_lt_termination si hi) => sj Hsj; by exists sj.
      - move=> [sj hj] Psj.
        + apply exists_ifte.
          * have : uniq(k, m, z, ext, int_, quot, C_, M_, B2K_, r0) by Uniq_uniq r0.
            move/(multi_sub_u_u_termination sj hj z) => [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 : uniq(ext, m, z, Y_, int_, quot, C_, M_, B2K_, r0) by Uniq_uniq r0.
      set s0 := store.upd _ _ _. set h0 := heap.upd _ _ _.
      move/(multi_sub_u_u_termination s0 h0 z) => [sk Hk].
      eexists; by apply Hk.
Qed.

Lemma mont_mul_strict_init_termination s h k alpha x y z m one ext int_ X_ B2K_ Y_ M_ quot C_ t s_ :
  uniq(k, alpha, x, y, 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 y z m one ext int_ X_ B2K_ Y_ M_ quot C_ t s_ ---> si }.
Proof.
move=> Hset; rewrite /mont_mul_strict_init.
apply exists_seq_P2 with (fun _ => True).
- have : uniq(k, z, ext, M_, r0) by Uniq_uniq r0.
  case/(multi_zero_u_termination s h) => si Hsi; by exists si.
- move=> [si hi] Psi.
  + apply exists_seq_P2 with (Q := fun sj => True).
    * by apply exists_mflhxu_seq_P, exists_mthi_seq_P, exists_mtlo_P.
    * move=> [sj hj] HPsj.
      - have : uniq(k, alpha, x, y, z, m, one, ext, int_, X_, B2K_, Y_, M_, quot, C_, t, s_, r0) by Uniq_uniq r0.
        case/(mont_mul_strict_termination sj hj) => x0 Hx0; by exists x0.
Qed.