Module Bijection

Require Import Coqlib.
Require Import Registers.

Require Import List.
Require Import Lia.
Require Import Bool.

Require Import FunInd.

Open Scope nat_scope.

Fixpoint pos2list (p:positive) : list bool :=
  match p with
    | xH => nil
    | xO p => false :: pos2list p
    | xI p => true :: pos2list p
  end.

Fixpoint list2pos (l:list bool) : positive :=
  match l with
    | nil => xH
    | false :: l => xO (list2pos l)
    | true :: l => xI (list2pos l)
  end.

Lemma list2pos_pos2list : forall p, list2pos (pos2list p) = p.

Lemma pos2list_list2pos : forall l, pos2list (list2pos l) = l.

Fixpoint fill (n:nat) (l:list bool) : list bool :=
  match n with
    | O => l
    | S n => false :: fill n l
  end.

Lemma length_fill : forall n l, length (fill n l) = n + length l.

Definition complete (n:nat) (l:list bool) : list bool :=
  fill (n - length l) l.

Lemma length_complete : forall n l,
  length l <= n -> length (complete n l) = n.

Fixpoint remove_first_zeros (l:list bool) : list bool :=
  match l with
    | nil => nil
    | false::l => remove_first_zeros l
    | _ => l
  end.

Lemma remove_first_zeros_fill : forall n l,
  remove_first_zeros (fill n (true::l)) = true::l.

Lemma remove_first_zeros_complete : forall n l,
  remove_first_zeros (complete n (true::l)) = true::l.

Lemma remove_first_zeros_fill_nil : forall n,
  remove_first_zeros (fill n nil) = nil.

Lemma remove_first_zeros_complete_nil : forall n,
  remove_first_zeros (complete n nil) = nil.

Lemma list2pos_not_xH : forall l,
  list2pos l = xH -> forall x, In x l -> x = false.

Lemma In_l_In_fill : forall n l x, In x l -> In x (fill n l).

Definition encode (n:nat) (p:positive) : list bool :=
  if Reg.eq p xH then (complete n nil)
    else (complete n (true :: (pos2list (Pos.pred p)))).

Definition decode (n:nat) (l:list bool) : positive :=
  match remove_first_zeros l with
    | true :: l => Pos.succ (list2pos l)
    | _ => xH
  end.

Lemma decode_encode : forall n p, decode n (encode n p) = p.

Function log_lower (p:positive) (n:nat) {struct n} : bool :=
  match p, n with
    | xH, _ => true
    | xO p, S n => log_lower p n
    | xI p, S n => log_lower p n
    | _, _ => false
  end.

Lemma log_lower_length_pos2list : forall p n,
  log_lower p n = true -> length (pos2list p) <= n.


Lemma log_lower_Pdouble_minus_one : forall p n,
  log_lower p n = true -> log_lower (Pdouble_minus_one p) (S n) = true.

Lemma log_lower_pred : forall p n,
  log_lower p n = true -> log_lower (Pos.pred p) n = true.

Lemma length_encode : forall n p,
  log_lower p n = true -> length (encode (S n) p) = S n.

Lemma remove_first_zeros_nil : forall n l,
  length l = n ->
  remove_first_zeros l = nil ->
  fill n nil = l.

Lemma length_remove_first_zeros : forall l,
  length l >= length (remove_first_zeros l).

Lemma remove_first_zeros_not_nil : forall n l l0,
  length l = n + S (length l0) ->
  remove_first_zeros l = true :: l0 ->
  fill n (true :: l0) = l.

Lemma remove_first_zeros_not_false : forall l l0,
  remove_first_zeros l <> false :: l0.

Lemma encode_decode : forall n l,
  length l = n ->
  encode n (decode n l) = l.

Fixpoint split (n:nat) (l:list bool) : (list bool) * (list bool) :=
  match n with
    | O => (nil,l)
    | S n =>
      match l with
        | nil => (nil,nil)
        | b::l => let (l1,l2) := split n l in (b::l1,l2)
      end
  end.

Lemma split_concat : forall n l1 l2,
  length l1 = n ->
  split n (app l1 l2) = (l1,l2).

Lemma concat_split : forall n l,
  l = app (fst (split n l)) (snd (split n l)).

Lemma length_fst_split : forall n l,
  (n <= length l)%nat -> length (fst (split n l)) = n.

Definition toPair (n:nat) (p:positive) : positive * positive :=
  let (l1,l2) := split n (pos2list p) in
    (decode n l1, list2pos l2).

Definition fromPair (n:nat) (p1_p2:positive*positive) : positive :=
  let (p1,p2) := p1_p2 in
    list2pos (app (encode n p1) (pos2list p2)).

Fixpoint app_positive (p1 p2:positive) : positive :=
  match p1 with
    | xH => p2
    | xO p1 => xO (app_positive p1 p2)
    | xI p1 => xI (app_positive p1 p2)
  end.

Lemma app_positive_prop : forall l1 l2,
  app_positive (list2pos l1) (list2pos l2) = list2pos (app l1 l2).

Fixpoint fill_positive (n:nat) (p:positive) : positive :=
  match n with
    | O => p
    | S n => xO (fill_positive n p)
  end.

Lemma fill_positive_prop : forall n l,
  fill_positive n (list2pos l) = list2pos (fill n l).

Fixpoint length_positive (p:positive) : nat :=
  match p with
    | xH => O
    | xO p => S (length_positive p)
    | xI p => S (length_positive p)
  end.

