Revision c9dfbba1e24a9c5f6ede8fe47907e7c9caf3fd7d authored by Son Ho on 01 March 2021, 18:40:02 UTC, committed by Son Ho on 01 March 2021, 18:40:02 UTC
compile_intrinsics
1 parent cf5a977
Lib.Meta.fst
module Lib.Meta
open Lib.IntTypes
/// Helpers used in tests and tactics (see e.g. Test.LowStarize)
#set-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 50"
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
type hex_digit = c:Char.char{is_hex_digit c}
val int_of_hex: c:hex_digit -> int
let int_of_hex = 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
val byte_of_hex: a:hex_digit -> b:hex_digit -> int
let byte_of_hex a b =
FStar.Mul.(int_of_hex a * 16 + int_of_hex b)
unfold
type hex_string =
s:string{normalize (String.strlen s % 2 = 0) /\
normalize (List.Tot.for_all is_hex_digit (String.list_of_string s))}
#push-options "--fuel 2"
let rec as_uint8s acc
(cs:list Char.char{normalize (List.length cs % 2 = 0) /\
normalize (List.Tot.for_all is_hex_digit cs)}):
Tot (l:list uint8{List.length l = List.length acc + List.length cs / 2}) (decreases (List.length cs))
=
match cs with
| c1 :: c2 :: cs' -> as_uint8s (u8 (byte_of_hex c1 c2) :: acc) cs'
| _ -> List.rev_length acc; List.rev acc
let from_hex (s:hex_string) : Seq.lseq uint8 (String.strlen s / 2) =
Seq.seq_of_list (as_uint8s [] (String.list_of_string s))
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...