Test vector extraction

M.fst

module M

open FStar.HyperStack.ST

module HS = FStar.HyperStack
module LB = LowStar.Buffer

noeq
type vector = 
| MkVec:
  key_len: UInt32.t ->
  key:     LB.buffer UInt8.t{LB.len key == key_len} ->
  vector

let v_key = LB.gcmalloc_of_list HS.root [ 0xAAuy; 0xBBuy; 0xFFuy; ]

let v = MkVec 3ul v_key

/// New style

noextract
val is_hex_digit: Char.char -> bool
let is_hex_digit = function
  | '0' 
  | '1' 
  | '2' 
  | '3' 
  | '4' 
  | '5' 
  | '6' 
  | '7' 
  | '8' 
  | '9' 
  | 'a' | 'A' 
  | 'b' | 'B' 
  | 'c' | 'C' 
  | 'd' | 'D' 
  | 'e' | 'E' 
  | 'f' | 'F' -> true
  | _ -> false

noextract
type hex_digit = c:Char.char{is_hex_digit c}

noextract
val digit_to_int: c:hex_digit -> int
let digit_to_int = function
  | '0' -> 0
  | '1' -> 1
  | '2' -> 2
  | '3' -> 3
  | '4' -> 4
  | '5' -> 5
  | '6' -> 6
  | '7' -> 7
  | '8' -> 8
  | '9' -> 9
  | 'a' | 'A' -> 10
  | 'b' | 'B' -> 11
  | 'c' | 'C' -> 12
  | 'd' | 'D' -> 13
  | 'e' | 'E' -> 14
  | 'f' | 'F' -> 15

noextract
val hex_to_uint8: a:hex_digit -> b:hex_digit -> UInt8.t
let hex_to_uint8 a b =
  UInt8.uint_to_t FStar.Mul.(digit_to_int a * 16 + digit_to_int b)

noextract
val hex_list_to_uint8: 
  l:list Char.char{List.Tot.length l % 2 == 0 /\ List.Tot.for_all is_hex_digit l} -> 
  u:list UInt8.t{List.Tot.length u == List.Tot.length l / 2}
let rec hex_list_to_uint8 s =
  match s with
  | a :: b :: s' -> hex_to_uint8 a b :: hex_list_to_uint8 s'
  | [] -> []

noextract unfold
type hex_string = 
  s:string{normalize_term (String.strlen s) % 2 == 0 /\
           List.Tot.for_all is_hex_digit (String.list_of_string s)}

inline_for_extraction noextract
val buffer_of_hex: s:hex_string ->
  ST (b:LB.buffer UInt8.t {
    let len = String.strlen s / 2 in
    LB.recallable b /\
    LB.alloc_post_static HS.root len b /\
    LB.alloc_of_list_post len b
  } )
  (requires (fun h -> is_eternal_region HS.root 
    /\ LB.alloc_of_list_pre #UInt8.t (hex_list_to_uint8 (String.list_of_string s))))
  (ensures (fun h b h' ->
    let len = String.strlen s / 2 in
    LB.alloc_post_common HS.root len b h h' /\
    LB.as_seq h' b == Seq.of_list (hex_list_to_uint8 (String.list_of_string s))
  ))
let buffer_of_hex s =
  LB.gcmalloc_of_list HS.root 
    (normalize_term (hex_list_to_uint8 (String.list_of_string s)))

/// Example

noextract
type _vector = {
  _key: hex_string
}

noextract
let _v = {
  _key = "AABBFF";
}

let _v_key = buffer_of_hex _v._key

let v' = MkVec 3ul _v_key