Lemma length_positive_prop : forall l,
  length_positive (list2pos l) = length l.

Definition complete_positive (n:nat) (p:positive) : positive :=
  fill_positive (n - length_positive p) p.

Definition encode_positive (n:nat) (p:positive) : positive :=
  if Reg.eq p xH then (complete_positive n xH)
    else (complete_positive n (xI (Pos.pred p))).

Definition fromPair_V2 (n:nat) (p1_p2:positive*positive) : positive :=
  let (p1,p2) := p1_p2 in
    app_positive (encode_positive n p1) p2.

Lemma fromPair_V2_prop : forall n p,
  fromPair_V2 n p = fromPair n p.

Lemma toPair_fromPair : forall n p1 p2,
  log_lower p1 n = true ->
  toPair (S n) (fromPair (S n) (p1,p2)) = (p1,p2).

Function log_greater (p:positive) (n:nat) {struct n} : bool :=
  match n, p with
    | O, _ => true
    | S n, xO p => log_greater p n
    | S n, xI p => log_greater p n
    | _, _ => false
  end.

Lemma log_greater_length_pos2list : forall p n,
  log_greater p n = true -> n <= length (pos2list p).

Lemma log_greater_length_pos2list_inv : forall n p,
  n <= length (pos2list p) -> log_greater p n = true.

Lemma log_lower_length_pos2list_inv : forall n p,
  length (pos2list p) <= n -> log_lower p n = true.

Fixpoint not_all_one (p:positive) : bool :=
  match p with
    | xH => true
    | xO p => true
    | xI p => not_all_one p
  end.

Lemma log_lower_implies_log_greater : forall p1 p2 n,
  log_lower p1 n = true ->
  log_greater (fromPair (S n) (p1,p2)) (S n) = true.

Lemma length_pos2list_Psucc : forall p,
  length (pos2list (Pos.succ p)) <= S (length (pos2list p)).

Lemma fromPair_toPair : forall n p,
  log_greater p n = true -> fromPair n (toPair n p) = p.

Module Type RTL_SSA_MAPPING.

  Definition index := positive.
  Definition size := nat.

  Parameter rmap : size -> reg -> reg * index.
  Parameter pamr : size -> reg * index -> reg.
  Parameter valid_index : size -> index -> bool.
  Parameter valid_reg_ssa : size -> reg -> bool.

  Parameter from_valid_index_to_valid_reg_ssa : forall size i,
    valid_index size i = true ->
    forall r, valid_reg_ssa size (pamr size (r,i)) = true.
  Parameter from_valid_reg_ssa_to_valid_index : forall size ri,
    valid_reg_ssa size ri = true -> valid_index size (snd (rmap size ri)) = true.

  Parameter INJ' : forall size r1 i1 r2 i2,
    valid_index size i1 = true ->
    valid_index size i2 = true ->
    pamr size (r1,i1) = pamr size (r2,i2) ->
    (r1,i1) = (r2,i2).

  Parameter INJ : forall size r1 r2,
    valid_reg_ssa size r1 = true ->
    valid_reg_ssa size r2 = true ->
    rmap size r1 = rmap size r2 ->
    r1 = r2.

  Parameter BIJ1 : forall size r i,
    valid_index size i = true -> rmap size (pamr size (r,i)) = (r,i).

  Parameter BIJ2 : forall size ri,
    valid_reg_ssa size ri = true -> pamr size (rmap size ri) = ri.

End RTL_SSA_MAPPING.

Module Bij : RTL_SSA_MAPPING.

  Definition index := positive.
  Definition size := nat.

  Definition rmap size r :=
    let (i,r) := toPair size r in (r,i).

  Definition pamr size (ri:positive*positive) :=
    let (r,i) := ri in fromPair_V2 size (i,r).

  Definition valid_index size i :=
    match size with
      | O => false
      | S n => log_lower i n
    end.

  Definition valid_reg_ssa size r :=
    match size with
      | O => false
      | S n => log_greater r size && log_lower (fst (toPair (S n) r)) n
    end.

  Lemma from_valid_index_to_valid_reg_ssa : forall size i,
    valid_index size i = true ->
    forall r, valid_reg_ssa size (pamr size (r,i)) = true.
  
  Lemma from_valid_reg_ssa_to_valid_index2 : forall size ri r i,
    valid_reg_ssa size ri = true -> rmap size ri = (r,i) -> valid_index size i = true.

  Lemma from_valid_reg_ssa_to_valid_index : forall size ri,
      valid_reg_ssa size ri = true -> valid_index size (snd (rmap size ri)) = true.
  
  Lemma BIJ1 : forall size r i,
    valid_index size i = true -> rmap size (pamr size (r,i)) = (r,i).

  Lemma BIJ2 : forall size ri,
    valid_reg_ssa size ri = true -> pamr size (rmap size ri) = ri.

  Lemma INJ' : forall size r1 i1 r2 i2,
    valid_index size i1 = true ->
    valid_index size i2 = true ->
    pamr size (r1,i1) = pamr size (r2,i2) ->
    (r1,i1) = (r2,i2).

  Lemma INJ : forall size r1 r2,
    valid_reg_ssa size r1 = true ->
    valid_reg_ssa size r2 = true ->
    rmap size r1 = rmap size r2 ->
    r1 = r2.

End Bij.