Library library_interfaces

Require Import ssreflect ssrbool eqtype seq.
Require Import Arith_ext ZArith_ext Lists_ext.
Require Import machine_int multi_int encode_decode integral_type.
Import MachineInt.
Local Open Scope machine_int_scope.
Require Import mips_bipl mips_seplog mips_tactics mips_syntax.
Import mips_bipl.expr_m.
Require Import simu.
Import simu.simu_m.

Require Import multi_zero_prg.
Require Import copy_prg.
Require Import abs_prg.
Require Import pick_sign_prg.
Require Import multi_add_prg.
Require Import multi_lt_prg.
Require Import multi_sub_prg.
Require Import multi_negate_prg.
Require Import multi_add_signed_unsigned_prg.
Require Import multi_sub_signed_unsigned_prg.
Require Import multi_div2_prg.
Require Import multi_is_even_prg.

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

Warning: This file contains only specifications and the corresponding code has not always been formally verified

Simulation of basic functions

Initialization with zero

Lemma pfwd_sim_zero_signed : forall (P : simu_m.relat) (x : bipl.var.v) d nk
  rx a0 a1 a2 a3,
  nodup(rx, a0, a1, a2, a3, r0) ->
  disj (mints_regs (seq_ext.s2l (assoc.cdom d))) (a0 :: a1 :: a2 :: a3 :: nil) ->
  x \notin assoc.dom d ->
  signed nk rx \notin (assoc.cdom d) ->
  pfwd_sim (state_mint (x |=> signed nk rx \U + d)) P
  (x <- nat_e%seplog_expr O)%seplog_cmd
  (multi_zero_signed rx a0 a1 a2 a3).
Proof.
Admitted.

Lemma safe_termination_zero_signed : forall a0 a1 a2 a3 nk rx x d,
  nodup(rx, a0, a1, a2, a3, r0) ->
  safe_termination (state_mint (x |=> signed nk rx \U + d))
  (multi_zero_signed rx a0 a1 a2 a3).
Proof.
Admitted.

Initialization with one

Definition multi_one (k z ext Z_ : reg) : while.cmd :=
  (multi_zero k z ext Z_;
   addiu ext r0 one16 ;
   sw ext zero16 z)%mips_cmd.

Lemma pfwd_sim_one : forall (x : bipl.var.v) d (rk rx a0 a1 : reg),
  nodup(rk, rx, a0, a1, r0) ->
  disj (mints_regs (seq_ext.s2l (assoc.cdom d))) (a0 :: a1 :: nil) ->
  x \notin assoc.dom d ->
  unsign rk rx \notin assoc.cdom d ->
  pfwd_sim (state_mint (x |=> unsign rk rx \U + d)) (fun _ _ _ => True)
  (x <- nat_e%seplog_expr 1%nat)%seplog_cmd
  (multi_one rk rx a0 a1).
Proof.
Admitted.

Lemma safe_termination_one : forall a0 a1 rx x rk d,
  nodup(rk, rx, a0, a1, r0) ->
  safe_termination
  (state_mint (x |=> unsign rk rx \U + d))
  (multi_one rk rx a0 a1).
Proof.
Admitted.

Initialization with one (signed variant)

Definition multi_one_signed (rx a0 a1 a2 a3 : reg) : while.cmd :=
  (multi_zero_signed rx a0 a1 a2 a3 ;
   lw a0 four16 rx ;
   addiu a1 r0 one16 ;
   sw a1 zero16 a0)%mips_cmd.

Lemma pfwd_sim_one_signed : forall (P : simu_m.relat) (x : bipl.var.v) d nk (rx a0 a1 a2 a3 : reg),
  nodup(rx, a0, a1, a2, a3, r0) ->
  disj (mints_regs (seq_ext.s2l (assoc.cdom d))) (a0 :: nil) ->
  x \notin assoc.dom d ->
  signed nk rx \notin assoc.cdom d ->
  pfwd_sim
  (state_mint (x |=> signed nk rx \U + d)) P
  (x <- nat_e%seplog_expr 1%nat)%seplog_cmd
  (multi_one_signed rx a0 a1 a2 a3).
Proof.
Admitted.

