Library EVMOpSem.rlplem

Require Import Arith.
Require Import Bool.
Require Import List.
Require Import String.
Require Import Program.Wf.

Require Import Lem.coqharness.

Open Scope nat_scope.
Open Scope string_scope.


Require Import Lem.lem_pervasives.
Require Export Lem.lem_pervasives.

Require Import Lem.lem_word.
Require Export Lem.lem_word.

Require Import word256.
Require Export word256.

Require Import word160.
Require Export word160.

Require Import word8.
Require Export word8.

Require Import keccak.
Require Export keccak.

Definition byte0 : Type := word8 .
Definition byte0_default: byte0 := word8_default.

Inductive tree : Type :=
 | Leaf: list byte0 -> tree
 | Node: list tree -> tree .
Definition tree_default: tree := Leaf DAEMON.

Program Fixpoint BE_rev_prim (limit : nat ) (n : nat ) : list (word8 ):= match ( limit) with
 | 0%nat => []
 |S (limit) =>
   if beq_nat n( 0%nat) then [] else
   if nat_ltb n( 256%nat) then [word8FromNatural n] else
         (word8FromNatural ( Nat.modulo n( 256%nat)) :: BE_rev_prim limit ( Nat.div n( 256%nat)))
end.


Definition BE (n : nat ) : list (word8 ):= List.rev ((fun (n : nat ) => BE_rev_prim n n) n).

Definition BE_nat (n : nat ) : list (word8 ):= List.rev ((fun (n : nat ) => BE_rev_prim n n) ( n)).

Program Fixpoint BD_rev (lst : list (word8 )) : nat := match ( lst) with
 | [] => 0%nat
 | h :: t => Coq.Init.Peano.plus (Coq.Init.Peano.mult( 256%nat) (BD_rev t)) (word8ToNatural h)
end.

Definition BD (lst : list (word8 )) : nat := BD_rev (List.rev lst).

Definition r_b (lst : list (word8 )) : list (word8 ):= match ( lst) with
 | [] => [(word8FromNumeral 128%nat)]
 | [k] => if nat_ltb (word8ToNat k)( 128%nat) then [k] else [(word8FromNumeral 129%nat); k]
 | lst =>
   if nat_ltb (List.length lst)( 56%nat) then word8FromNat ( Coq.Init.Peano.plus( 128%nat) (List.length lst)) :: lst
    else word8FromNat ( Coq.Init.Peano.plus( 183%nat) (List.length (BE_nat (List.length lst)))) :: (@ List.app _)(BE_nat (List.length lst)) lst
end.

Definition read_n_bytes (n : nat ) (lst : list (word8 )) : option ((list (word8 )*list (word8 )) % type) :=
  if nat_gteb (List.length lst) n then Some (take n lst, drop n lst)
  else None.

Definition de_r_b (lst : list (word8 )) : option ((list (word8 )*list (word8 )) % type) := match ( lst) with
 | [] => None
 | k :: lst =>
   if classical_boolean_equivalence k(word8FromNumeral 128%nat) then Some ([], lst)
   else if w8Less k(word8FromNumeral 128%nat) then Some ([k], lst)
   else if w8Less k(word8FromNumeral 184%nat) then
       (let len := Coq.Init.Peano.minus (word8ToNat k)( 128%nat) in
       (if nat_gteb (List.length lst) len then Some (take len lst, drop len lst)
                                         else None))
   else if w8LessEqual k(word8FromNumeral 192%nat) then
      match ( read_n_bytes ( Coq.Init.Peano.minus(word8ToNat k)( 183%nat)) lst) with
       | None => None
       | Some (be_bytes, x_and_rest) =>
         read_n_bytes ( (BD be_bytes)) x_and_rest
      end
   else None
end.

Program Fixpoint RLP (tree1 : tree ) : list (word8 ):= match ( tree1) with
 | Leaf l => r_b l
 | Node lst =>
   let s := lem_list.concat (List.map RLP lst) in
   let len_s := List.length s in
   if nat_ltb len_s( 56%nat) then word8FromNat ( Coq.Init.Peano.plus( 192%nat) len_s) :: s
   else word8FromNat ( Coq.Init.Peano.plus( 247%nat) (List.length (BE_nat len_s))) :: ( (@ List.app _)(BE_nat len_s) s)
end.

Definition RLP_nat (i : nat ) : list (byte0 ):= RLP (Leaf (BE i)).

Definition RLP_w256 (i : (Bvector 256) ) : tree := Leaf (BE (Z.abs_nat ((two_compl_value 255 i)))).

Definition word_rsplit160 (w : word160 ) : list (keccak.byte ):= (word_rsplit_aux (boolListFromWord160 w)( 20%nat)).

Definition RLP_address (addr : word160 ) : tree := Leaf (word_rsplit160 addr).