Hash module

Hash values represent a string of hash bits, and support associated bit string operations.

Representations for Hash type

We consider two representations for a hash value:

  • as a linked list of booleans, as BitList below; or,

  • as a bit vector packed into a Word type (specifically, Word32).

Why?

Bit lists are closest to the mathematical definition of finite, but unbounded bit strings.

However, for practical applications, a bit vector provides (much) more efficient operations over a bit list, but limits the length of each bit string to that of a word.

For this reason, we recommend using bit vectors for hash values, and other practical situations. We define the type Hash below as such.

Canonical representations

We choose a canonical representation of hash values for the rest of the standard library to use, based on the (more efficient) bit vector representation:

public type Hash = BitVec;
public let Hash = BitVec;

A "bit string" as a linked list of bits:

public type BitList = ?(Bool, BitList);

A "bit vector" is a bounded-length bit string packed into a single word:

public type BitVec = Word32;

module BitVec

A "bit vector" is a bounded-length bit string packed into a single word.

 public type t = BitVec ;

 public func hashWord8s(key:[BitVec]) : BitVec ;

 public func length() : Nat ;

 public func hashOfInt(i:Int) : BitVec ;

 public func hashOfIntAcc(h1:BitVec, i:Int) : BitVec ;

 public func hashOfText(t:Text) : BitVec ;

Project a given bit from the bit vector:

 public func getHashBit(h:BitVec, pos:Nat) : Bool ;

Test if two lists of bits are equal:-

public func hashEq(ha:BitVec, hb:BitVec) : Bool ;

Helpers

 public func bitsPrintRev(bits:BitVec) ;

 public func hashPrintRev(bits:BitVec) ;

 public func toList(v:BitVec) : BitList ;

module BitList

Encode hashes as lists of booleans.

public type t = BitList;

public func hashOfInt(i:Int) : BitList ;

Test if two lists of bits are equal.

public func getHashBit(h:BitList, pos:Nat) : Bool ;

Test if two lists of bits are equal.

public func hashEq(ha:BitList, hb:BitList) : Bool ;

Helpers

public func bitsPrintRev(bits:BitList) ;

public func hashPrintRev(bits:BitList) ;