Lemma safe_termination_one_signed : forall a0 a1 a2 a3 nk rx x d,
  nodup(rx, a0, a1, a2, a3, r0) ->
  safe_termination
  (state_mint (x |=> signed nk rx \U + d))
  (multi_one_signed rx a0 a1 a2 a3).
Proof.
Admitted.

Array copy

Lemma pfwd_sim_copy : forall (P : simu_m.relat) (u x : bipl.var.v) d (rk ru rx a0 a1 a2 : reg),
  nodup(rk, ru, rx, a0, a1, a2, r0) ->
  disj (mints_regs (seq_ext.s2l (assoc.cdom d))) (a0 :: a1 :: a2 :: nil) ->
  unsign rk rx \notin assoc.cdom d ->
  unsign rk ru \notin assoc.cdom d ->
  pfwd_sim (state_mint
    (x |=> unsign rk rx \U + (u |=> unsign rk ru \U + d))) P
  (u <- var_e%seplog_expr x)%seplog_cmd
  (copy rk ru rx a0 a1 a2).
Proof.
Admitted.

Lemma safe_termination_copy : forall a0 a1 a2 rk rx x ru u d,
  nodup(rk, rx, ru, a0, a1, a2, r0) ->
  safe_termination
  (state_mint (x |=> unsign rk rx \U + (u |=> unsign rk ru \U + d)))
  (copy rk ru rx a0 a1 a2).
Proof.
Admitted.

Array copy (signed-unsigned variant)

Definition copy_signed_unsigned (rk rd rs a0 a1 a2 a3 : reg) : @while.cmd mips_cmd.cmd0 expr_b :=
  (lw a0 four16 rd ;
   copy rk a0 rs a1 a2 a3)%mips_cmd.

Lemma pfwd_sim_copy_signed_unsigned : forall (P : simu_m.relat) (u x : bipl.var.v) d (rk ru rx a0 a1 a2 a3 : reg) L,
  nodup(rk, ru, rx, a0, a1, a2, a3, r0) ->
  disj (mints_regs (seq_ext.s2l (assoc.cdom d))) (a0 :: a1 :: a2 :: a3 :: nil) ->
  unsign rk rx \notin assoc.cdom d ->
  signed L ru \notin assoc.cdom d ->
  pfwd_sim (state_mint
    (x |=> unsign rk rx \U + (u |=> signed L ru \U + d))) P
  (u <- var_e%seplog_expr x)%seplog_cmd
  (copy_signed_unsigned ru rk rx a0 a1 a2 a3).
Proof.
Admitted.

Lemma safe_termination_copy_signed_unsigned : forall a0 a1 a2 a3 rk rx x ru u d L,
  nodup(rk, rx, ru, a0, a1, a2, a3, r0) ->
  safe_termination
  (state_mint (x |=> unsign rk rx \U + (u |=> signed L ru \U + d)))
  (copy_signed_unsigned ru rk rx a0 a1 a2 a3).
Proof.
Admitted.

Array copy (signed-signed variant)

Definition copy_signed_signed (rd rs a0 a1 a2 a3 a4 : reg) : while.cmd :=
  (lw a0 four16 rd ;
   lw a1 four16 rs ;
   copy a4 a0 a1 a2 a3 a4)%mips_cmd.

Lemma pfwd_sim_copy_signed_signed : forall (P : simu_m.relat) (u x : bipl.var.v) d L (ru rx a0 a1 a2 a3 a4 : reg),
  nodup(ru, rx, a0, a1, a2, a3, a4, r0) ->
  disj (mints_regs (seq_ext.s2l (assoc.cdom d))) (a0 :: a1 :: a2 :: a3 :: a4 :: nil) ->
  signed L ru \notin assoc.cdom d ->
  signed L rx \notin assoc.cdom d ->
  pfwd_sim (state_mint (u |=> signed L ru \U + (x |=> signed L rx \U + d))) P
  (u <- var_e%seplog_expr x)%seplog_cmd
  (copy_signed_signed ru rx a0 a1 a2 a3 a4).
Proof.
Admitted.

Lemma safe_termination_copy_signed_signed : forall u x d L ru rx a0 a1 a2 a3 a4,
  nodup(ru, rx, a0, a1, a2, a3, a4, r0) ->
  safe_termination
  (state_mint (u |=> signed L ru \U + (x |=> signed L rx \U + d)))
  (copy_signed_signed ru rx a0 a1 a2 a3 a4).
