let uint8 = Lib.IntTypes.uint8
let uint8 =
Lib.IntTypes.uint8
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
Lib.IntTypes.uint8
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
let preserves_freeable #a (s: state a) (h0 h1: HS.mem): Type0 =
  freeable h0 s ==> freeable h1 s

val footprint_s: #a:alg -> state_s a -> GTot B.loc
let footprint (#a:alg) (m: HS.mem) (s: state a) =
  B.(loc_union (loc_addr_of_buffer s) (footprint_s (B.deref m s)))

inline_for_extraction noextract
val invariant_s: (#a:alg) -> HS.mem -> state_s a -> Type0

inline_for_extraction noextract
let invariant (#a:alg) (m: HS.mem) (s: state a) =
  B.live m s /\
  B.(loc_disjoint (loc_addr_of_buffer s) (footprint_s (B.deref m s))) /\
  invariant_s m (B.get m s 0)

val invariant_loc_in_footprint
  (#a: alg)
  (s: state a)
  (m: HS.mem)
: Lemma
  (requires (invariant m s))
  (ensures (B.loc_in (footprint m s) m))
  [SMTPat (invariant m s)]

val frame_invariant: #a:alg -> l:B.loc -> s:state a -> h0:HS.mem -> h1:HS.mem -> Lemma
  (requires (
    invariant h0 s /\
    B.loc_disjoint l (footprint h0 s) /\
    B.modifies l h0 h1))
  (ensures (
    invariant h1 s /\
    footprint h0 s == footprint h1 s))
  [ SMTPat (invariant h1 s); SMTPat (B.modifies l h0 h1) ]

/// Ghost accessors
/// ---------------

/// We keep ghost values for the key and the iv, meaning that their value
/// doesn't depend on the heap, once we dereference past the initial pointer.
/// This should give preservation of key and iv automatically to clients.
val kv: #a:alg -> state_s a -> GTot (Spec.key a)
val iv: #a:alg -> state_s a -> GTot (Spec.nonce a)

/// ctr is mutated from call to call
val ctr: #a:alg -> h:HS.mem -> state a -> GTot Spec.ctr

/// Stateful API
/// ------------
val uint8 : Type0
Type0