val mk_auth_conf (auth: list auth_level) (conf: list conf_level)
    : Pure auth_conf
      (requires (normalize_term (List.Tot.length auth) = normalize_term (List.Tot.length conf)))
      (ensures (fun _ -> True))
val mk_auth_conf (auth: list auth_level) (conf: list conf_level)
    : Pure auth_conf
      (requires (normalize_term (List.Tot.length auth) = normalize_term (List.Tot.length conf)))
      (ensures (fun _ -> True))
let mk_auth_conf(auth : list auth_level) (conf : list conf_level) :
  Pure auth_conf
  (requires (normalize_term (List.Tot.length auth) = normalize_term (List.Tot.length conf)))
  (ensures (fun _ -> True)) =
  normalize_term_spec (List.Tot.length auth);
  normalize_term_spec (List.Tot.length conf);
  auth, conf
module Spec.Noise.PatternsSecurity

open Spec.Noise.Base
open Spec.Noise.WellFormedness
open Meta.Noise
open Spec.Noise.AuthConf
open Spec.Noise.Patterns
module T = FStar.Tactics
open FStar.List.Tot

#set-options "--z3rlimit 15 --fuel 0 --ifuel 0"

(*** Reference levels *)
/// The following file defines the security (secrecy, authentication, identity hiding)
/// levels for the patterns listed in the Noise technical paper.
/// We just copied the levels listed in the paper.

//type secrecy_level = x:nat{x <= 5}
//type auth_level = x:nat{x <= 2}
type id_hide_level = nat // x:nat{x <= 9}

type pattern_levels = {
  confidentiality : list conf_level;
  authentication : (auth:list auth_level{List.Tot.length auth = List.Tot.length confidentiality});
  init_hide : option id_hide_level;
  resp_hide : option id_hide_level;
}

type auth_conf =
  ls:((list auth_level) & (list conf_level)) {
    let ls1, ls2 = ls in
    List.Tot.length ls1 = List.Tot.length ls2
  }

type id_hide = option id_hide_level & option id_hide_level // (initiator, responder)
/
Spec.Noise.WellFormedness.fsti.checked Spec.Noise.Patterns.fst.checked Spec.Noise.Base.fst.checked Spec.Noise.AuthConf.fst.checked prims.fst.checked Meta.Noise.fsti.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.Properties.fst.checked FStar.List.Tot.fst.checked
Spec.Noise.PatternsSecurity.fst
auth: Prims.list Spec.Noise.AuthConf.auth_level -> conf: Prims.list Spec.Noise.AuthConf.conf_level
  -> Prims.Pure Spec.Noise.PatternsSecurity.auth_conf
Prims.list Spec.Noise.AuthConf.auth_level Spec.Noise.AuthConf.conf_level FStar.Pervasives.Native.Mktuple2 Prims.unit FStar.Pervasives.normalize_term_spec Prims.nat FStar.List.Tot.Base.length Spec.Noise.PatternsSecurity.auth_conf Prims.b2t Prims.op_Equality FStar.Pervasives.normalize_term Prims.l_True
let mk_auth_conf (auth: list auth_level) (conf: list conf_level)
    : Pure auth_conf
      (requires (normalize_term (List.Tot.length auth) = normalize_term (List.Tot.length conf)))
      (ensures (fun _ -> True)) =
  
normalize_term_spec (List.Tot.length auth);
normalize_term_spec (List.Tot.length conf);
auth, conf