Skip to main content

🍃 Hex.v

Environment

Gitlab

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.

The useful functions of Hex.v are globally opaqued, so that tactics do not unfold them (this can break proofs)

Inductive t : Set :=
| Hex : string t.

Checks whether the char 'c' is in the list 'l'
Definition inb_ascii (l : list ascii) (c : ascii) : bool :=
  existsb (fun c0Ascii.eqb c0 c) l.

Outputs the Z-value of an ascii character c
Definition Z_of_ascii (c : ascii) : Z.t := BinIntDef.Z.of_N (N_of_ascii 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)).

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 pascii_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).

[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.

[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)).

[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.

[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')
  | EmptyStrings
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
  | NoneHex (of_string_no_opt [] s)
  | Some ligHex (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
        | NoneNone
        | Some clet res0 := to_string_aux s0 in match res0 with
          | NoneNone
          | Some s1Some (String c s1)
          end
        end
    | String c0 EmptyStringNone
    | EmptyStringSome EmptyString
    end.

same as [to_string_aux s] except that [s] is in the type [t]
Definition to_string (hs : t) : option string :=
  match hs with
  | Hex sto_string_aux s
  end.

[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.
Definition of_bytes (ignore : option (list ascii)) (s : bytes) : t :=
  of_string ignore s.

[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.
Definition to_bytes (hs : t) : option bytes := to_string hs.

[to_bytes] and [of_bytes] are globally opaqued, so that tactics do not unfold them (this can break proofs)
Global Opaque to_bytes.
Global Opaque of_bytes.

these debug functions below are not translated
Parameter hexdump_s : option bool option bool t string.

Parameter pp : Format.formatter t unit.

Parameter show : t string.