Check use of keys vs key-hashes

[dnadales]

Check that the specification and implementation agree w.r.t. the use of keys vs key hashes in the mappings.

As pointed out by Duncan here https://github.com/input-output-hk/cardano-ledger-specs/issues/754#issuecomment-520819824

[dnadales]

Formal (and therefore executable) spec differ from the implementation in the use of key vs key hashes.

[dnadales]

Next, I'm checking that key hashes are consistently used in the implementation. If the difference between key and key hashes can be glossed over in the elaboration, then this discrepancy might be ok.

[dnadales]

For UTxO we have:

So we're using addresses hashes instead of addresses in the implementation :heavy_check_mark:

[dnadales]

For delegation scheduling we have:

:heavy_check_mark:

[dnadales]

Note that in the implementation we're hashing the keys before checking set inclusion:

[dnadales]

Delegation activation:

:heavy_check_mark:

[dnadales]

For update we have:

:heavy_check_mark:

[dnadales]

Finally the chain environment and state uses key hashes as well:

:heavy_check_mark: