Unfinished RLP proof

rlp.v

From Coq Require Import ssreflect ssrfun ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Init.Nat.
Require Import Coq.Lists.List.
Require Import Coq.Strings.Byte.
Require Import Arith Omega.
Require Import Coq.Arith.Even.
Require Import Psatz.
From Equations Require Import Equations.
Export ListNotations.


Definition Encoding := list byte.

Inductive RLP :=
  |tip : Encoding -> RLP
  |node : list RLP -> RLP.

Equations? div (n m : nat) : nat * nat by wf n lt :=
  div 0 (S y) := (0, 0);
  div x 0 := (0, 0);
  div x (S y) := if (S x) <=? (S y) then
                 (0, x)
             else
                 let (div, rest) := div (x - (S y)) (S y) in
                 (div+1, rest).
lia.
Defined.

Theorem correct_div : forall x y,
  let (div, rest) := div x (S y) in x = ((S y) * div) + rest.
intros.
funelim(div x (S y)).
simp div.
lia.
remember (S (S n) <=? S n0).
destruct b.
rewrite <- Heqcall.
lia.
simp div.
rewrite <- Heqb.
simpl.
simpl in H, Heqcall.
symmetry in Heqb.
pose(leb_complete_conv _ _ Heqb).
remember (n - n0) .
destruct n1.
simp div.
simpl.
replace (n0 * 1 + 0) with n0 by lia.
lia.
destruct (div (S n1) (S n0)).
simpl in *.
replace (n2 + 1) with (S n2) by lia.
rewrite Heqn1 in H.
simpl.
assert(n = 
 n2 + n0 * n2 + n3 + n0) by lia.
rewrite H0.
lia.
Qed.

Definition divide x y := (div x y).1.
Definition module x y := (div x y).2.

Theorem correct_div2 : forall x y,
  x = (S y * divide x (S y)) + module x (S y).
  intros.
  pose (correct_div x y).
  unfold divide; unfold module.
  move : y0.
  destruct (div x (S y)).
  auto.
Qed.

Theorem well_rec_division : forall x y, divide (S x) (S (S y)) < S x.
intros.  
unfold divide.
pose(correct_div (S x) (S y)).
move : y0.
destruct (div (S x) (S (S y))).
intros.
simpl in *.
lia.
Qed.

Theorem mod_less : forall x y, module (S x) (S y) <= S x.
intros.  
unfold module.
pose(correct_div (S x) y).
move : y0.
destruct (div (S x) (S y)).
intros.
simpl.
lia.
Qed.


Theorem mod_less2 : forall x y, module x y <= y.
intros.
unfold module.
funelim(div x y).
simp div; trivial.
simpl div; auto with arith.
simp div; trivial.
simp div.
remember (S (S n) <=? S n0).
destruct b.
simpl.
pose (leb_complete _ _ (eq_sym Heqb)).
auto with arith.
destruct (div (S n - S n0) (S n0)).
simpl in *.
assumption.
Qed.

Equations? base_256 (n : nat) : Encoding by wf n lt :=
  base_256 0 := [];
  base_256 (S n1) := match (of_nat (module (S n1) 256)) with
      |Some x => x :: base_256 (divide (S n1) 256)
      |None => []
    end.
apply : well_rec_division.
Qed.

Fixpoint from_base256 (ls : Encoding) {struct ls} : nat := match ls with
   |[] => 0
   |[x] => to_nat x 
   |x :: xs => (to_nat x) + from_base256 xs * 256
  end.

Theorem module_256_bytes : forall x, {b | of_nat (module x 256) = Some b}.
  move => x.
  have : (module x 256) <= 256 by apply : mod_less2.
  move => H.
  generalize dependent (module x 256).
  move => n H2.
Admitted. (* This is not axiom, we are not just going to 256 cases *)

Theorem identity_base_256 : forall x, from_base256 (base_256 x) = x.
  intros.
  funelim (base_256 x).
  trivial.
  intros.
  destruct (module_256_bytes (S n)).
  rewrite e.
  pose (H x).
  generalize dependent e0.
  clear H.
  move => H.
  simpl.
  destruct (zerop (divide (S n) 256)).
  rewrite e0.
  simp base_256.
  rewrite e0 in H.
  simp base_256 in H.
  simpl in *.
  pose (correct_div2 (S n) 255).
  move : e1.
  rewrite e0.
  move => H1.
  simpl in H1.
  rewrite H1.
  by apply : to_of_nat.
  rewrite H.
  have : to_nat x = (module (S n) 256) by apply :  to_of_nat.
  move => H1; rewrite H1.
  clear H1.
  have :  base_256 (divide (S n) 256) <> [].
    destruct (divide (S n) 256).
    inversion l. 
    simp base_256.
    destruct (module_256_bytes (S n0)).
    rewrite e0.
    congruence.
  move => H1.
  remember (base_256 (divide (S n) 256)).
  destruct e0.
  congruence.
  pose (correct_div2 (S n) 255).
  rewrite Nat.add_comm.
  rewrite Nat.mul_comm.
  by symmetry.
