Library POLAR_library_functions_triple

Require Import ssreflect ssrbool eqtype.
Require Import ZArith_ext String_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.

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 machine_int_scope.
Local Open Scope zarith_ext_scope.

Definition slice {A : Type} (l : list A) (a n : nat) := firstn n (skipn a l).

Notation "l |[ a , n )" := (slice l a n) (at level 75, no associativity) : lists_ext_scope.

Local Open Scope lists_ext_scope.

Import RFC5246.

Definition SSL_BUFFER_LEN := 16384 + 512.

Import PolarSSL.


Local Open Scope string_scope.

Axiom ssl_fetch_input_triple : forall (nexp : exp) (n in_left0 : nat)
  (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),
  {{ fun s h => (wf_tstore (_tstore s) /\
     s |g- "ssl_context" -| PolarSSL.ssl_ctxt /\ s |g- "ssl_session" -| PolarSSL.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- "n" -| btyp sint32 /\
     s |t- "ret" -| btyp sint32 /\ s |t- "ssl" -| ptyp PolarSSL.ssl_context /\
     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 |~ PolarSSL.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" |~ PolarSSL.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 (Z_of_nat in_left0))
       :: pval ciphers
       :: pval rb
       :: nil
       CST_SE wf_ssl_context)) s h) /\
     [ nexp ]_s = Some (bval32 (Z2s 32 (Z_of_nat n))) /\
     Z_of_nat (in_left0 + n) < SSL_BUFFER_LEN
     }}
   PolarSSL.ssl_fetch_input "ret" "ssl" nexp
   {{fun s h => exists in_left : int 32,
       (wf_tstore (_tstore s) /\
         s |g- "ssl_context" -| PolarSSL.ssl_ctxt /\ s |g- "ssl_session" -| PolarSSL.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 PolarSSL.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 |~ PolarSSL.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" |~ PolarSSL.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" ]_ s = Some (bval32 (Z2s 32 0)) /\
        (Datatypes.length SI >= n)%nat /\
        (BU |[ 8 + in_left0, n )) = (SI |[ in_left0, n )) /\
        in_left = Z2u 32 (Z_of_nat in_left0) [.+] Z2u 32 (Z_of_nat n)
        \/
        [var_e "ret"%string ]_ s <> Some (bval32 (Z2s 32 0)) /\
        (List.length SI < in_left0 + n)%nat)}}.

Local Close Scope string_scope.

Axiom md5_update_triple : forall e0 e1 e2,
  {{ FF }} PolarSSL.md5_update e0 e1 e2 {{ TT }}.

Axiom sha1_update_triple : forall e0 e1 e2,
  {{ FF }} PolarSSL.sha1_update e0 e1 e2 {{ TT }}.