🍃 Hex.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Format.
Require Coq.Strings.Ascii.
Require TezosOfOCaml.Environment.Structs.V0.Z.
Require Coq.Arith.Arith.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Format.
Require Coq.Strings.Ascii.
Require TezosOfOCaml.Environment.Structs.V0.Z.
Require Coq.Arith.Arith.
The useful functions of Hex.v are globally opaqued, so that tactics do not
unfold them (this can break proofs)
Checks whether the char 'c' is in the list 'l'
Outputs the Z-value of an ascii character c
z0,..., zF are the Z-values of the ascii characters 0,..., F
These constants are used to check whether a x : Z is an hexadecimal digit
Definition z0 := Eval compute in Z_of_ascii "0"%char.
Definition z9 := Eval compute in Z_of_ascii "9"%char.
Definition za := Eval compute in Z_of_ascii "a"%char.
Definition zf := Eval compute in Z_of_ascii "f"%char.
Definition zA := Eval compute in Z_of_ascii "A"%char.
Definition zF := Eval compute in Z_of_ascii "F"%char.
Definition is_hex_digit (c : ascii ) : bool :=
let Zc := Z_of_ascii c in ((z0 <=? Zc ) && (Zc <=? z9)) || ((zA <=? Zc )
&& (Zc <=? zF)) || ((za <=? Zc ) && (Zc <=? zf)).
Definition z9 := Eval compute in Z_of_ascii "9"%char.
Definition za := Eval compute in Z_of_ascii "a"%char.
Definition zf := Eval compute in Z_of_ascii "f"%char.
Definition zA := Eval compute in Z_of_ascii "A"%char.
Definition zF := Eval compute in Z_of_ascii "F"%char.
Definition is_hex_digit (c : ascii ) : bool :=
let Zc := Z_of_ascii c in ((z0 <=? Zc ) && (Zc <=? z9)) || ((zA <=? Zc )
&& (Zc <=? zF)) || ((za <=? Zc ) && (Zc <=? zf)).
Outputs the ascii character corresponding to a [Z]-value [x]
if [x >= 256], [x] is replaced with [x mod 256]
if [x < 0], [x] is replaced with [0]
Definition ascii_of_Z (x : Z) : ascii :=
match x with
| Zpos p ⇒ ascii_of_pos p
| _ ⇒ "000"%char
end.
match x with
| Zpos p ⇒ ascii_of_pos p
| _ ⇒ "000"%char
end.
Takes a number [0 <= x <= 15] of type [Z] and outputs the corresponding
ascii-hexadecimal digit
No post-condition if [x] is not between 0 and 15.
Definition Z_to_hex_digit (x : Z) : ascii :=
if x <=? 9 then ascii_of_Z (z0 + x) else ascii_of_Z (za + x - 10).
if x <=? 9 then ascii_of_Z (z0 + x) else ascii_of_Z (za + x - 10).
[hex_digit_to_Z x] outputs the (optional) [Z]-value of a hex digit [x]
If [x] is not in ['0'..'9'], ['a'..'f'], or ['A'..'F'], returns None
Definition hex_digit_to_Z (c : ascii) : option Z :=
let Zc := Z_of_ascii c in
if ((z0 <=? Zc) && (Zc <=? z9))%bool then Some (Zc - z0)
else if ((Z.leb zA Zc ) && (Z.leb Zc zF))%bool then Some (Zc + 10 - zA)
else if ((Z.leb za Zc ) && (Z.leb Zc zf))%bool then Some (Zc + 10 - za)
else None.
let Zc := Z_of_ascii c in
if ((z0 <=? Zc) && (Zc <=? z9))%bool then Some (Zc - z0)
else if ((Z.leb zA Zc ) && (Z.leb Zc zF))%bool then Some (Zc + 10 - zA)
else if ((Z.leb za Zc ) && (Z.leb Zc zf))%bool then Some (Zc + 10 - za)
else None.
[of_char c] outputs the two-hexadecimal digit representation of [c]
Definition of_char (c : ascii) : ascii × ascii :=
let Zc := Z_of_ascii c in let (Zc1,Zc2) := Z.ediv_rem Zc 16 in
(Z_to_hex_digit Zc1 , Z_to_hex_digit (Zc2)).
let Zc := Z_of_ascii c in let (Zc1,Zc2) := Z.ediv_rem Zc 16 in
(Z_to_hex_digit Zc1 , Z_to_hex_digit (Zc2)).
[to_char c1 c2] is the character corresponding to the [c1c2]
hexadecimal encoding.
Returns [None] if [c1] or [c2] are not in the ranges ['0'..'9'],
['a'..'f'], or ['A'..'F'].
Definition to_char (c1 c2 : ascii): option ascii :=
let res := (hex_digit_to_Z c1 , hex_digit_to_Z c2) in
match res with
| (Some z1 , Some z2) ⇒ Some (ascii_of_Z (16 × z1 + z2))
| _ ⇒ None
end.
let res := (hex_digit_to_Z c1 , hex_digit_to_Z c2) in
match res with
| (Some z1 , Some z2) ⇒ Some (ascii_of_Z (16 × z1 + z2))
| _ ⇒ None
end.
[of_string_no_opt s] is the hexadecimal representation of the binary
string [s] while skipping the characters in the list [ignore]
when converting. Eg [of_string_no_opt [[" "%char]] "a f"].
Fixpoint of_string_no_opt (ignore : list ascii) (s : string) : string :=
match s with
| String c s0 ⇒
let s0' := of_string_no_opt ignore s0 in
if inb_ascii ignore c then s0'
else
let (c1,c2) := of_char c in
String c1 (String c2 s0')
| EmptyString ⇒ s
end.
match s with
| String c s0 ⇒
let s0' := of_string_no_opt ignore s0 in
if inb_ascii ignore c then s0'
else
let (c1,c2) := of_char c in
String c1 (String c2 s0')
| EmptyString ⇒ s
end.
[of_string ignore s] is the hexadecimal representation of the binary
string [s]. If [ignore] is [Some lig], skip the characters in the list [lig]
when converting. Eg [of_string Some [" "%char] "a f"]. The default
value of [ignore] is [☐]).
Definition of_string (ignore : option (list ascii)) (s : string) : t :=
match ignore with
| None ⇒ Hex (of_string_no_opt [] s)
| Some lig ⇒ Hex (of_string_no_opt lig s)
end.
match ignore with
| None ⇒ Hex (of_string_no_opt [] s)
| Some lig ⇒ Hex (of_string_no_opt lig s)
end.
[to_string_aux s] is the optional binary string [s0] such that
[of_string s0] is [s].
Returns [None] if [s] contains a character that is not in the range
['0'..'9'], ['a'..'f'], or ['A'..'F'].
Fixpoint to_string_aux (s : string) : option string :=
match s with
| String c1 (String c2 s0) ⇒ match to_char c1 c2 with
| None ⇒ None
| Some c ⇒ let res0 := to_string_aux s0 in match res0 with
| None ⇒ None
| Some s1 ⇒ Some (String c s1)
end
end
| String c0 EmptyString ⇒ None
| EmptyString ⇒ Some EmptyString
end.
match s with
| String c1 (String c2 s0) ⇒ match to_char c1 c2 with
| None ⇒ None
| Some c ⇒ let res0 := to_string_aux s0 in match res0 with
| None ⇒ None
| Some s1 ⇒ Some (String c s1)
end
end
| String c0 EmptyString ⇒ None
| EmptyString ⇒ Some EmptyString
end.
same as [to_string_aux s] except that [s] is in the type [t]
[to_bytes s] is the binary string [s] such that [of_bytes s] is
[s].
Returns [None] if [s] contains a character that is not in the range
['0'..'9'], ['a'..'f'], or ['A'..'F'].
Since bytes = string, [of_bytes] is an alias.
[to_bytes s] is the binary string [s0] such that [of_bytes s0] is
[s].
Returns [None] if [s] contains a character that is not in the range
['0'..'9'], ['a'..'f'], or ['A'..'F'].
Since bytes = string, [to_bytes] is an alias.
[to_bytes] and [of_bytes] are globally opaqued, so that tactics do not
unfold them (this can break proofs)
these debug functions below are not translated