Lib.PrintBuffer.fsti
module Lib.PrintBuffer
open Lib.IntTypes
open Lib.Buffer
open FStar.HyperStack.All
val print_bytes:
len: size_t
-> buf: lbuffer uint8 len ->
Stack unit
(requires (fun h -> live h buf))
(ensures (fun h0 _ h1 -> modifies0 h0 h1))
val print_compare:
len: size_t
-> buf0: lbuffer uint8 len
-> buf1: lbuffer uint8 len ->
Stack unit
(requires (fun h -> live h buf0 /\ live h buf1))
(ensures (fun h0 _ h1 -> modifies0 h0 h1))
val print_compare_display:
len: size_t
-> buf0: lbuffer uint8 len
-> buf1: ilbuffer uint8 len ->
Stack unit
(requires (fun h -> live h buf0 /\ live h buf1))
(ensures (fun h0 _ h1 -> modifies0 h0 h1))
val result_compare_display:
len: size_t
-> buf0: lbuffer uint8 len
-> buf1: ilbuffer uint8 len ->
Stack bool
(requires (fun h -> live h buf0 /\ live h buf1))
(ensures (fun h0 _ h1 -> modifies0 h0 h1))