Require Import compcert.lib.Coqlib.
Require Import Bvector.
Require Import List.
Require Import compcert.lib.Integers.
Require Import BinNums.
Require Import VST.msl.Axioms.
Require Import FCF.Blist.
Import List.
Require Import Lia.

Require Import sha.ByteBitRelations.
Require Import sha.hmac_pure_lemmas.
Require Import sha.general_lemmas.
Require Import sha.HMAC_functional_prog.
Require Import sha.HMAC_common_defs.
Require Import sha.HMAC_spec_abstract.
Require Import sha.HMAC_equivalence.

(*SHA256-specific Modules*)
Require Import sha.common_lemmas.
Require Import sha.HMAC256_functional_prog.
Require Import sha.sha_padding_lemmas.
Require Import sha.ShaInstantiation.
Require Import sha.hmac_common_lemmas.
Require Import sha.HMAC256_spec_pad.
Require Import sha.HMAC256_spec_concat.
Require Import sha.HMAC256_spec_list. (*for toBlocks*)

(*
Lemma of_length_proof_irrel {A:Set} n (l: list A) M:
      Vector.to_list (@of_list_length _ n l M) = l.
Proof. destruct M. apply Vector.to_list_of_list_opp. Qed.
*)
(*Section EQUIV.*)
(*Definition h_v (iv:Bvector c) (blk:Bvector b): Bvector c :=
  of_list_length _
   (sha_h_length _ _ (VectorToList_length _ iv) (VectorToList_length _ blk)).

Lemma h_eq : forall (block_v : Bvector b) (block_l : Blist)
               (HVL: block_l = Vector.to_list block_v)
               ivA ivB (IV: ivA = Vector.to_list ivB),
               sha_h ivA block_l = Vector.to_list (h_v ivB block_v).
Proof. intros. unfold h_v, of_list_length.
  destruct (sha_h_length (Vector.to_list ivB) (Vector.to_list block_v)
      (VectorToList_length c ivB) (VectorToList_length b block_v)).
  symmetry. subst. apply Vector.to_list_of_list_opp.
Qed.
*)

Definition iv_v : Bvector c := Vector.of_list sha_iv.

Lemma iv_eq : sha_iv = Vector.to_list iv_v.
Proof. unfold iv_v.
  rewrite <- Vector.to_list_of_list_opp.
  reflexivity.
Qed.
(*
Lemma opad_length: length (bytesToBits (HP.HMAC_SHA256.sixtyfour
                       (Integers.Byte.unsigned HP.Opad))) = b.
Proof. rewrite bytesToBits_len, length_SF. reflexivity. Qed.

Definition opad_v: Bvector b := of_list_length _ opad_length.

Lemma ipad_length: length (bytesToBits (HP.HMAC_SHA256.sixtyfour
                       (Integers.Byte.unsigned HP.Ipad))) = b.
Proof. rewrite bytesToBits_len, length_SF. reflexivity. Qed.

Definition ipad_v: Bvector b := of_list_length _ ipad_length.
*)
Lemma fpad_length (v:Bvector c): length (fpad (Vector.to_list v)) = p.
Proof. unfold fpad, fpad_inner. rewrite bytesToBits_len.
  repeat rewrite app_length. rewrite repeat_length, length_intlist_to_bytelist.
  rewrite (Nat.mul_comm 4), Nat.add_comm, Zlength_correct.
  rewrite bitsToBytes_len_gen with (n:=32%nat).
    reflexivity.
    apply VectorToList_length.
Qed.

Definition fpad_v (v:Bvector c): Bvector p := of_list_length _ (fpad_length v).

Lemma fpad_eq : forall (v : Bvector c) (l : Blist),
                  l = Vector.to_list v ->
                  fpad l = Vector.to_list (fpad_v v).
Proof. intros. unfold fpad_v, of_list_length.
  destruct (fpad_length v).
  rewrite Vector.to_list_of_list_opp.
  subst; reflexivity.
Qed.

Fixpoint splitAndPad_aux (m:list Blist) (M: Forall (fun x => length x = 512%nat) m):
           list (Bvector b) :=
(match m as l return (Forall (fun x => length x = 512%nat) l) -> list (Bvector b) with
  nil => fun F => nil
|  cons h t => fun F => cons (of_list_length h (Forall_inv F))
                    (splitAndPad_aux t (Forall_tl _ _ _ _ F))
 end) M.

