https://github.com/project-everest/hacl-star
Tip revision: b19fcefc0560fbbf4187ca2d32a16d8b90489341 authored by Nikhil Swamy on 16 September 2020, 17:03:35 UTC
fixing another couple of nested norms in Lib.ByteBuffer
fixing another couple of nested norms in Lib.ByteBuffer
Tip revision: b19fcef
Lib.ByteBuffer.fsti
module Lib.ByteBuffer
open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Mul
open LowStar.Buffer
open Lib.IntTypes
open Lib.Buffer
module B = LowStar.Buffer
module BS = Lib.ByteSequence
/// Host to {little,big}-endian conversions
/// TODO: missing specifications
inline_for_extraction
val uint_to_be: #t:inttype{unsigned t /\ ~(U128? t)} -> #l:secrecy_level -> uint_t t l -> uint_t t l
inline_for_extraction
val uint_to_le: #t:inttype{unsigned t /\ ~(U128? t)} -> #l:secrecy_level -> uint_t t l -> uint_t t l
inline_for_extraction
val uint_from_be: #t:inttype{unsigned t /\ ~(U128? t)} -> #l:secrecy_level -> uint_t t l -> uint_t t l
inline_for_extraction
val uint_from_le: #t:inttype{unsigned t /\ ~(U128? t)} -> #l:secrecy_level -> uint_t t l -> uint_t t l
(** Constructs the equality mask for two buffers of secret integers in constant-time *)
inline_for_extraction noextract
val buf_eq_mask:
#t:inttype{~(S128? t)}
-> #len1:size_t
-> #len2:size_t
-> b1:lbuffer (int_t t SEC) len1
-> b2:lbuffer (int_t t SEC) len2
-> len:size_t{v len <= v len1 /\ v len <= v len2}
-> res:lbuffer (int_t t SEC) (size 1) ->
Stack (int_t t SEC)
(requires fun h ->
live h b1 /\ live h b2 /\ live h res /\ disjoint res b1 /\ disjoint res b2 /\
v (bget h res 0) == v (ones t SEC))
(ensures fun h0 z h1 ->
modifies1 res h0 h1 /\
v z == v (BS.seq_eq_mask (as_seq h0 b1) (as_seq h0 b2) (v len)))
(** Compares two buffers of secret bytes of equal length in constant-time,
declassifying the result *)
inline_for_extraction
val lbytes_eq: #len:size_t -> b1:lbuffer uint8 len -> b2:lbuffer uint8 len -> Stack bool
(requires fun h -> live h b1 /\ live h b2)
(ensures fun h0 r h1 -> modifies0 h0 h1 /\ r == BS.lbytes_eq (as_seq h0 b1) (as_seq h0 b2))
inline_for_extraction
val uint_from_bytes_le:
#t:inttype{unsigned t /\ ~(U1? t)}
-> #l:secrecy_level
-> i:lbuffer (uint_t U8 l) (size (numbytes t)) ->
Stack (uint_t t l)
(requires fun h0 -> live h0 i)
(ensures fun h0 o h1 ->
h0 == h1 /\ live h1 i /\
o == BS.uint_from_bytes_le #t #l (as_seq h0 i))
inline_for_extraction
val uint_from_bytes_be:
#t:inttype{unsigned t /\ ~(U1? t)}
-> #l:secrecy_level
-> i:lbuffer (uint_t U8 l) (size (numbytes t)) ->
Stack (uint_t t l)
(requires fun h0 -> live h0 i)
(ensures fun h0 o h1 ->
h0 == h1 /\ live h1 i /\
o == BS.uint_from_bytes_be #t (as_seq h0 i))
inline_for_extraction
val uint_to_bytes_le:
#t:inttype{unsigned t}
-> #l:secrecy_level
-> o:lbuffer (uint_t U8 l) (size (numbytes t))
-> i:uint_t t l ->
Stack unit
(requires fun h0 -> live h0 o)
(ensures fun h0 _ h1 ->
live h1 o /\ modifies (loc o) h0 h1 /\
as_seq h1 o == BS.uint_to_bytes_le #t i)
inline_for_extraction
val uint_to_bytes_be:
#t:inttype{unsigned t}
-> #l:secrecy_level
-> o:lbuffer (uint_t U8 l) (size (numbytes t))
-> i:uint_t t l ->
Stack unit
(requires fun h0 -> live h0 o)
(ensures fun h0 _ h1 ->
live h1 o /\ modifies (loc o) h0 h1 /\
as_seq h1 o == BS.uint_to_bytes_be #t i)
inline_for_extraction
val uints_from_bytes_le:
#t:inttype{unsigned t /\ ~(U1? t)}
-> #l:secrecy_level
-> #len:size_t{v len * numbytes t <= max_size_t}
-> o:lbuffer (uint_t t l) len
-> i:lbuffer (uint_t U8 l) (len *! size (numbytes t)) ->
Stack unit
(requires fun h0 -> live h0 o /\ live h0 i /\ disjoint o i)
(ensures fun h0 _ h1 ->
modifies1 o h0 h1 /\
as_seq h1 o == BS.uints_from_bytes_le #t #l #(v len) (as_seq h0 i))
inline_for_extraction
val uints_from_bytes_be:
#t:inttype{unsigned t /\ ~(U1? t)}
-> #l:secrecy_level
-> #len:size_t{v len * numbytes t <= max_size_t}
-> o:lbuffer (uint_t t l) len
-> i:lbuffer (uint_t U8 l) (len *! size (numbytes t)) ->
Stack unit
(requires fun h0 -> live h0 o /\ live h0 i /\ disjoint o i)
(ensures fun h0 _ h1 ->
modifies1 o h0 h1 /\
as_seq h1 o == BS.uints_from_bytes_be #t #l #(v len) (as_seq h0 i))
inline_for_extraction
val uints_to_bytes_le:
#t:inttype{unsigned t}
-> #l:secrecy_level
-> len:size_t{v len * numbytes t <= max_size_t}
-> o:lbuffer (uint_t U8 l) (len *! size (numbytes t))
-> i:lbuffer (uint_t t l) len ->
Stack unit
(requires fun h0 -> live h0 o /\ live h0 i /\ disjoint o i)
(ensures fun h0 _ h1 ->
modifies1 o h0 h1 /\
as_seq h1 o == BS.uints_to_bytes_le #t #l #(v len) (as_seq h0 i))
inline_for_extraction
val uints_to_bytes_be:
#t:inttype{unsigned t}
-> #l:secrecy_level
-> len:size_t{v len * numbytes t <= max_size_t}
-> o:lbuffer (uint_t U8 l) (len *! size (numbytes t))
-> i:lbuffer (uint_t t l) len ->
Stack unit
(requires fun h0 -> live h0 o /\ live h0 i /\ disjoint o i)
(ensures fun h0 _ h1 ->
modifies1 o h0 h1 /\
as_seq h1 o == BS.uints_to_bytes_be #t #l #(v len) (as_seq h0 i))
inline_for_extraction
let uint32s_to_bytes_le len = uints_to_bytes_le #U32 #SEC len
inline_for_extraction
let uint32s_from_bytes_le #len = uints_from_bytes_le #U32 #SEC #len
inline_for_extraction
val uint_at_index_le:
#t:inttype{unsigned t /\ ~(U1? t)}
-> #l:secrecy_level
-> #len:size_t{v len * numbytes t <= max_size_t}
-> i:lbuffer (uint_t U8 l) (len *! size (numbytes t))
-> idx:size_t{v idx < v len} ->
Stack (uint_t t l)
(requires fun h0 -> live h0 i)
(ensures fun h0 r h1 ->
h0 == h1 /\
r == BS.uint_at_index_le #t #l #(v len) (as_seq h0 i) (v idx))
inline_for_extraction
val uint_at_index_be:
#t:inttype{unsigned t /\ ~(U1? t)}
-> #l:secrecy_level
-> #len:size_t{v len * numbytes t <= max_size_t}
-> i:lbuffer (uint_t U8 l) (len *! size (numbytes t))
-> idx:size_t{v idx < v len} ->
Stack (uint_t t l)
(requires fun h0 -> live h0 i)
(ensures fun h0 r h1 ->
h0 == h1 /\
r == BS.uint_at_index_be #t #l #(v len) (as_seq h0 i) (v idx))