val strong (pv: TC.protocolVersion) : bool
val strong (pv: TC.protocolVersion) : bool
let strong (pv:TC.protocolVersion): bool = false
﻿(* Copyright (C) 2012--2015 Microsoft Research and INRIA *)
module MiTLS.RSAKey
open MiTLS

module HS = FStar.HyperStack //Added automatically

open FStar.Bytes
open FStar.HyperStack.All

module TC = MiTLS.TLSConstants

type pk = bytes
type sk = bytes

type pred = | SK_PK of sk * pk

(* TODO: use the following to idealize *)
//let honest_log = FStar.Error.if_ideal (fun _ -> ref [])

//let honest (pk:pk): bool = failwith "only used in ideal implementation, unverified"
let honest (pk:pk): bool = false
/
prims.fst.checked MiTLS.TLSConstants.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked FStar.Bytes.fsti.checked
MiTLS.RSAKey.fst
pv: MiTLS.TLSConstants.protocolVersion -> Prims.bool
MiTLS.TLSConstants.protocolVersion Prims.bool
let strong (pv: TC.protocolVersion) : bool =
  
false