val pattern_X : Spec.Noise.SPatterns.wfs_handshake_pattern
let pattern_X = mk_wfs_pattern Spec.Noise.Patterns.pattern_X
/// The following file takes the patterns defined in Spec.Noise.SPatterns and
/// add information about the security levels in their type.

module Spec.Noise.SPatterns

open Spec.Noise.Base
open Spec.Noise.Base
open Spec.Noise.WellFormedness
open Meta.Noise
module T = FStar.Tactics
open Spec.Noise.Patterns
open Spec.Noise.PatternsSecurity

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

type wfs_handshake_pattern = hsk:wf_handshake_pattern{Some? (ac_levels hsk)}

[@ (strict_on_arguments [0]) ] noextract
let check_swf (hsk : handshake_pattern) : bool =
  Some? (ac_levels hsk)

inline_for_extraction noextract
let mk_wfs_pattern (hsk : wf_handshake_pattern{normalize_term #bool (check_swf hsk)}) :
  wfs_handshake_pattern =
  hsk

inline_for_extraction noextract let pattern_NN = mk_wfs_pattern Spec.Noise.Patterns.pattern_NN
inline_for_extraction noextract let pattern_KN = mk_wfs_pattern Spec.Noise.Patterns.pattern_KN
inline_for_extraction noextract let pattern_NK = mk_wfs_pattern Spec.Noise.Patterns.pattern_NK
inline_for_extraction noextract let pattern_KK = mk_wfs_pattern Spec.Noise.Patterns.pattern_KK
inline_for_extraction noextract let pattern_NX = mk_wfs_pattern Spec.Noise.Patterns.pattern_NX
inline_for_extraction noextract let pattern_KX = mk_wfs_pattern Spec.Noise.Patterns.pattern_KX
inline_for_extraction noextract let pattern_XN = mk_wfs_pattern Spec.Noise.Patterns.pattern_XN
inline_for_extraction noextract let pattern_IN = mk_wfs_pattern Spec.Noise.Patterns.pattern_IN
inline_for_extraction noextract let pattern_XK = mk_wfs_pattern Spec.Noise.Patterns.pattern_XK
inline_for_extraction noextract let pattern_IK = mk_wfs_pattern Spec.Noise.Patterns.pattern_IK
inline_for_extraction noextract let pattern_XX = mk_wfs_pattern Spec.Noise.Patterns.pattern_XX
inline_for_extraction noextract let pattern_IX = mk_wfs_pattern Spec.Noise.Patterns.pattern_IX
inline_for_extraction noextract let pattern_N = mk_wfs_pattern Spec.Noise.Patterns.pattern_N
/
Spec.Noise.WellFormedness.fsti.checked Spec.Noise.PatternsSecurity.fst.checked Spec.Noise.Patterns.fst.checked Spec.Noise.Base.fst.checked prims.fst.checked Meta.Noise.fsti.checked FStar.Tactics.fst.checked FStar.Pervasives.fsti.checked
Spec.Noise.SPatterns.fst
Spec.Noise.SPatterns.wfs_handshake_pattern
Spec.Noise.SPatterns.mk_wfs_pattern Spec.Noise.Patterns.pattern_X
let pattern_X =
  
mk_wfs_pattern Spec.Noise.Patterns.pattern_X