val preserves_freeable (#a: _) (s: state a) (h0 h1: HS.mem) : Type0
let preserves_freeable #a (s: state a) (h0 h1: HS.mem): Type0 =
  freeable h0 s ==> freeable h1 s
val preserves_freeable (#a: _) (s: state a) (h0 h1: HS.mem) : Type0
let preserves_freeable #a (s: state a) (h0: HS.mem) (h1: HS.mem) : Type0 =
freeable h0 s ==> freeable h1 s
NotEverCrypt.CTR.fsti.checked
Spec.Loops.fst.checked Spec.Agile.CTR.fst.checked prims.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked EverCrypt.Error.fsti.checked
NotEverCrypt.CTR.fsti
NotEverCrypt.CTR.alg NotEverCrypt.CTR.state FStar.Monotonic.HyperStack.mem Prims.l_imp NotEverCrypt.CTR.freeable
module NotEverCrypt.CTR

module ST = FStar.HyperStack.ST
module HS = FStar.HyperStack
module B = LowStar.Buffer
module G = FStar.Ghost

module Spec = Spec.Agile.CTR

open FStar.HyperStack.ST
open EverCrypt.Error

unfold noextract
let alg = Spec.cipher_alg

/// Classic boilerplate
/// -------------------

[@CAbstractStruct]
val state_s: alg -> Type0

let state alg = B.pointer (state_s alg)

inline_for_extraction noextract
val freeable_s: #(a: alg) -> state_s a -> Type0

inline_for_extraction noextract
let freeable (#a: alg) (h: HS.mem) (p: state a) =
  B.freeable p /\ freeable_s (B.deref h p)

inline_for_extraction noextract
val preserves_freeable (#a: _) (s: state a) (h0 h1: HS.mem) : Type0

    s: NotEverCrypt.CTR.state a ->
    h0: FStar.Monotonic.HyperStack.mem ->
    h1: FStar.Monotonic.HyperStack.mem
  -> Type0