practical extraction of the certified hash function

How to build

install coq (if you don't have it)

opam install coq

build

cd proofs/hash_calculus/
./configure
make

The generated ML code

proofs/hash_calculus/coq_hash.ml

module Prefix =
 struct
 end

type t = Hash.Prefix.t * string

(** val of_bud : t option -> Hash.Prefix.t * string **)

let of_bud = function
| Some hash ->
  ((let f =
      (fun set_last_2bits n ss -> Hash.make_h ~set_last_2bits n ss) (Some 3) 2
    in
    let x = Hash.to_strings hash in f x), "")
| None -> (Hash.Prefix.zero, "")

(** val of_leaf : Value.t -> Hash.Prefix.t * string **)

let of_leaf v =
  (((fun set_last_2bits n ss -> Hash.make_h ~set_last_2bits n ss) None 0
     ((Value.to_string v) :: [])), "")

(** val of_internal : t -> t -> Hash.Prefix.t * string **)

let of_internal l r =
  (((fun set_last_2bits n ss -> Hash.make_h ~set_last_2bits n ss) (Some 0) 1
     (Hash.(^^) l r)), "")

(** val of_extender : Segment.t -> t -> Hash.Prefix.t * string **)

let of_extender seg h =
  ((fst h), (Segment.encode seg))

Axioms

• 1 <> 2
• forall xs, string_empty ^ xs = xs
• forall xs, xs ^ string_empty = xs
• forall xs ys zs, (xs ^ ys) ^ zs = xs ^ (ys ^ zs)
• forall xs1 xs2 ys1 ys2, (xs1 ^ ys1) = (xs2 ^ ys2) -> string_length ys1 = string_length ys2 -> (xs1, ys1) = (xs2, ys2)
• forall xs ys, string_length (xs ^ ys) = string_length xs + string_length ys
• forall c, string_length (string_make1 c) = 1%nat
• forall n1 n2, char_of_nat n1 = char_of_nat n2 -> n1 = n2
• forall c1 c2, string_make1 c1 = string_make1 c2 -> c1 = c2
• forall last_2bits1 n1 ss1 last_2bits2 n2 ss2, make_h last_2bits1 n1 ss1 = make_h last_2bits2 n2 ss2 -> (last_2bits1, n1, string_concat ss1) = (last_2bits2, n2, string_concat ss2)
• forall h1 h2, h1 ^^ h2 = Hash.to_strings h1 ++ Hash.to_strings h2 ++ [string_make1 (char_of_nat (string_length (string_concat (Hash.to_strings h2))))]
• forall prefix, string_length (prefix_to_string prefix) = 28%nat.
• forall p1 p2, prefix_to_string p1 = prefix_to_string p2 -> p1 = p2
• forall prefix var_part, Hash.to_strings (prefix, var_part) = [prefix_to_string prefix; var_part].
• forall bits n ss, make_h bits n ss <> Prefix.zero
• forall seg, encode seg <> string_empty
• forall x y, encode x = encode y -> x = y
• forall x y, to_string x = to_string y -> x = y