Proof.
Admitted.

Signed addition (not in-place variant)

Lemma safe_termination_multi_add_s_u : forall A y L d
  rk rA ry a0 a1 a2 a3 a4 ret X,
  nodup(rk, rA, ry, a3, a0, a4, ret, a1, a2, X, r0) ->
  safe_termination (state_mint (A |=> signed L rA \U + (y |=> unsign rk ry \U + d)))
  (multi_add_s_u rk rA ry a0 a1 a2 a3 a4 ret X).
Proof.
Admitted.

z <- x + y with z, x signed and y unsigned

Definition multi_add_signed_signed_unsigned rk rz rx ry a0 a1 a2 a3 a4 ret X Z :=
  (lw Z four16 rz ;
   lw X four16 rx ;
   pick_sign rx a0 a1 ;
   while.ifte (expr_m.beq a1 r0)
   (addiu a3 r0 one16 ;
    multi_add rk a3 ry X Z a0 a1 a2 ;
    mflo a3)
   (multi_lt rk ry X a0 a1 ret a2 a3 a4 ;
    while.ifte (expr_m.beq ret r0)
    (multi_sub rk ry X Z a0 a1 a2 a3 a4 ret ;
     negate rz a0)
    (multi_sub rk X ry Z a0 a1 ret a3 a2 a4)))%mips_cmd.