Qed.
  
Definition rlp_length_encoding (len : nat) (offSet : nat) : Encoding.
refine (if len <=? 55 then _ else _).
destruct (of_nat (offSet + len)).
exact ([b]).
exact [].
refine (let b := rev (base_256 len) in _).
destruct (of_nat (length b + offSet + 55)).
exact (b0 :: b).
exact [].
Defined.

Fixpoint rlp_encode (x : RLP) : Encoding.
destruct x.
refine (if (length e =? 1) && (to_nat(hd x00 e) <=? 127) then _ else _).
exact e.
exact (rlp_length_encoding (length e) 128 ++ e).
refine (let encode_all :=
   fold_left (fun pred y => pred ++ rlp_encode y) l [] in _).
exact (rlp_length_encoding (length encode_all) 192 ++ encode_all).
Defined.

Definition pretty x := map to_nat x.
Definition to_binary x := map of_nat x.

Fixpoint repeat_ls {A} (x : A) (n : nat) := match n with
  | 0 => []
  |(S n) => x :: repeat_ls x n
 end.


Definition split {A} (ls : list A) (n : nat) := (firstn n ls, skipn n ls).

Inductive RLP_PREFIXES :=
   | prefix_error
   | prefix_128
   | prefix_184
   | prefix_192
   | prefix_248
   | prefix_255.

Definition rlp_decode_length (len : nat) (prefix : byte) (rest : Encoding) :=
   if to_nat prefix - len <=? 55 then
     split rest (to_nat prefix - len)
   else
     let H := split rest ((to_nat prefix - len) - 55) in
       split (snd H) (from_base256 (rev (fst H))).


Compute rlp_decode_length 150 xff
  [x00; x00; x00; x00; x00; x00; x00; x00; x00; x00; x00; x00; x00; x00; x00; x00; 
  x00; x00; x00; x00; x00; x00].


Fixpoint interval (intervals : list nat) (n : nat) (p : nat) : nat.
destruct intervals.
exact p.
exact (if n <=? n0 then p else S (interval intervals n p)).
Defined.

Theorem to_solve_later :
  forall P : Type, P.
Admitted.

Equations? rlp_decode (x : Encoding) : list RLP by wf (length x) lt :=
rlp_decode [] => [];
rlp_decode (b :: xs) => (match interval [127; 191; 247] (to_nat b) 0
                          as c return c = interval [127; 191; 247] (to_nat b) 0 -> list RLP with
    |0 =>  fun H => tip [b] :: rlp_decode xs
    |1 =>  fun H => tip (fst (rlp_decode_length 128 b xs)) 
           :: rlp_decode (snd (rlp_decode_length 128 b xs))
    |(S (S n)) => fun H => let H1 := (rlp_decode_length 192 b xs) in 
                    node (rlp_decode (fst H1)) :: rlp_decode (snd H1)
   end) eq_refl.

(*remember (to_nat b <=? 127).
destruct b0.
inversion H.
remember (to_nat b <=? 191).
destruct b0.
unfold rlp_decode_length.
admit.
inversion H.
remember (to_nat b <=? 127).
destruct b0.
inversion H.
remember ( to_nat b <=? 191).
destruct b0.
inversion H.
unfold rlp_decode_length.
remember (to_nat b <=? 247).
destruct b0.
admit.
admit.
admit. *)
apply : to_solve_later.
apply : to_solve_later.
apply : to_solve_later.
Defined.

Definition decode x := hd (node []) (rlp_decode x).

Compute decode (rlp_encode (node [tip [x00]])).


Theorem of_nat_bound : forall x, x <= 255 -> {y | (of_nat x) = Some y /\ to_nat y = x}.
Admitted.


Theorem div_cutting : forall x y z, x <= y -> divide (S x) (S z) <= divide (S y) (S z).
intros.
Admitted.

Compute base_256 1000.

Theorem base_256_bound : forall x, x <= 256 ^ (length (base_256 x)).
intros.
funelim (base_256 x).
auto with arith.
pose (H x00 (j - 1)).
destruct j.
admit.
simp base_256 in H0.
remember (of_nat (module (S n) 256)).
destruct o.
simpl in H0.
have : length (base_256 (divide (S n) 256)) <= j - 0 by lia.
move => H1.
apply l in H1.
rewrite (correct_div2 (S n) 255).
rewrite Nat.pow_succ_r'.
have : divide (S n) 256 + module (S n) 256 <= 256 ^ j.
lia.
Admitted.