Lemma splitAndPad_aux_consD h t M:
      splitAndPad_aux (cons h t) M
      = (of_list_length h (Forall_inv M))
         :: (splitAndPad_aux t (Forall_tl _ _ _ _ M)).
Proof. reflexivity. Qed.

Lemma splitAndPad_aux_nil m M: m=nil -> splitAndPad_aux m M= nil.
Proof. intros; subst. reflexivity. Qed.

Lemma length_splitandpad_inner_aux: forall ssm pf,
  Forall2
  (fun (bv : Vector.t bool b) (bl : list bool) => bl = Vector.to_list bv)
  (splitAndPad_aux (toBlocks ssm) pf)
  (toBlocks ssm).
Proof.
  intros ssm. remember (toBlocks ssm). generalize dependent ssm.
  induction l.
  { simpl; intros. constructor. }
  { intros. rewrite toBlocks_equation in Heql.
    destruct ssm. discriminate.
    remember ( Compare_dec.leb (length (b :: ssm)) 511) as d.
    destruct d. exfalso.
           rewrite Heql in pf. apply Forall_inv in pf.  clear Heql.
           rewrite firstn_length in pf.
           symmetry in Heqd. apply leb_complete in Heqd.
           eapply Nat.min_l_iff in pf. lia.
    rewrite splitAndPad_aux_consD.
    constructor.
      rewrite of_length_proof_irrel. trivial.
    eapply (IHl (skipn 512 (b :: ssm))).
      remember (firstn 512 (b :: ssm)) as zz.
      remember (toBlocks (skipn 512 (b :: ssm))) as yy.
      clear - Heql. inversion Heql. trivial. }
Qed.

Definition splitAndPad_v (m: Blist): list (Bvector b).
  apply (splitAndPad_aux (sha_splitandpad_blocks m)).
  apply InBlocks_Forall_512. apply sha_splitandpad_inc_InBlocks.
Defined.

Lemma splitAndPad_nil: exists pf,
  splitAndPad_v nil =
  cons (@of_list_length bool 512 (sha_splitandpad_inc nil) pf) nil.
Proof. unfold splitAndPad_v, sha_splitandpad_blocks.
  remember (InBlocks_Forall_512 _ (sha_splitandpad_inc_InBlocks nil)). clear Heqf.
  remember (toBlocks (sha_splitandpad_inc nil)).
  rewrite toBlocks_equation in Heql.
  remember (sha_splitandpad_inc nil) as m.
  destruct m. exfalso. clear Heql f l.
    unfold sha_splitandpad_inc in Heqm.
    assert (@length bool nil = length (bytesToBits (pad_inc (bitsToBytes nil)))).
      rewrite <- Heqm; trivial.
    simpl in H; clear Heqm. lia.
  rewrite leb_correct_conv in Heql.
    2: rewrite Heqm; simpl; lia.
  rewrite sublist.firstn_same in Heql.
    2: rewrite Heqm; simpl; lia.
  rewrite skipn_short in Heql.
    2: rewrite Heqm; simpl; lia.
  rewrite toBlocks_equation in Heql. subst l.
  simpl. eexists. reflexivity.
Qed.

Lemma length_splitandpad_inner m :
   Forall2
     (fun (bv : Vector.t bool b) (bl : list bool) => bl = Vector.to_list bv)
     (splitAndPad_v m) (sha_splitandpad_blocks m).
Proof. apply length_splitandpad_inner_aux. Qed.

Lemma C: Nat.divide 8 c.
  exists 32%nat. reflexivity.
Qed.

Module EQ256 <: EQUIV_Inst SHA256.
  Definition c := c.
  Definition C := C.
  Definition p := p.
  Definition b := b.
  Definition B := B.
  Definition BS: (SHA256.BlockSize * 8)%nat = b. reflexivity. Qed.
  Definition h := sha_h.
  Definition h_length := sha_h_length.
(*  Definition h_v := h_v.
  Definition h_eq := h_eq.*)
  Definition ir: list int := SHA256.init_registers.
