module M

open FStar.HyperStack.ST

module HS = FStar.HyperStack
module LB = LowStar.Buffer
module L  = FStar.List.Tot

noextract
type _vector = {
  _key: string;
}

noeq
type vector = {
  key:     LB.buffer UInt8.t;
  key_len: UInt32.t;
}

let v_key: LB.buffer UInt8.t = LB.gcmalloc_of_list HS.root [
  0xAAuy; 0xBBuy; 0xCCuy;
]

inline_for_extraction
let v_key_len = 3ul

let v = {
  key = v_key;
  key_len = v_key_len;
}

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

open FStar.UInt32

noextract
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
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: list Char.char -> list UInt8.t
let rec hex_list_to_uint8 s =
  match s with
  | a :: b :: s' -> hex_to_uint8 a b :: hex_list_to_uint8 s'
  | _ -> []

noextract
let _v'_key = hex_list_to_uint8 (String.list_of_string _v._key)

let v'_key = LB.gcmalloc_of_list HS.root (normalize_term _v'_key)

let v' = {
  key = v'_key;
  key_len = normalize_term (UInt32.uint_to_t (List.Tot.length _v'_key));
}