Require Import Div2 Even.
Require Import ssreflect ssrbool eqtype.
Require Import ZArith_ext String_ext Lists_ext.
Require Import machine_int.
Import MachineInt.
Require Import C_types C_expr C_bipl C_cmd C_seplog.
Require Import POLAR_parse_client_hello.
Require Import rfc5246.
Import RFC5246.
Require Import POLAR_library_functions_triple.
Import PolarSSL.

Local Open Scope minC_hoare_scope.
Local Open Scope minC_assert_scope.
Local Open Scope minC_expr_scope.
Local Open Scope minC_cmd_scope.
Local Open Scope minC_types.
Local Open Scope machine_int_scope.
Local Open Scope zarith_ext_scope.
Local Open Scope lists_ext_scope.

Definition maj_ver := Zabs_nat (fixed_length S621.ContentType).

Definition min_ver := (maj_ver + Zabs_nat (fixed_length S44.uint8))%nat.

Definition record_sz := Zabs_nat (fixed_length S621.ContentType + fixed_length S621.ProtocolVersion).

Definition n' A := u2Z (nth record_sz A zero8) :: u2Z (nth (S record_sz) A zero8) :: nil.
Definition Zs2Z l := fold_left (fun x acc => x * 2 ^^ 8 + acc) l 0.
Definition n A := Zabs_nat (Zs2Z (n' A)).

Definition handshake_sz := Zabs_nat (S621.TLSPlainText_hd + fixed_length S621.ContentType).
Definition m A := Zabs_nat (u2Z ((nth handshake_sz A zero8 [.||]
                                  nth (S handshake_sz) A zero8) [.||]
                                  nth (S (S handshake_sz)) A zero8)).

Definition req_maj := Zabs_nat (S621.TLSPlainText_hd + S74.Handshake_hd).

Definition min_req := (req_maj + Zabs_nat (fixed_length S44.uint8))%nat.

Definition rand := Zabs_nat (S621.TLSPlainText_hd + S74.Handshake_hd +
  fixed_length S621.ProtocolVersion).

Definition sid := (rand + Zabs_nat (fixed_length S7412.Random))%nat.

Definition sess_len A := Zabs_nat (u2Z (nth sid A zero8)).

Definition csuites := Zabs_nat (S621.TLSPlainText_hd + S74.Handshake_hd
  + fixed_length S621.ProtocolVersion + fixed_length S7412.Random + fixed_length S7412.SessionID).

Definition ciph_len A := Zabs_nat (u2Z (nth (csuites + sess_len A) A zero8 [.||]
                                      nth (S csuites + sess_len A) A zero8)).

Definition compmeth := (csuites + Zabs_nat (fixed_length S7412.CipherSuite))%nat.

Definition comp_len A := Zabs_nat (u2Z (nth (compmeth + sess_len A + ciph_len A) A zero8)).

Lemma cover_ssl_context : forall s,
  s |g- "ssl_context" -| ssl_ctxt ->
  s |g- "ssl_session" -| ssl_sess ->
  cover (_ctxt s) (ptyp ssl_context).

Local Open Scope string_scope.

Lemma error_return :
{{ fun s h => (s |t- "ret" -| btyp sint32) }} "ret" <- POLARSSL_ERR_SSL_BAD_HS_CLIENT_HELLO; ret {{ fun s h => [var_e "ret" ]_ s <> Some int32_0 }}.
Proof.

apply hoare_assign with (btyp sint32) (fun s h =>
  [var_e "ret"%string ]_ s <> Some int32_0).
rewrite /wp_assign => s h H.
eexists; split; first by rewrite /=; reflexivity.
split; first by OEqtm.
split; first by OEqtm.
Store_upd.
case; by apply Z2s_dis.

by apply while.hoare_hoare0, hoare0_skip.
Qed.

Lemma POLAR_parse_client_hello_triple : forall (SI BU RB ID : list (int 8))
  (CI : list (int 32)) (len_BU : Z_of_nat (List.length BU) = SSL_BUFFER_LEN)
  (len_RB : List.length RB = 64%nat) (len_ID : List.length ID = 32%nat)
  (majv0 minv0 mmaj0 mmin0 cipher0 length0 : int 32)
  (a rb ses id ciphers vssl : int ptr_len),
  u2Z vssl +
   Z_of_nat (sizeof (styp (mkStag "ssl_context") ssl_ctxt)) <
   2 ^^ ptr_len ->
  {{ fun s h => wf_tstore (_tstore s) /\
    s |g- "ssl_context" -| ssl_ctxt /\ s |g- "ssl_session" -| ssl_sess /\
    s |t- "_buf0_" -| btyp uchar /\ s |t- "_buf1_" -| btyp uchar /\
    s |t- "_buf3_" -| btyp uchar /\ s |t- "_buf4_" -| btyp uchar /\
    s |t- "buf" -| ptyp (btyp uchar) /\ s |t- "ret" -| btyp sint32 /\
    s |t- "ssl" -| ptyp ssl_context /\ s |t- "n" -| btyp sint32 /\
    s |v- "ssl" -| pval vssl /\
    ((cst_pe wf_uchar a |%c%> map cst8 BU) ** (cst_pe wf_uchar rb |%c%> map cst8 RB) **
     (cst_pe wf_uchar id |%c%> map cst8 ID) **
     (cst_pe wf_ssl_session ses |~ ssl_session ~>
       (bval32 cipher0 :: bval32 length0 :: pval id :: nil) CST_SE wf_ssl_session) **
     (cst_pe wf_uint32 ciphers |% btyp uint32 %> map cst32 CI) ** TT **
     (var_e "ssl" |~ ssl_context ~> (bval32 (Z2u 32 S74.client_hello) ::
       bval32 majv0 :: bval32 minv0 :: bval32 mmaj0 :: bval32 mmin0 ::
       pval ses ::
       pval (a [.+] Z2u ptr_len 8) :: pval (a [.+] Z2u ptr_len 13) ::
       bval32 zero32 :: pval ciphers :: pval rb :: nil)
      CST_SE wf_ssl_context)) s h }}
  ssl_parse_client_hello
  {{ fun s h => (exists i,
    [ var_e "ret" ]_ s = Some int32_0 /\
    (BU |[8, Zabs_nat (S621.TLSPlainText_hd) + n SI)) =
    (SI |[0, Zabs_nat (S621.TLSPlainText_hd) + n SI)) /\
    u2Z (nth O SI zero8) = S621.handshake /\
    u2Z (nth (Zabs_nat (S74.Handshake_hd + 1)) SI zero8) = S74.client_hello /\
    u2Z (nth maj_ver SI zero8) = S621.SSLv30_maj /\
    u2Z (nth req_maj SI zero8) = S621.SSLv30_maj /\
    In (u2Z (nth min_ver SI zero8)) (S621.SSLv30_min :: S621.TLSv10_min :: nil) /\
    In (u2Z (nth min_req SI zero8)) (S621.SSLv30_min :: S621.TLSv10_min :: nil) /\
    (S621.length_maxp (n' SI))%nat /\
    
    (Zabs_nat (S74.Handshake_hd) + m SI <= n SI)%nat /\
    (Z_of_nat (sess_len SI) <= tls_max S7412.SessionID) /\
    
    tls_min S7412.cipher_suites_type <= Z_of_nat (ciph_len SI) <= tls_max S7412.cipher_suites_type /\
    even (ciph_len SI) /\
    (i < div2 (ciph_len SI))%nat /\
    (exists k, zext 16 (nth (compmeth + sess_len SI + 2 * i) SI zero8 [.||]
                        nth (compmeth + sess_len SI + 2 * i + 1) SI zero8) =
               nth k CI zero32) /\
    
    (tls_min S7412.compression_methods_type <= Z_of_nat (comp_len SI) <=
      tls_max S7412.compression_methods_type) /\
    
    In (Z2u 8 S61.null) (SI |[ compmeth + 1 + sess_len SI + ciph_len SI, comp_len SI) ) /\
    
    ~~ (S7412.client_extensions_present (m SI) (sess_len SI) (ciph_len SI) (comp_len SI)) /\
    ((cst_pe wf_uchar rb |%c%>
        map cst8 (SI |[ rand, Zabs_nat (tls_max S7412.Random)))++
        map cst8 (skipn (Zabs_nat (tls_max S7412.Random)) RB)) **
     (cst_pe wf_uchar id |%c%> map cst8 (SI |[ sid, sess_len SI) ) ) **
     (cst_pe wf_ssl_session ses |~ ssl_session ~>
       (bval32 (zext 16 ((nth (compmeth + sess_len SI + 2 * i) SI zero8) [.||]
                          nth (compmeth + sess_len SI + 2 * i + 1) SI zero8)) ::
        bval32 (Z2u 32 (Z_of_nat (sess_len SI))) ::
        pval id :: nil) CST_SE wf_ssl_session) ** TT **
      (var_e "ssl" |~ ssl_context ~>
        (bval32 (Z2u 32 S74.server_hello) ::
         bval32 (zext 24 (nth maj_ver SI zero8)) ::
         bval32 (zext 24 (nth min_ver SI zero8)) ::
         bval32 (zext 24 (nth req_maj SI zero8)) ::
         bval32 (zext 24 (nth min_req SI zero8)) ::
         pval ses ::
         pval (a [.+] Z2u ptr_len 8) :: pval (a [.+] Z2u ptr_len 13) ::
         bval32 (Z2u 32 (S621.TLSPlainText_hd + Z_of_nat (n SI))) ::
         pval ciphers :: pval rb :: nil) CST_SE wf_ssl_context)) s h )
    \/
    [ var_e "ret"]_ s <> Some int32_0
 }}.
Proof.
move=> SI BU RB ID CI len_BU len_RB len_ID
  majv0 minv0 mmaj0 mmin0 cipher0 length0
  a rb ses id ciphers vssl vssl_fit .

rewrite /ssl_parse_client_hello.

apply while.hoare_seq with (fun s h => exists in_left : int 32,
    (wf_tstore (_tstore s) /\
     s |g- "ssl_context" -| ssl_ctxt /\ s |g- "ssl_session" -| ssl_sess /\
     s |t- "_buf0_" -| btyp uchar /\ s |t- "_buf1_" -| btyp uchar /\
     s |t- "_buf3_" -| btyp uchar /\ s |t- "_buf4_" -| btyp uchar /\
     s |t- "buf" -| ptyp (btyp uchar) /\ s |t- "ret" -| btyp sint32 /\
     s |t- "ssl" -| ptyp ssl_context /\ s |t- "n" -| btyp sint32 /\
     s |v- "ssl" -| pval vssl /\
    ((cst_pe wf_uchar a |%c%> map cst8 BU) **
     (cst_pe wf_uchar rb |%c%> map cst8 RB) **
     (cst_pe wf_uchar id |%c%> map cst8 ID) **
     (cst_pe wf_ssl_session ses |~ ssl_session ~>
       (bval32 cipher0 :: bval32 length0 :: pval id :: nil)
       CST_SE wf_ssl_session) **
     (cst_pe wf_uint32 ciphers |% btyp uint32 %> map cst32 CI) ** TT **
     (var_e "ssl"%string |~ ssl_context ~>
       bval32 (Z2u 32 S74.client_hello)
       :: bval32 majv0 :: bval32 minv0 :: bval32 mmaj0 :: bval32 mmin0
       :: pval ses
       :: pval (a[.+]Z2u ptr_len 8) :: pval (a[.+]Z2u ptr_len 13)
       :: bval32 in_left
       :: pval ciphers :: pval rb :: nil CST_SE wf_ssl_context)) s h) /\
    ([var_e "ret"%string ]_ s = Some int32_0 /\
      (List.length SI >= 5)%nat /\
      (BU |[ 8 + 0, 5 )) = (SI |[ 0, 5 )) /\
      in_left = Z2u 32 (Z_of_nat 0) [.+] Z2u 32 (Z_of_nat 5)
      \/
      [var_e "ret"%string ]_ s <> Some int32_0 /\
      (List.length SI < 0 + 5)%nat)).

  eapply minc_hoare_prop_m.hoare_stren; last by apply ssl_fetch_input_triple.
  move=> s h /= H; by intuition.

set code := while.ifte _ _ _.
apply while.hoare_ifte.

apply minc_hoare_prop_m.hoare_stren with
  (fun s h => [var_e "ret"%string ]_ s <> Some int32_0).
  move=> s h.
  case=> precond /= Htest Hret.
  rewrite Hret /= in Htest.
  case: ifP Htest => //.
  case: ifP.
  + by rewrite u2Z_Z2u.
  + move/Zeq_boolP; tauto.
apply minc_hoare_prop_m.hoare_weak with
  (fun s h => [var_e "ret"%string ]_ s <> Some int32_0).
  move=> s h; by intuition.
  rewrite /PolarSSL.ret.
  by apply while.hoare_hoare0, hoare0_skip.

move=> {code}.

apply minc_hoare_prop_m.hoare_stren with
  (fun s h => (wf_tstore (_tstore s) /\
      s |g- "ssl_context" -| ssl_ctxt /\ s |g- "ssl_session" -| ssl_sess /\
      s |t- "_buf0_" -| btyp uchar /\ s |t- "_buf1_" -| btyp uchar /\
      s |t- "_buf3_" -| btyp uchar /\ s |t- "_buf4_" -| btyp uchar /\
      s |t- "buf" -| ptyp (btyp uchar) /\ s |t- "ret" -| btyp sint32 /\
      s |t- "ssl" -| ptyp ssl_context /\ s |t- "n" -| btyp sint32 /\
      s |v- "ssl" -| pval vssl /\
      (((((((cst_pe wf_uchar a |%c%> map cst8 BU) **
        cst_pe wf_uchar rb |%c%> map cst8 RB) **
        cst_pe wf_uchar id |%c%> map cst8 ID) **
        cst_pe wf_ssl_session ses |~ ssl_session ~>
        bval32 cipher0 :: bval32 length0 :: pval id :: nil
        CST_SE wf_ssl_session) **
        cst_pe wf_uint32 ciphers |% btyp uint32 %> map cst32 CI) ** TT) **
        var_e "ssl" |~ ssl_context ~>
        bval32 (Z2u 32 S74.client_hello) ::
        bval32 majv0 :: bval32 minv0 :: bval32 mmaj0 :: bval32 mmin0 ::
        pval ses ::
        pval (a [.+] Z2u ptr_len 8):: pval (a [.+] Z2u ptr_len 13) ::
        bval32 (Z2u 32 5) ::
        pval ciphers :: pval rb :: nil CST_SE wf_ssl_context) s h) /\
    ((length SI >= 5)%nat /\ BU |[8, 5) = (BU |[8, 0)) ++ (SI |[0, 5)))%list).
  move=> s h.
  case=> [[in_left [H1 [[Hret H2] | [Hret H2]]]]] Htest.
  - case: H2 => [Hlen [Happ in_leftE]].
    rewrite /= add_com add_0 in in_leftE.
    by rewrite in_leftE in H1.
  - case: H1 => wf_store_s.
    do 7 case=> _; case=> t_ret.
    rewrite /cst32_0 in Htest.
    move/(neg_exp2bexp _ wf_store_s _ _ sint32 t_ret): Htest.
    by move/(exp2bexp_neq _ wf_store_s _ _ t_ret).

apply hoare_lookup_back'' with (ptyp (btyp uchar))
 (fun s h => (wf_tstore (_tstore s) /\
  s |g- "ssl_context" -| ssl_ctxt /\ s |g- "ssl_session" -| ssl_sess /\
  s |t- "_buf0_" -| btyp uchar /\ s |t- "_buf1_" -| btyp uchar /\
  s |t- "_buf3_" -| btyp uchar /\ s |t- "_buf4_" -| btyp uchar /\
  s |t- "buf" -| ptyp (btyp uchar) /\ s |t- "ret" -| btyp sint32 /\
  s |t- "ssl" -| ptyp ssl_context /\ s |t- "n" -| btyp sint32 /\
  s |v- "ssl" -| pval vssl /\
  (((((((cst_pe wf_uchar a |%c%> map cst8 BU) **
    cst_pe wf_uchar rb |%c%> map cst8 RB) **
    cst_pe wf_uchar id |%c%> map cst8 ID) **
    cst_pe wf_ssl_session ses |~ ssl_session ~>
         bval32 cipher0 :: bval32 length0 :: pval id :: nil
         CST_SE wf_ssl_session) **
        cst_pe wf_uint32 ciphers |% btyp uint32 %> map cst32 CI) ** TT) **
      var_e "ssl" |~ ssl_context ~>
      bval32 (Z2u 32 S74.client_hello) ::
      bval32 majv0 :: bval32 minv0 :: bval32 mmaj0 :: bval32 mmin0 ::
      pval ses ::
      pval (a [.+] Z2u ptr_len 8) :: pval (a [.+] Z2u ptr_len 13) ::
      bval32 (Z2u 32 5) ::
      pval ciphers :: pval rb :: nil CST_SE wf_ssl_context) s h) /\
 ([ var_e "buf"]_s = Some (pval (a [.+] Z2u ptr_len 8))) /\
 ((length SI >= 5)%nat /\ BU |[8, 5) = (BU |[8, 0)) ++ (SI |[0, 5)))%list).

move=> s h.
case=> Hwfmem H.
Ltac case_Hwfmem H := case: H => [wf_store_s [Hssl_context [Hssl_session [t_buf0 [t_buf1 [t_buf3 [t_buf4 [t_buf [t_ret [t_ssl [t_n [s_ssl Hmem]]]]]]]]]]]].
case_Hwfmem Hwfmem.

repeat (split => //).
by OEqtm.
by OEqtm.

exists (vssl [.+] Z2u ptr_len ((Z_of_nat ptr_size) + 20)); split.
  rewrite /= /typof /= t_ssl /= /tstore_get s_ssl /deref /Lists_ext.ifind.
  rewrite [Lists_ext.ifind' _ _ _ _]/= {1}[Z_of_nat]lock /= -lock plus_0_r sizeof_ptyp.
  do 4 f_equal.
  by rewrite (_ : 20 = Z_of_nat 20) // -inj_plus plus_comm.
exists (cst_pe wf_uchar (a [.+] Z2u ptr_len 8)).
apply strictly_exact_prop; first by apply strictly_exact_mapsto.
rewrite /wp_assign.
repeat (split => //).
- eexists; split; first by reflexivity.
  repeat Store_upd.
  split; first by OEqtm.
  split; first by OEqtm.
  split.
    split; first by Store_upd.
    repeat (split; first by done).
    repeat (split; first by Store_upd).
    move: Hmem; apply monotony => h' //.
    + apply monotony => h2 //.
      apply monotony => h3 //; last first.
        apply mapstos_ext_cst32 => //; repeat Store_upd; by OEqtm.
      apply monotony => h4 //.
      apply monotony => h5 //; last first.
        apply mapstos_ext_cst8 => //; repeat Store_upd; by OEqtm.
      apply monotony => h6 //; last first.
        apply mapstos_ext_cst8 => //; repeat Store_upd; by OEqtm.
      apply mapstos_ext_cst8 => //; repeat Store_upd; by OEqtm.
    + apply mapsto_ext => //; repeat Store_upd.
      * OEqtm. by apply cover_ssl_context.
      * OEqtm. by apply cover_ssl_context.
      * reflexivity.
  split; by [Store_upd | done].
- case: Hmem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
  apply con_TT_inv.
  rewrite h1_U_h2 hp.union_com //.
  apply con_cons; [by apply hp.disj_sym | idtac | done].
  set lst := _ :: _ in Hh2.
  have Hlen : List.length ssl_ctxt = List.length lst by done.
  apply (mapsto_styp_inv _ (mkStag "ssl_context") ssl_ctxt lst _ _ vssl
    Hssl_context wf_ssl_context Hlen wf_uchar Hh2 s_ssl vssl_fit 6%nat _ _
    (ptyp (btyp uchar)) (pval (a [.+] Z2u ptr_len 8))).
  by rewrite /ifind /=.
  rewrite /=; reflexivity.
  rewrite /=; reflexivity.   by Eqtm.
  rewrite /=. do 2 f_equal. by apply ProofIrrelevance.proof_irrelevance.

case hd_SI : SI => [| msg_type SI'].
apply minc_hoare_prop_m.hoare_stren with FF; last by exact: hoare_false.
  move=> s h /=.
  case=> _; case=> _; case=> H.
  exfalso; omega.
rewrite -hd_SI.
apply hoare_lookup_back'' with (btyp uchar) (fun s h =>
 (wf_tstore (_tstore s) /\
  s |g- "ssl_context" -| ssl_ctxt /\ s |g- "ssl_session" -| ssl_sess /\
  s |t- "_buf0_" -| btyp uchar /\ s |t- "_buf1_" -| btyp uchar /\
  s |t- "_buf3_" -| btyp uchar /\ s |t- "_buf4_" -| btyp uchar /\
  s |t- "buf" -| ptyp (btyp uchar) /\ s |t- "ret" -| btyp sint32 /\
  s |t- "ssl" -| ptyp ssl_context /\ s |t- "n" -| btyp sint32 /\
  s |v- "ssl" -| pval vssl /\
  (((((((cst_pe wf_uchar a |%c%> map cst8 BU) **
    cst_pe wf_uchar rb |%c%> map cst8 RB) **
    cst_pe wf_uchar id |%c%> map cst8 ID) **
    cst_pe wf_ssl_session ses |~ ssl_session ~>
         bval32 cipher0 :: bval32 length0 :: pval id :: nil
         CST_SE wf_ssl_session) **
        cst_pe wf_uint32 ciphers |% btyp uint32 %> map cst32 CI) ** TT) **
      var_e "ssl" |~ ssl_context ~>
      bval32 (Z2u 32 S74.client_hello) ::
      bval32 majv0 :: bval32 minv0 :: bval32 mmaj0 :: bval32 mmin0 ::
      pval ses ::
      pval (a [.+] Z2u ptr_len 8) :: pval (a [.+] Z2u ptr_len 13) ::
      bval32 (Z2u 32 5) :: pval ciphers :: pval rb :: nil
      CST_SE wf_ssl_context) s h) /\
 ([ var_e "buf"]_s = Some (pval (a [.+] Z2u ptr_len 8)) /\
  [ var_e "_buf0_"]_s = Some (bval8 msg_type) /\
 ((length SI >= 5)%nat /\
  BU |[8, 5) = (BU |[8, 0)) ++ msg_type :: (SI |[1, 4)))%list)).

move=> s h.
case=> [Hwfmem [Hbuf [len_SI BU_SI]]].
case_Hwfmem Hwfmem.
repeat (split => //).
- by OEqtm.
- by OEqtm.
- exists (a [.+] Z2u _ 8); split; first by done.
  exists (cst8 msg_type).
  apply strictly_exact_prop; first by apply strictly_exact_mapsto.
  rewrite /wp_assign.
  repeat (split => //).

eexists; split; first by reflexivity.
split; first by OEqtm.
split; first by OEqtm.
split.
  split; first by Store_upd.
  repeat (split; first by done).
  repeat (split; first by Store_upd).
  move: Hmem; apply monotony => h' //.
  - apply monotony => h2 //.
    apply monotony => h3 //; last first.
      apply mapstos_ext_cst32 => //; repeat Store_upd; by OEqtm.
    apply monotony => h4 //.
    apply monotony => h5 //; last first.
      apply mapstos_ext_cst8 => //; repeat Store_upd; by OEqtm.
    apply monotony => h6 //.
      apply mapstos_ext_cst8 => //; repeat Store_upd; by OEqtm.
    apply mapstos_ext_cst8 => //; repeat Store_upd; by OEqtm.
  - apply mapsto_ext => //; repeat Store_upd.
    + OEqtm. by apply cover_ssl_context.
    + OEqtm. by apply cover_ssl_context.
    + reflexivity.
repeat (split; first by Store_upd).
split; first by assumption.
by rewrite BU_SI hd_SI.

do 6 apply/con_TT_inv.
move: Hmem.
do 6 apply monotony => // {h} h.
rewrite /slice in BU_SI.
rewrite -(firstn_skipn 8 BU).
move=> Hmem.
set BU' := skipn 8 BU in BU_SI Hmem.
apply mapstos_app_sepcon_cst8 in Hmem => //; last 2 first.
  rewrite (len_firstn (Zabs_nat SSL_BUFFER_LEN)) // -len_BU Zabs_nat_Z_of_nat //.
  apply Z_of_nat_le_inj; by rewrite len_BU.
  by OEqtm.
apply con_TT_inv.
apply/con_com.
apply: monotony Hmem => // {h} h.
rewrite -(firstn_skipn 5 BU') => Hmem.
apply mapstos_app_sepcon_cst8 in Hmem => //; last 2 first.
  rewrite (len_firstn (Zabs_nat (SSL_BUFFER_LEN - 8))) // /BU'; last first.
    rewrite /SSL_BUFFER_LEN.
    vm_compute.
    do 5 apply le_n_S.
    by apply le_O_n.
  rewrite len_skipn -len_BU Zabs_nat_Zminus.
  by rewrite Zabs_nat_Z_of_nat.
  split; [done | by rewrite len_BU].
  by OEqtm.
apply con_TT_inv.
apply: monotony Hmem => // {h} h Hmem.
rewrite BU_SI hd_SI firstn_length inj_min len_BU /SSL_BUFFER_LEN /Zmin /= in Hmem.
apply: monotony Hmem => // {h} h Hmem.
apply: mapsto_ext Hmem => //.
- by OEqtm.
- by OEqtm.
- by rewrite Hbuf /= /sizeof /= s2Z_Z2s.

apply while.hoare_ifte.

eapply while.hoare_conseq; last by apply error_return.
rewrite /while.entails => s h H; by right.
rewrite /while.entails => s h H; tauto.

apply while.hoare_ifte.

eapply while.hoare_conseq; last by apply error_return.
rewrite /while.entails => s h H; by right.
rewrite /while.entails => s h H; tauto.

case Hmaj_ver : SI' => [| maj_ver SI''].
apply minc_hoare_prop_m.hoare_stren with FF; last by exact: hoare_false.
  subst SI' SI => s h /= H.
  exfalso; omega.

apply hoare_lookup_back'' with (btyp uchar) (fun s h =>
  (((wf_tstore (_tstore s) /\
    s |g- "ssl_context" -| ssl_ctxt /\ s |g- "ssl_session" -| ssl_sess /\
    s |t- "_buf0_" -| btyp uchar /\ s |t- "_buf1_" -| btyp uchar /\
    s |t- "_buf3_" -| btyp uchar /\ s |t- "_buf4_" -| btyp uchar /\
    s |t- "buf" -| ptyp (btyp uchar) /\ s |t- "ret" -| btyp sint32 /\
    s |t- "ssl" -| ptyp ssl_context /\ s |t- "n" -| btyp sint32 /\
    s |v- "ssl" -| pval vssl /\
    ((((((cst_pe wf_uchar a |%c%> map cst8 BU **
          cst_pe wf_uchar rb |%c%> map cst8 RB) **
          cst_pe wf_uchar id |%c%> map cst8 ID) **
          cst_pe wf_ssl_session ses |~ ssl_session ~>
            bval32 cipher0 :: bval32 length0 :: pval id :: nil
            CST_SE wf_ssl_session) **
          cst_pe wf_uint32 ciphers |% btyp uint32 %> map cst32 CI) ** TT) **
          var_e "ssl" |~ ssl_context ~> bval32 (Z2u 32 S74.client_hello) ::
            bval32 majv0 :: bval32 minv0 :: bval32 mmaj0 :: bval32 mmin0 ::
            pval ses ::
            pval (a[.+]Z2u ptr_len 8) :: pval (a[.+]Z2u ptr_len 13) ::
            bval32 (Z2u 32 5) :: pval ciphers :: pval rb :: nil
            CST_SE wf_ssl_context) s h) /\
  [var_e "buf" ]_ s = Some (pval (a[.+]Z2u ptr_len 8)) /\
  [var_e "_buf0_" ]_ s = Some (bval8 msg_type) /\
  [var_e "_buf1_" ]_ s = Some (bval8 maj_ver) /\
  (List.length SI >= 5)%nat /\
  (BU |[ 8, 5)) = ((BU |[ 8, 0)) ++ msg_type :: maj_ver :: (SI |[2, 3)))%list /\
  u2Z msg_type = S621.handshake))).

move=> s h H.
case: H => [[H test1_buf0] test2_buf0].
case: H => [H [Hbuf [Hbuf0 [HSI BU_SI]]]].
case_Hwfmem H.
split; first by tauto.
split; first by OEqtm.
split; first by OEqtm.
exists (a [.+] Z2u ptr_len 9); split.
  rewrite /= in Hbuf.
  rewrite /= Hbuf /typof /=.
  typ_var.
  by rewrite /scalez s2Z_Z2s //= add_assoc add_Z2u.
exists (cst8 maj_ver).
apply strictly_exact_prop; first by apply strictly_exact_mapsto.
rewrite /wp_assign.
repeat (split => //).
- eexists; split; first by reflexivity.
  repeat Store_upd.
  split; first by OEqtm.
  split; first by OEqtm.
  split.
    split; first by Store_upd.
    repeat (split; first by done).
    repeat (split; first by Store_upd).
    move: Hmem; apply monotony => // h1.
    - apply monotony => // h2.
      apply monotony => // h3; last first.
        apply mapstos_ext_cst32 => //; repeat Store_upd; by OEqtm.
      apply monotony => // h4.
      apply monotony => // h5; last first.
        apply mapstos_ext_cst8 => //; repeat Store_upd; by OEqtm.
      apply monotony => // h6; last first.
        apply mapstos_ext_cst8 => //; repeat Store_upd; by OEqtm.
      apply mapstos_ext_cst8 => //; repeat Store_upd; by OEqtm.
    - apply mapsto_ext => //; repeat Store_upd.
      OEqtm. by apply cover_ssl_context.
      OEqtm. by apply cover_ssl_context.
      reflexivity.
  repeat (split; first by done).
  split.
    by rewrite /= BU_SI /= hd_SI Hmaj_ver.
  rewrite /= in Hbuf0.
  rewrite /= Hbuf0 in test2_buf0.
  case: ifP test2_buf0; last by done.
  case: ifP; last by move=> _; rewrite u2Z_Z2u.
  move/Zeq_boolP => ->; by rewrite u2Z_Z2s_pos.
-
  rewrite (skipn_nth_firstn (Z2u 8 0) 9 BU) in Hmem; last first.
    apply Z_of_nat_le_inj; by rewrite len_BU.
  rewrite !con_assoc_equiv in Hmem.
  case: Hmem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
  apply mapstos_app_sepcon_cst8 in Hh1; last 3 first.
    rewrite (len_firstn (Zabs_nat SSL_BUFFER_LEN)) // -len_BU Zabs_nat_Z_of_nat //.
    apply Z_of_nat_le_inj; by rewrite len_BU.
    exact wf_store_s.
    by OEqtm.
  rewrite con_com_equiv map_cons con_assoc_equiv in Hh1.
  apply con_TT_inv.
  exists h1, h2; repeat (split => //).
  move: Hh1; apply monotony => // h'.
  apply mapsto_ext.
  by OEqtm.
  by OEqtm.
  rewrite /= in Hbuf.
  rewrite [in X in _ = X]/= Hbuf.
  rewrite /typof [typ_of _ _ _]/=.
  typ_var.
  rewrite sizeof_btyp s2Z_Z2s // (len_firstn (Zabs_nat SSL_BUFFER_LEN)); last first.
    apply Z_of_nat_le_inj; by rewrite Z_of_nat_Zabs_nat.
    by rewrite -len_BU Zabs_nat_Z_of_nat.
  rewrite /= sizeof_btyp s2Z_Z2s //.
  f_equal.
  f_equal.
  rewrite /scalez /= add_assoc.
  by rewrite add_Z2u.
  rewrite /= in BU_SI.
  rewrite hd_SI Hmaj_ver /= in BU_SI.
  rewrite /slice in BU_SI.
  rewrite (nth_firstn_skipn (Z2u 8 0)) in BU_SI; last first.
    apply Z_of_nat_lt_inj; by rewrite len_BU.
  rewrite (nth_firstn_skipn (Z2u 8 0)) in BU_SI; last first.
    apply Z_of_nat_lt_inj; by rewrite len_BU.
  by case: BU_SI => _ -> _.

apply while.hoare_ifte.

eapply while.hoare_conseq; last by apply error_return.
rewrite /while.entails => s h H; by right.
rewrite /while.entails => s h H; tauto.

case Hmin_ver : SI'' => [| min_ver SI'''].
apply minc_hoare_prop_m.hoare_stren with FF; last by exact: hoare_false.
  subst SI'' SI' SI => s h /= H.
  exfalso; omega.
case Hm_low : SI''' => [| m_low SI4].
apply minc_hoare_prop_m.hoare_stren with FF; last by exact: hoare_false.
  subst SI''' SI'' SI' SI => s h /= H.
  exfalso; omega.

apply hoare_lookup_back'' with (btyp uchar) (fun s h =>
  (((wf_tstore (_tstore s) /\
    s |g- "ssl_context" -| ssl_ctxt /\ s |g- "ssl_session" -| ssl_sess /\
    s |t- "_buf0_" -| btyp uchar /\ s |t- "_buf1_" -| btyp uchar /\
    s |t- "_buf3_" -| btyp uchar /\ s |t- "_buf4_" -| btyp uchar /\
    s |t- "buf" -| ptyp (btyp uchar) /\ s |t- "ret" -| btyp sint32 /\
    s |t- "ssl" -| ptyp ssl_context /\ s |t- "n" -| btyp sint32 /\
    s |v- "ssl" -| pval vssl /\
    ((((((cst_pe wf_uchar a |%c%> map cst8 BU **
          cst_pe wf_uchar rb |%c%> map cst8 RB) **
          cst_pe wf_uchar id |%c%> map cst8 ID) **
          cst_pe wf_ssl_session ses |~ ssl_session ~>
            bval32 cipher0 :: bval32 length0 :: pval id :: nil
            CST_SE wf_ssl_session) **
          cst_pe wf_uint32 ciphers |% btyp uint32 %> map cst32 CI) ** TT) **
          var_e "ssl" |~ ssl_context ~> bval32 (Z2u 32 S74.client_hello) ::
            bval32 majv0 :: bval32 minv0 :: bval32 mmaj0 :: bval32 mmin0 ::
            pval ses ::
            pval (a[.+]Z2u ptr_len 8) :: pval (a[.+]Z2u ptr_len 13) ::
            bval32 (Z2u 32 5) :: pval ciphers :: pval rb :: nil
            CST_SE wf_ssl_context) s h) /\
  [var_e "buf" ]_ s = Some (pval (a[.+]Z2u ptr_len 8)) /\
  [var_e "_buf0_" ]_ s = Some (bval8 msg_type) /\
  [var_e "_buf1_" ]_ s = Some (bval8 maj_ver) /\
  [var_e "_buf3_" ]_ s = Some (bval8 m_low) /\
  (List.length SI >= 5)%nat /\
  (BU |[ 8, 5)) = ((BU |[ 8, 0)) ++ msg_type :: maj_ver :: min_ver :: m_low :: (SI |[4, 1)))%list /\
  u2Z msg_type = S621.handshake))).

move=> s h H.
case: H => [H test_buf1].
case: H => [H [Hbuf [Hbuf0 [Hbuf1 [HSI [BU_SI msg_typ_handshake]]]]]].
case_Hwfmem H.
split; first by assumption.
split; first by OEqtm.
split; first by OEqtm.
exists (a [.+] Z2u ptr_len 11); split.
  rewrite /= in Hbuf.
  rewrite /= Hbuf /typof /=.
  typ_var.
  by rewrite /scalez s2Z_Z2s //= add_assoc add_Z2u.
exists (cst8 m_low).
apply strictly_exact_prop; first by apply strictly_exact_mapsto.
rewrite /wp_assign.
repeat (split => //).
- eexists; split; first by reflexivity.
  repeat Store_upd.
  split; first by OEqtm.
  split; first by OEqtm.
  split.
    split; first by Store_upd.
    repeat (split; first by done).
    repeat (split; first by Store_upd).
    move: Hmem; apply monotony => // h1.
    - apply monotony => // h2.
      apply monotony => // h3; last first.
        apply mapstos_ext_cst32 => //; repeat Store_upd; by OEqtm.
      apply monotony => // h4.
      apply monotony => // h5; last first.
        apply mapstos_ext_cst8 => //; repeat Store_upd; by OEqtm.
      apply monotony => // h6; last first.
        apply mapstos_ext_cst8 => //; repeat Store_upd; by OEqtm.
      apply mapstos_ext_cst8 => //; repeat Store_upd; by OEqtm.
    - apply mapsto_ext => //; repeat Store_upd.
      OEqtm. by apply cover_ssl_context.
      OEqtm. by apply cover_ssl_context.
      reflexivity.
  repeat (split; first by done).
  split; last by done.
  by rewrite BU_SI hd_SI Hmaj_ver Hmin_ver Hm_low.
-
  rewrite (skipn_nth_firstn (Z2u 8 0) 11 BU) in Hmem; last first.
    apply Z_of_nat_le_inj; by rewrite len_BU.
  rewrite !con_assoc_equiv in Hmem.
  case: Hmem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
  apply mapstos_app_sepcon_cst8 in Hh1; last 3 first.
    rewrite (len_firstn (Zabs_nat SSL_BUFFER_LEN)) // -len_BU Zabs_nat_Z_of_nat //.
    apply Z_of_nat_le_inj; by rewrite len_BU.
    exact wf_store_s.
    by OEqtm.
  rewrite con_com_equiv map_cons con_assoc_equiv in Hh1.
  apply con_TT_inv.
  exists h1, h2; repeat (split => //).
  move: Hh1; apply monotony => // h'.
  apply mapsto_ext.
  by OEqtm.
  by OEqtm.
  rewrite /= in Hbuf.
  rewrite [in X in _ = X]/= Hbuf.
  rewrite /typof [typ_of _ _ _]/=.
  typ_var.
  rewrite sizeof_btyp s2Z_Z2s // (len_firstn (Zabs_nat SSL_BUFFER_LEN)); last first.
    apply Z_of_nat_le_inj; by rewrite Z_of_nat_Zabs_nat.
    by rewrite -len_BU Zabs_nat_Z_of_nat.
  rewrite /= sizeof_btyp s2Z_Z2s //.
  f_equal.
  f_equal.
  rewrite /scalez /= add_assoc.
  by rewrite add_Z2u.
  rewrite /= in BU_SI.
  rewrite hd_SI Hmaj_ver /= Hmin_ver Hm_low in BU_SI.
  rewrite /slice in BU_SI.

  rewrite (nth_firstn_skipn (Z2u 8 0)) in BU_SI; last first.
    apply Z_of_nat_lt_inj; by rewrite len_BU.
  rewrite (nth_firstn_skipn (Z2u 8 0)) in BU_SI; last first.
    apply Z_of_nat_lt_inj; by rewrite len_BU.
  rewrite (nth_firstn_skipn (Z2u 8 0)) in BU_SI; last first.
    apply Z_of_nat_lt_inj; by rewrite len_BU.
  rewrite (nth_firstn_skipn (Z2u 8 0)) in BU_SI; last first.
    apply Z_of_nat_lt_inj; by rewrite len_BU.
  by case: BU_SI => _ _ _ -> _.

case Hm_hi : SI4 => [| m_hi SI5].
apply minc_hoare_prop_m.hoare_stren with FF; last by exact: hoare_false.
  subst SI4 SI''' SI'' SI' SI => s h /= H.
  exfalso; omega.

apply hoare_lookup_back'' with (btyp uchar) (fun s h =>
  (wf_tstore (_tstore s) /\
    s |g- "ssl_context" -| ssl_ctxt /\ s |g- "ssl_session" -| ssl_sess /\
    s |t- "_buf0_" -| btyp uchar /\ s |t- "_buf1_" -| btyp uchar /\
    s |t- "_buf3_" -| btyp uchar /\ s |t- "_buf4_" -| btyp uchar /\
    s |t- "buf" -| ptyp (btyp uchar) /\ s |t- "ret" -| btyp sint32 /\
    s |t- "ssl" -| ptyp ssl_context /\ s |t- "n" -| btyp sint32 /\
    s |v- "ssl" -| pval vssl /\
    ((((((cst_pe wf_uchar a |%c%> map cst8 BU **
          cst_pe wf_uchar rb |%c%> map cst8 RB) **
          cst_pe wf_uchar id |%c%> map cst8 ID) **
          cst_pe wf_ssl_session ses |~ ssl_session ~>
            bval32 cipher0 :: bval32 length0 :: pval id :: nil
            CST_SE wf_ssl_session) **
          cst_pe wf_uint32 ciphers |% btyp uint32 %> map cst32 CI) ** TT) **
          var_e "ssl" |~ ssl_context ~> bval32 (Z2u 32 S74.client_hello) ::
            bval32 majv0 :: bval32 minv0 :: bval32 mmaj0 :: bval32 mmin0 ::
            pval ses ::
            pval (a[.+]Z2u ptr_len 8) :: pval (a[.+]Z2u ptr_len 13) ::
            bval32 (Z2u 32 5) :: pval ciphers :: pval rb :: nil
            CST_SE wf_ssl_context) s h) /\
  [var_e "buf" ]_ s = Some (pval (a[.+]Z2u ptr_len 8)) /\
  [var_e "_buf0_" ]_ s = Some (bval8 msg_type) /\
  [var_e "_buf1_" ]_ s = Some (bval8 maj_ver) /\
  [var_e "_buf3_" ]_ s = Some (bval8 m_low) /\
  [var_e "_buf4_" ]_ s = Some (bval8 m_hi) /\
  (List.length SI >= 5)%nat /\
  (BU |[ 8, 5)) = ((BU |[ 8, 0)) ++ msg_type :: maj_ver :: min_ver :: m_low :: m_hi :: nil )%list /\
  u2Z msg_type = S621.handshake).

move=> s h H.
case: H => [H [Hbuf [Hbuf0 [Hbuf1 [Hbuf3 [HSI [BU_SI msg_typ_handshake]]]]]]].
case_Hwfmem H.
split; first by assumption.
split; first by OEqtm.
split; first by OEqtm.
exists (a [.+] Z2u ptr_len 12); split.
  rewrite /= in Hbuf.
  rewrite /= Hbuf /typof /=.
  typ_var.
  by rewrite /scalez s2Z_Z2s //= add_assoc add_Z2u.
exists (cst8 m_hi).
apply strictly_exact_prop; first by apply strictly_exact_mapsto.
rewrite /wp_assign.
repeat (split => //).
- eexists; split; first by reflexivity.
  repeat Store_upd.
  split; first by OEqtm.
  split; first by OEqtm.
  split.
    split; first by Store_upd.
    repeat (split; first by done).
    repeat (split; first by Store_upd).
    move: Hmem; apply monotony => // h1.
    - apply monotony => // h2.
      apply monotony => // h3; last first.
        apply mapstos_ext_cst32 => //; repeat Store_upd; by OEqtm.
      apply monotony => // h4.
      apply monotony => // h5; last first.
        apply mapstos_ext_cst8 => //; repeat Store_upd; by OEqtm.
      apply monotony => // h6; last first.
        apply mapstos_ext_cst8 => //; repeat Store_upd; by OEqtm.
      apply mapstos_ext_cst8 => //; repeat Store_upd; by OEqtm.
    - apply mapsto_ext => //; repeat Store_upd.
      OEqtm. by apply cover_ssl_context.
      OEqtm. by apply cover_ssl_context.
      reflexivity.
  repeat (split; first by done).
  split; last by done.
  by rewrite BU_SI hd_SI Hmaj_ver Hmin_ver Hm_low Hm_hi.
-
  rewrite (skipn_nth_firstn (Z2u 8 0) 12 BU) in Hmem; last first.
    apply Z_of_nat_le_inj; by rewrite len_BU.
  rewrite !con_assoc_equiv in Hmem.
  case: Hmem => h1 [h2 [h1_d_h2 [h1_U_h2 [Hh1 Hh2]]]].
  apply mapstos_app_sepcon_cst8 in Hh1; last 3 first.
    rewrite (len_firstn (Zabs_nat SSL_BUFFER_LEN)) // -len_BU Zabs_nat_Z_of_nat //.
    apply Z_of_nat_le_inj; by rewrite len_BU.
    exact wf_store_s.
    by OEqtm.
  rewrite con_com_equiv map_cons con_assoc_equiv in Hh1.
  apply con_TT_inv.
  exists h1, h2; repeat (split => //).
  move: Hh1; apply monotony => // h'.
  apply mapsto_ext.
  by OEqtm.
  by OEqtm.
  rewrite /= in Hbuf.
  rewrite [in X in _ = X]/= Hbuf.
  rewrite /typof [typ_of _ _ _]/=.
  typ_var.
  rewrite sizeof_btyp s2Z_Z2s // (len_firstn (Zabs_nat SSL_BUFFER_LEN)); last first.
    apply Z_of_nat_le_inj; by rewrite Z_of_nat_Zabs_nat.
    by rewrite -len_BU Zabs_nat_Z_of_nat.
  rewrite /= sizeof_btyp s2Z_Z2s //.
  f_equal.
  f_equal.
  rewrite /scalez /= add_assoc.
  by rewrite add_Z2u.
  rewrite /= in BU_SI.
  rewrite hd_SI Hmaj_ver /= Hmin_ver Hm_low Hm_hi in BU_SI.
  rewrite /slice in BU_SI.

  rewrite (nth_firstn_skipn (Z2u 8 0)) in BU_SI; last first.
    apply Z_of_nat_lt_inj; by rewrite len_BU.
  rewrite (nth_firstn_skipn (Z2u 8 0)) in BU_SI; last first.
    apply Z_of_nat_lt_inj; by rewrite len_BU.
  rewrite (nth_firstn_skipn (Z2u 8 0)) in BU_SI; last first.
    apply Z_of_nat_lt_inj; by rewrite len_BU.
  rewrite (nth_firstn_skipn (Z2u 8 0)) in BU_SI; last first.
    apply Z_of_nat_lt_inj; by rewrite len_BU.
  rewrite (nth_firstn_skipn (Z2u 8 0)) in BU_SI; last first.
    apply Z_of_nat_lt_inj; by rewrite len_BU.
  by case: BU_SI => _ _ _ _ ->.