(*  Definition iv:= sha_iv.*)
  Lemma iv_length: length (HMAC_spec_pad.convert ir) = c.
     apply sha_iv_length. Qed.
  (*Definition iv_length := sha_iv_length.*)
  Definition iv_v: Bvector c := iv_v. (*of_list_length _ iv_length.*)
  Lemma iv_eq: HMAC_spec_pad.convert ir  = Vector.to_list iv_v.
  Proof. reflexivity. Qed.
  (*
  Definition ipd:Z := 54.
  Definition opd:Z:=92.
  Lemma isbyteZ_Ipad: isbyteZ ipd.
    unfold ipd. split; lia. Qed.
  Lemma isbyteZ_Opad: isbyteZ opd.
    unfold opd. split; lia. Qed.*)
  Definition fpad_v := fpad_v.
  Definition fpad := fpad.
  Definition fpad_length msg: length msg = c -> length (fpad msg) = p.
  Proof. apply ShaInstantiation.fpad_length. Qed.
  Definition fpad_eq := fpad_eq.
  Definition splitAndPad := sha_splitandpad.
  Definition splitAndPad_v := splitAndPad_v.
  Definition splitandpad_blocks := sha_splitandpad_blocks.
  Definition sap_fpad:=sha_splitandpad_fpad.
  Definition shasplitandpad_blocks_b:= sha_splitandpad_blocks_512.
  Definition sap' m := concat (splitandpad_blocks m).
  Definition sap_app:forall (l m : Blist),
                         length l = b ->
                         splitAndPad (l ++ m) = l ++ sap' m.
  Proof. intros. rewrite sha_splitandpad_app; trivial.
    f_equal. unfold sap', splitandpad_blocks, sha_splitandpad_blocks.
    rewrite concat_toBlocks_id; trivial.
    apply sha_splitandpad_inc_InBlocks.
  Qed.
  Lemma sap'_InBlocks m: InBlocks b (sap' m).
    apply concat_InBlocks. apply sha_splitandpad_blocks_512. Qed.
  Definition hashblock : list int -> list int -> list int := SHA256.hash_block.
  Lemma HHB : h =
      (fun rgs bl : Blist =>
       intsToBits (hashblock (bitsToInts rgs) (bitsToInts bl))).
    reflexivity. Qed.

  Definition hashblocks: list int -> list int -> list int:= SHA256.hash_blocks.
  Definition d := 16%nat.

  Definition HBS_eq : forall r msg : list int,
         hashblocks r msg =
         match msg with
         | List.nil => r
         | _ :: _ => hashblocks (hashblock r (firstn d msg)) (skipn d msg)
         end := SHA256.hash_blocks_equation.
  Lemma D: (d * 32)%nat = b. reflexivity. Qed.

  Definition gap:list byte -> list int := SHA256.generate_and_pad.
  Lemma GAP: forall bits, Nat.divide d (length (gap (bitsToBytes bits))).
    intros. rewrite <- pad_compose_equal. apply gap_divide16. Qed.

  Lemma sap_gap: splitAndPad = fun bits => bytesToBits (intlist_to_bytelist (gap (bitsToBytes bits))).
  Proof. apply extensionality. intros l. unfold splitAndPad, sha_splitandpad.
    f_equal. rewrite <- pad_compose_equal. unfold generate_and_pad'.
    rewrite pure_lemmas.bytelist_to_intlist_to_bytelist. trivial.
    destruct (pad_len_64_nat (bitsToBytes l)). rewrite Zlength_correct, H. exists (Z.of_nat(x*16)). do 2 rewrite Nat2Z.inj_mul. rewrite Z.mul_comm, <- Z.mul_assoc. reflexivity.
  Qed.

  Lemma HASH m: SHA256.Hash m = intlist_to_bytelist (hashblocks ir (gap m)).
     unfold SHA256.Hash.
     rewrite functional_prog.SHA_256'_eq; reflexivity.
  Qed.

  Lemma FOLD_HB_eq: forall l ls, length l = (c + p)%nat ->
     Forall (fun x => length x = (c + p)%nat) ls ->
     fold_left h (l :: ls) (Vector.to_list iv_v) =
          hash_blocks_bits (HMAC_spec_concat.HMAC_Concat.b c p) B h
          (Vector.to_list iv_v) (l ++ concat ls).
  Proof. intros.
     assert (SH: sha_iv = Vector.to_list iv_v). rewrite <- iv_eq; trivial.
     rewrite <- SH; apply (fold_hash_blocks_eq _ _ H H0).
  Qed.

  Lemma length_splitandpad_inner m:
    Forall2
     (fun (bv : Vector.t bool b) (bl : list bool) => bl = Vector.to_list bv)
     (splitAndPad_v m) (splitandpad_blocks m).
  Proof. apply length_splitandpad_inner. Qed.

End EQ256.