Lemma pfwd_sim_multi_add_signed_signed_unsigned_wo_overflow : forall (z x y : assoc.l) d L
  rk rz rx ry a0 a1 a2 a3 a4 ret X Y,
  nodup(z, x, y) ->
  nodup(rz, rx, rk, ry, 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 ->
  z \notin assoc.dom d -> x \notin assoc.dom d -> y \notin assoc.dom d ->
  signed L rz \notin assoc.cdom d -> signed L rx \notin assoc.cdom d -> unsign rk ry \notin assoc.cdom d ->
   pfwd_sim
   (state_mint (z |=> signed L rz \U + (x |=> signed L rx \U + (y |=> unsign rk ry \U + d))))
   (fun s st _ => [rk ]_ st <> zero32 /\
     u2Z ([rk ]_ st) < 2 ^^ 31 /\
     L <> O /\
     L = Zabs_nat (u2Z ([rk ]_ st)) /\
     Zabs ([x ]_ s)%seplog_expr < Zbeta (L - 1) /\
     0 <= ([y ]_ s)%seplog_expr < Zbeta (L - 1))%mips_expr
   (z <- (var_e x +e var_e y)%seplog_expr)%seplog_cmd
   (multi_add_signed_signed_unsigned rk rz rx ry a0 a1 a2 a3 a4 ret X Y).
Proof.
Admitted.

Lemma safe_termination_multi_add_signed_signed_unsigned : forall z x y d L
  rz rx rk ry a0 a1 a2 a3 a4 ret X Y,
  nodup(rz, rx, rk, ry, a0, a1, a2, a3, a4, ret, X, Y, r0) ->
  safe_termination (state_mint
    (z |=> signed L rz \U +
    (x |=> signed L rx \U +
    (y |=> unsign rk ry \U + d))))
  (multi_add_signed_signed_unsigned rk rz rx ry a0 a1 a2 a3 a4 ret X Y).
Proof.
Admitted.

Signed subtraction (not in-place variant)

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

z <- x - y with z, x signed and y unsigned

Definition multi_sub_signed_signed_unsigned rk rz rx ry a0 a1 a2 a3 a4 ret X Z :=
  (lw Z four16 rz ;
   lw X four16 rx ;
   pick_sign rx a0 a1 ;
   while.ifte (expr_m.beq a1 r0)
   (multi_lt rk X ry a0 a1 ret a2 a3 a4 ;
    while.ifte (expr_m.beq ret r0)
    (multi_sub rk X ry Z a0 a1 a2 a3 a4 ret)
    (multi_sub rk ry X Z a0 a1 a2 a3 a4 ret ;
     negate rz a0)
   )
   (addiu a3 r0 one16 ;
    multi_add rk a3 ry X Z a0 a1 a2 ;
    mflo a3))%mips_cmd.

z <- x - y with z, x, y signed

Definition multi_sub_signed_signed_signed rk rz rx ry a0 a1 a2 a3 a4 ret X Y Z :=
  (lw Y four16 ry;
   pick_sign ry a0 a1 ;
   while.ifte (expr_m.beq a1 r0)
   (multi_sub_signed_signed_unsigned rk rz rx Y a0 a1 a2 a3 a4 ret X Z)
   (multi_add_signed_signed_unsigned rk rz rx Y a0 a1 a2 a3 a4 ret X Z))%mips_cmd.

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

Lemma safe_termination_multi_sub_signed_signed_signed : forall z x y d L
  rz rx rk ry a0 a1 a2 a3 a4 ret X Y Z,
  nodup(rz, rx, rk, ry, a0, a1, a2, a3, a4, ret, X, Y, Z, r0) ->
  safe_termination (state_mint
    (z |=> signed L rz \U +
    (x |=> signed L rx \U +
    (y |=> signed L ry \U + d))))
  (multi_sub_signed_signed_signed rk rz rx ry a0 a1 a2 a3 a4 ret X Y Z).
Proof.
Admitted.

Lemma pfwd_sim_multi_sub_signed_signed_unsigned_wo_overflow : forall (z x y : assoc.l) d L
  rk rz rx ry a0 a1 a2 a3 a4 ret X Y,
  nodup(z, x, y) ->
  nodup(rz, rx, rk, ry, 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 ->
  z \notin assoc.dom d -> x \notin assoc.dom d -> y \notin assoc.dom d ->
  signed L rz \notin assoc.cdom d -> signed L rx \notin assoc.cdom d -> unsign rk ry \notin assoc.cdom d ->
   pfwd_sim
   (state_mint (z |=> signed L rz \U + (x |=> signed L rx \U + (y |=> unsign rk ry \U + d))))
   (fun s st _ => [rk ]_ st <> zero32 /\
     u2Z ([rk ]_ st) < 2 ^^ 31 /\
     L <> O /\
     L = Zabs_nat (u2Z ([rk ]_ st)) /\
     Zabs ([x ]_ s)%seplog_expr < Zbeta (L - 1) /\
     0 <= ([y ]_ s)%seplog_expr < Zbeta (L - 1))%mips_expr
   (z <- (var_e x .-e var_e y)%seplog_expr)%seplog_cmd
   (multi_sub_signed_signed_unsigned rk rz rx ry a0 a1 a2 a3 a4 ret X Y).
Proof.
Admitted.

Lemma safe_termination_multi_sub_signed_signed_unsigned : forall z x y d L
  rz rx rk ry a0 a1 a2 a3 a4 ret X Y,
  nodup(rz, rx, rk, ry, a0, a1, a2, a3, a4, ret, X, Y, r0) ->
  safe_termination (state_mint
    (z |=> signed L rz \U +
    (x |=> signed L rx \U +
    (y |=> unsign rk ry \U + d))))
  (multi_sub_signed_signed_unsigned rk rz rx ry a0 a1 a2 a3 a4 ret X Y).
Proof.
Admitted.

Division by 2 (signed variant)

Definition multi_div2_s rx a0 a1 a2 a3 rk :=
  (lw rk zero16 rx ;
   abs rk a0 ;
   lw a0 four16 rx ;
   multi_div2 rk rx a0 a1 a2 a3)%mips_cmd.

Lemma pfwd_sim_div2_s : forall (P : simu_m.relat) (x : bipl.var.v) d nk
  rx a0 a1 a2 a3 a4,
  nodup(rx, a0, a1, a2, a3, a4, r0) ->
  disj (mints_regs (seq_ext.s2l (assoc.cdom d))) (a0 :: a1 :: a2 :: a3 :: a4 :: nil) ->
  x \notin assoc.dom d ->
  signed nk rx \notin assoc.cdom d ->
  pfwd_sim (state_mint (x |=> signed nk rx \U + d)) P
  (x <- var_e x ./e nat_e 2)%seplog_expr%seplog_cmd
  (multi_div2_s rx a0 a1 a2 a3 a4).
Admitted.

Lemma safe_termination_div2_s : forall a0 a1 a2 a3 a4 nk rx x d,
  nodup(rx, a0, a1, a2, a3, a4, r0) ->
  safe_termination
  (state_mint (x |=> signed nk rx \U + d))
  (multi_div2_s rx a0 a1 a2 a3 a4).
Admitted.

Negation

Lemma pfwd_sim_negate : forall (P : simu_m.relat) (x : bipl.var.v) d L
  rx a0,
  nodup(rx, a0, r0) ->
  disj (mints_regs (seq_ext.s2l (assoc.cdom d))) (a0 :: nil) ->
  x \notin assoc.dom d ->
  signed L rx \notin assoc.cdom d ->
  pfwd_sim (state_mint (x |=> signed L rx \U + d)) P
  (x <- .--e (var_e x))%seplog_expr%seplog_cmd
  (negate rx a0).
Admitted.

Lemma safe_termination_negate : forall a0 rx x L d, nodup(rx, a0, r0) ->
  safe_termination (state_mint (x |=> signed L rx \U + d)) (negate rx a0).
Admitted.

Conditionals

Sign testing

Lemma fwd_sim_b_pick_sign : forall x rx a0 a1 L d,
  nodup(rx, a0, a1, r0) ->
  fwd_sim_b
  (state_mint (x |=> signed L rx \U + d))
  (var_e x >>= nat_e 0)%seplog_expr (pick_sign rx a0 a1)
  (bgez a1).
Admitted.

Lemma fwd_sim_b_pick_sign_bne : forall x rx a0 a1 L d,
  fwd_sim_b
  (state_mint (x |=> signed L rx \U + d))
  (var_e x <>e nat_e 0)%seplog_expr (pick_sign rx a0 a1)
  (bne a1 r0).
Admitted.

Lemma fwd_sim_b_pick_sign_lez : forall x rx a0 a1 L d,
  fwd_sim_b
  (state_mint (x |=> signed L rx \U + d))
  (nat_e 0 >>= var_e x)%seplog_expr (pick_sign rx a0 a1)
  (blez a1).
Admitted.

Parity testing (signed variant)

Definition multi_is_even_signed (rx rk a0 : reg) :=
  (lw rk zero16 rx ;
   abs rk a0 ;
   lw a0 four16 rx ;
   multi_is_even rk rx a0)%mips_cmd.

Section multi_is_even_signed.

Variables rx rk a0 : reg.

Lemma multi_is_even_signed_triple : nodup(rx, rk, a0, r0) ->
  forall nk A slen ptr, length A = nk ->
    Zabs (s2Z slen) = Z_of_nat nk ->
    ({{ fun s h =>
      ((var_e rx |--> slen :: ptr :: nil ) ** (int_e ptr |--> A)) s h }}
    multi_is_even_signed rx rk a0
    {{ fun s h => (Zeven (Sum nk A) -> [a0]_s = one32) /\ (Zodd (Sum nk A) -> [a0]_s = zero32) }})
    %mips_expr%mips_assert%mips_hoare.
Admitted.

End multi_is_even_signed.

Lemma fwd_sim_b_multi_is_even_signed : forall x rx a0 a1 L d,
  fwd_sim_b
  (state_mint (x |=> signed L rx \U + d))
  (var_e x mode nat_e 2 =e nat_e 0)%seplog_expr
  (multi_is_even_signed rx a0 a1)
  (bne a1 r0).
Proof.
Admitted.

Definition multi_is_even_s_and rx ry a0 a1 a2 :=
  (multi_is_even_signed rx a0 a1 ; multi_is_even_signed ry a0 a2 ; cmd_and a0 a1 a2)%mips_cmd.

Lemma fwd_sim_b_multi_is_even_s_and : forall ru rv a0 a1 a2 u v d
  L,
  nodup(u, v) -> nodup(ru, rv, a0, a1, a2, r0) ->
  fwd_sim_b (fun s st h =>
    state_mint ((u |=> signed L ru \U + (v |=> signed L rv \U + d ))) s st h)
  (var_e u mode nat_e 2 =e nat_e 0 &e var_e v mode nat_e 2 =e nat_e 0)%seplog_expr
  (multi_is_even_s_and ru rv a0 a1 a2) (bne a0 r0).
Proof.
Admitted.