Lib.Memzero.fsti
module Lib.Memzero
open FStar.HyperStack.All
open FStar.Mul
open Lib.IntTypes
open Lib.Buffer
// REMARK:
// The C implementation clears one 32-bit word at a time, so we need [len]
// to be such that we clear an exact multiple of 32-bit words.
// This condition can be relaxed, but it's enough for our use in e.g. Frodo.
val clear_words_u16:
nwords:size_t{v nwords % 2 == 0}
-> b:buffer uint16{v nwords <= length b}
-> Stack unit
(requires fun h -> live h b)
(ensures fun h0 _ h1 -> modifies (loc b) h0 h1 /\
as_seq h1 (gsub #MUT #uint16 #(size (length b)) b (size 0) nwords) ==
Seq.create (v nwords) (u16 0))
val clear_words_u8:
nwords:size_t{v nwords % 4 == 0}
-> b:buffer uint8{v nwords <= length b}
-> Stack unit
(requires fun h -> live h b)
(ensures fun h0 _ h1 -> modifies (loc b) h0 h1 /\
as_seq h1 (gsub #MUT #uint8 #(size (length b)) b (size 0) nwords) ==
Seq.create (v nwords) (u8 0))