Module EQ := HMAC_Equiv SHA256 EQ256.

(* Note we're comparing to HP.HMAC_SHA256.HmacCore, not HMAC. *)
Lemma Equivalence (P : Blist -> Prop) (HP: forall msg, P msg -> Nat.divide 8 (length msg))
      (kv : Bvector b) (m : HMAC_Abstract.Message P):
      Vector.to_list (HMAC_spec.HMAC EQ.h_v iv_v (HMAC_Abstract.wrappedSAP _ _ splitAndPad_v)
                      fpad_v EQ.opad_v EQ.ipad_v kv m) =
      bytesToBits (HMAC_SHA256.HmacCore EQ.ipd EQ.opd
                              (bitsToBytes (HMAC_Abstract.Message2Blist m))
                               (bitsToBytes (Vector.to_list kv))).
Proof.
  specialize (EQ.Equivalence _ HP kv m); intros.
  unfold EQ.h_v in H.
  unfold EQ256.c, EQ256.p, EQ256.splitAndPad_v in H.
  unfold EQ256.fpad_v in H.
  unfold EQ256.b in H. apply H.
Qed.

(* Earlier explicit proof:
Lemma Equivalence (P : Blist -> Prop) (HP: forall msg, P msg -> NPeano.divide 8 (length msg))
      (kv : Bvector b) (m : HMAC_Abstract.Message P):
      Vector.to_list (HMAC_spec.HMAC h_v iv_v (HMAC_Abstract.wrappedSAP _ _ splitAndPad_v)
                      fpad_v opad_v ipad_v kv m) =
      bytesToBits (HP.HMAC_SHA256.HmacCore (Integers.Byte.repr 54) (Integers.Byte.repr 92)
                              (bitsToBytes (HMAC_Abstract.Message2Blist m))
                              (map Integers.Byte.repr (bitsToBytes (Vector.to_list kv)))).
Proof.
  assert (LK : length (Vector.to_list kv) = b).
    { apply VectorToList_length. }
  erewrite <- HMAC_Abstract.HMAC_abstract_list; try reflexivity.
  2: apply h_eq.
  2: apply fpad_eq.
  2: apply length_splitandpad_inner.
  erewrite HMAC256_spec_list.HMAC_list_concat_sap_instantiated. (*; trivial.*)
SearchAbout sha_splitandpad_inc.
(*sap' to be instantiated to sha_splitandpad_inc*)
  2: apply sha_h_length.
  2: apply VectorToList_length.
  2: apply VectorToList_length.
  2: apply VectorToList_length.
  2: apply fold_hash_blocks_eq.
  2: apply LK.
(*  rewrite <- sha_splitandpad_inc_eq.*)
  rewrite <- HMAC256_spec_concat.HMAC_concat_pad_sap_instantiated; trivial.
  2: apply sha_h_length.
  2: apply VectorToList_length.
  2: apply VectorToList_length.
  eapply HMAC256_spec_pad.HMAC_pad_concrete'.

  split; lia.
  split; lia.

  (* key length *)
  { rewrite map_length, bitsToBytes_len_gen with (n:=64%nat).
    reflexivity.
    rewrite LK; reflexivity. }

  (* key length *)
  { rewrite Zlength_map, bitsToBytes_len. reflexivity. apply LK. }

  (* TODO: maybe replace bytes_bits_lists with bytesToBits? Since bytes_bits_comp_ind
     is used a lot *)

  (* key *)
  { rewrite map_unsigned_Brepr_isbyte.
      apply bytes_bits_comp_ind.
      eapply bitsToBytes_isbyteZ; reflexivity.
      rewrite  bits_bytes_bits_id; trivial.
      apply block_8. assumption.
      eapply bitsToBytes_isbyteZ. reflexivity. }

  (* uses fact that message is in blocks of 8 *)
  { apply bytes_bits_comp_ind.
    eapply bitsToBytes_isbyteZ; reflexivity.
    rewrite bits_bytes_bits_id; trivial.
    apply InBlocks_len.
    apply HP. destruct m. simpl; trivial. }

  (* opad *)
  { apply bytes_bits_comp_ind.
    apply Forall_repeat. unfold HP.Opad. lia.
    apply of_length_proof_irrel. }

  (* ipad *)
  { apply bytes_bits_comp_ind.
    apply Forall_repeat. unfold HP.Ipad. lia.
    apply of_length_proof_irrel. }

Qed.
End EQUIV. *)