Hexadecimal encoding and decoding of a string

Implementation of functions to encode and decode strings into hexadecimal.

The length of the encoded string is always twice the length of the input string.

use mach.int.Int
use mach.int.Int63
use string.String
use string.Char
use string.OCaml
use string.StringBuffer

predicate valid_hex_char (c: char) =
  48 <= code c < 58 || 65 <= code c < 71

function hex (i: int) : char =
  if 0 <= i < 10 then chr (i + 48)
  else if 10 <= i < 16 then chr (i + 55)
  else "\000"[0]

let hex (i: int63) : char
  requires { 0 <= i < 16 }
  ensures  { result = hex i }
= if i < 10 then chr (i + 48) else chr (i + 55)

function xeh (c: char) : int =
  if 48 <= code c < 58 then code c - 48
  else if 65 <= code c < 71 then code c - 55
  else -1

let xeh (c: char) : int63
  requires { valid_hex_char c }
  ensures  { result = xeh c }
= if 48 <= code c < 58 then code c - 48
  else code c - 55

predicate valid_hex (s : string) =
  mod (length s) 2 = 0 &&
  ( forall i. 0 <= i < length s -> valid_hex_char s[i] )

predicate encoding (s1 s2: string) =
  length s2 = 2 * length s1 &&
  (forall i. 0 <= i < length s1 ->
             s1[i] = chr (xeh s2[2 * i] * 16 + xeh s2[2 * i + 1])) &&
  valid_hex s2

lemma decode_unique: forall s1 s2 s3.
  encoding s1 s2 /\ encoding s3 s2 -> s1 = s3

let encode (s: string) : string
  ensures { encoding s result }
= let ref i = 0 in
  let r = StringBuffer.create (length s) in
  while i < OCaml.length s do
    variant { length s - i }
    invariant { 0 <= i <= length s }
    invariant { length r = 2 * i }
    invariant { forall j. 0 <= j < i  ->
                  r[2 * j] = hex (div (code s[j]) 16) &&
                  r[2 * j + 1] = hex (mod (code s[j]) 16)
    }
    invariant { forall j. 0 <= j < 2*i -> valid_hex_char r[j]}
    let v = code s[i] in
    StringBuffer.add_char r (hex (v / 16));
    StringBuffer.add_char r (hex (v % 16));
    i <- i + 1
  done;
  StringBuffer.contents r

let decode (s: string) : string
  requires { valid_hex s }
  ensures  { encoding result s }
= let ref i = 0 in
  let r = StringBuffer.create (length s / 2) in
  while i < length s do
    variant {length s - i}
    invariant { mod i 2 = 0 }
    invariant { 0 <= i <= length s }
    invariant { length r = div i 2 }
    invariant { forall j. 0 <= j < div i 2 ->
                  r[j] = chr (xeh s[2 * j] * 16 + xeh s[2 * j + 1]) }
    let v_i = xeh s[i] in
    let v_ii = xeh s[i + 1] in
    StringBuffer.add_char r (chr (v_i * 16 + v_ii));
    i <- i + 2
  done;
  StringBuffer.contents r

let decode_encode (s: string) : unit
= let s1 = encode s in
  let s2 = decode s1 in
  assert { s = s2 }