Skip to content

Change the implementation of hash of node

yoshihiro503 requested to merge proof_ninja/plebeia:yoshihiro503@change_implementation_of_hash_of_node into master

What is proved

I prove the collision resistance of Node_hash.compute using Coq.

The definition of node

Inductive node : Set :=
| Bud : option node -> node
| Leaf : value -> node
| Internal : node -> node -> node
| Extender : segment -> node -> node.

The algorithm of computing the hash of node

Fixpoint compute node :=
  match node with
  | Bud None => zero
  | Bud (Some n) =>
    set_last_2bits 3 (h 2 (to_string (compute n)))
  | Leaf v => h 0 v
  | Internal n1 n2 =>
    set_last_2bits 0 (h 1 (to_string (compute n1) ^^ to_string (compute n2)))
  | Extender seg n => of_string (to_string (compute n) ++ seg)
  end.

The main theorem

Theorem hash_CR : forall n1 n2,
    Invariant_node n1 -> Invariant_node n2 ->
    compute n1 = compute n2 -> n1 = n2.

Parameterized functions and data types

  • (^^) : string -> string -> string
  • NodeHash.t : Set
  • zero : NodeHash.t
  • of_value : value -> NodeHash.t
  • to_string : NodeHash.t -> string
  • of_string : string -> NodeHash.t
  • h : nat -> string -> NodeHash.t
  • set_last_2bits : nat -> NodeHash.t -> NodeHash.t

Axioms

  • The function (^^) is injective
  • h _ _ must not zero
  • set_last_2bits must not zero
  • h is injective
  • to_string is injective
  • The length of the hash zero is 28
  • of_string (to_string t) = t
  • to_string (of_string s) = s if the length s >= 28
  • The length of h _ _ is always 28
  • set_last_2bits does not change the length of the input
  • length of hash is always more than 28
  • The length of (s1 ^^ s2) is grater than length s1 + length s2

Links

Merge request reports