Library multi_sub_signed_signed_simu

Require Import ssreflect ssrbool eqtype.
Require Import ZArith_ext Lists_ext.
Require Import machine_int nodup multi_int.
Import MachineInt.
Require Import mips_bipl.
Import expr_m.
Require Import simu.
Import simu_m.
Require Import multi_sub_signed_signed_prg multi_sub_signed_signed_triple.

Local Open Scope machine_int_scope.
Local Open Scope mips_expr_scope.
Local Open Scope zarith_ext_scope.
Local Open Scope assoc_scope.
Local Open Scope nodup_scope.
Local Open Scope heap_scope.

Require Import seq.

Lemma pfwd_sim_multi_sub_s_s : forall (y A : assoc.l) d
  L rk ry rA a0 a1 a2 a3 a4 ret X Y,
  nodup(y, A) ->
  nodup(rk, ry, rA, a0, a1, a2, a3, a4, ret, X, Y, r0) ->
  disj (mints_regs (seq_ext.s2l (assoc.cdom d))) (a0 :: a1 :: a2 :: a3 :: a4 :: ret :: X :: Y :: List.nil)%list ->
  A \notin assoc.dom d -> y \notin assoc.dom d ->
  signed L rA \notin assoc.cdom d -> unsign rk ry \notin assoc.cdom d ->
   pfwd_sim (state_mint (A |=> signed L rA \U+ (y |=> signed L ry \U+ d)))
   (fun s st _ => [rk ]_ st <> zero32 /\
     u2Z ([rk ]_ st) < 2 ^^ 31 /\
     L = Zabs_nat (u2Z ([rk ]_ st)) /\
     Zabs ([A ]_ s)%seplog_expr < Zbeta L /\
     Zabs ([y ]_ s)%seplog_expr < Zbeta L /\
     Zabs (([A ]_ s)%seplog_expr - ([y ]_ s)%seplog_expr) < Zbeta L)
   (A <- (var_e A .-e var_e y)%seplog_expr)%seplog_cmd
   (multi_sub_s_s rk rA ry a0 a1 a2 a3 a4 ret X Y).
Proof.
move=> y A d L rk ry rA a0 a1 a2 a3 a4 ret X Y y_A Hreg Hd A_d y_d rA_d ry_d.
rewrite /multi_sub_s_s.
Admitted.

Lemma pfwd_sim_multi_sub_s_s_wo_overflow : forall (y A : assoc.l) d
  L rk ry rA a0 a1 a2 a3 a4 ret X Y,
  nodup(y, A) ->
  nodup(rk, ry, rA, a0, a1, a2, a3, a4, ret, X, Y, r0) ->
  disj (mints_regs (seq_ext.s2l (assoc.cdom d))) (a0 :: a1 :: a2 :: a3 :: a4 :: ret :: X :: Y :: List.nil)%list ->
  A \notin assoc.dom d -> y \notin assoc.dom d ->
  signed L rA \notin assoc.cdom d -> unsign rk ry \notin assoc.cdom d ->
  pfwd_sim (state_mint (A |=> signed L rA \U+ (y |=> signed L ry \U+ d)))
  (fun s st _ => [rk ]_ st <> zero32 /\
    u2Z ([rk ]_ st) < 2 ^^ 31 /\
    L <> O /\
    L = S (Zabs_nat (u2Z ([rk ]_ st))) /\
    Zabs ([A ]_ s)%seplog_expr < Zbeta (L - 1) /\
    Zabs ([y ]_ s)%seplog_expr < Zbeta (L - 1))
  (A <- (var_e A .-e var_e y)%seplog_expr)%seplog_cmd
  (multi_sub_s_s rk rA ry a0 a1 a2 a3 a4 ret X Y).
Proof.
Admitted.

Lemma safe_termination_multi_sub_s_s : forall x B L d
  rk rx rB a0 a1 a2 a3 a4 ret X Y,
  nodup(rk, rx, rB, a0, a1, a2, a3, a4, ret, X, Y, r0) ->
  safe_termination (state_mint (B |=> signed L rB \U+ (x |=> signed L rx \U+ d)))
  (multi_sub_s_s rk rB rx a0 a1 a2 a3 a4 ret X Y).
Proof.
Admitted.