Theorem base_256_bound : forall x, x <= 256 ^(length (base_256 x)) .
intros.
funelim (base_256 x).
auto with arith.
set (H xff).
destruct (module_256_bytes (S n)).
rewrite e.
replace (length (x :: base_256 (divide (S n) 256))) with (S (length (base_256 (divide (S n) 256)))).
rewrite Nat.pow_succ_r'.
pose (correct_div2 (S n) 255).
erewrite e0 at 1.
pose (correct_div2 (S n) 255).
have : 256 * divide (S n) 256 = S n - module (S n) 256.
lia.
move => H1.
clear e0.
rewrite Nat.pow_succ_r'.
pose(mod_less n 256).
pose (well_rec_division n 254).
unfold lt in l1.
have : (divide (S n) 256) <= S n.
lia.
move => H3.
lia.
have : divide (S n) 256 <= S n.
pose(mod_less2 (S n) 255).
have : n <= S y * z -> 
Search (pow _ _ = _).
have : 255 ^ S (length (base_256 (divide (S n) 256))) = (255 * (255 ^ (length (base_256 (divide (S n) 256))))).
simpl.
by simpl.
Admitted.

Theorem take_all_list : forall {A} (x : list A), fst (split x (length x)) = x.
intros.
unfold split.
simpl.
apply : firstn_all2.
trivial.
Qed.

Theorem rlp_identity : forall  x, decode (rlp_encode x) = x.
intros.
destruct x.
simpl.
remember ((length e =? 1) && (to_nat (hd "000"%byte e) <=? 127)).
destruct b.
destruct (proj1 (Bool.andb_true_iff _ _) (eq_sym Heqb)).
unfold decode.
destruct e.
inversion H.
simp rlp_decode.
remember (interval [127; 191; 247] (to_nat b) 0).
destruct n.
simpl.
destruct e.
trivial.
inversion H.
simpl in Heqn.
remember (to_nat b <=? 127).
destruct b0.
inversion Heqn.
simpl in H0.
congruence.
destruct e.
simpl.
unfold decode.
simp rlp_decode.
remember (interval [127; 191; 247] (to_nat "128") 0).
destruct n.
simpl.
inversion Heqn.
simpl in Heqn.
destruct n.
trivial.
inversion Heqn.
simpl.
pose (proj1 (Bool.andb_false_iff _ _) (eq_sym Heqb)).
destruct o.
simpl in H.
destruct e.
inversion H.
unfold rlp_length_encoding.
remember (S (length (b0 :: e)) <=? 55).
destruct b1.
pose (proj1 (Nat.leb_le _ _) (eq_sym Heqb1)).
have: (128 + S (length (b0 :: e))) <= 255.
lia.
move => H3.
destruct (of_nat_bound H3).
destruct a. 
rewrite H0.
simpl.
unfold decode.
simp rlp_decode.
remember (interval [127; 191; 247] (to_nat x) 0).
destruct n.
simpl in Heqn.
remember (to_nat x <=? 127).
destruct b1.
rewrite H1 in Heqb0.
inversion Heqb0.
inversion Heqn.
simpl in Heqn.
remember ( to_nat x <=? 127).
destruct b1.
inversion Heqn.
remember (to_nat x <=? 191).
destruct b1.
have : n = 0 by congruence.
move => Hn0.
rewrite Hn0.

simpl.
clear Heqn.
unfold rlp_decode_length.
have : to_nat x > 127 /\ to_nat x <= 191.
constructor.
by apply : leb_complete_conv.
by apply : leb_complete.
move => H4.
destruct H4.
have : to_nat x - 128 <= 55.
lia.
move => H5.
pose (leb_correct _ _ H5).
rewrite e0.
have : to_nat x = 128 + S (length (b0 :: e)).
apply : to_of_nat.
assumption.
move => H6.
rewrite H6.
have : (128 + S (length (b0 :: e)) - 128) = S (length (b0 :: e)).
lia.
move => H7.
rewrite H7.
by rewrite take_all_list.
have : n = S (if to_nat x <=? 247 then 0 else 1) by congruence.
move => H2.
rewrite H2.
simpl.
have : to_nat x =  128 + S (length (b0 :: e)).
apply : to_of_nat.
assumption.
move => H4.
rewrite H4 in Heqb2.
pose (leb_complete_conv _ _ (eq_sym Heqb2)).
lia
Admitted.