val check_swf (hsk: handshake_pattern) : bool
val check_swf (hsk: handshake_pattern) : bool
let check_swf (hsk : handshake_pattern) : bool =
  Some? (ac_levels hsk)
/// 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)}
/
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
hsk: Spec.Noise.Base.Definitions.handshake_pattern -> Prims.bool
Spec.Noise.Base.Definitions.handshake_pattern FStar.Pervasives.Native.uu___is_Some Prims.list FStar.Pervasives.Native.tuple2 Spec.Noise.AuthConf.auth_level Spec.Noise.AuthConf.conf_level Spec.Noise.PatternsSecurity.ac_levels Prims.bool
let check_swf (hsk: handshake_pattern) : bool =
  
Some? (ac_levels hsk)