Use mappings from verification key hashs, not verification keys.

[dcoutts]

In general we should not be comparing or ordering keys directly. When we need to compare or index on keys we should be using key hashes.

More specifically, the approach is that verification keys have an Eq but no Ord, while signing keys have no Eq or Ord at all.

More or less we do do that everywhere. But in the executable spec for Updates.hs we do have one place where we have a mapping from genesis verification keys to other things. It looks like it would not be a significant change to switch that over to genesis key hashes (in both executable and formal spec)

Specifically:

• AVUpdate is a Map (VKeyGenesis dsignAlgo) Applications
• PPUpdate is a Map (VKeyGenesis dsignAlgo) (Set Ppm)

And we should check for any others. Trying to compile will the latest cardano-prelude crypto classes will reveal any remaining cases.

[nc6]

Assigning this to myself, since I need to change it for integration with ouroboros-network

[JaredCorduan]

In both the Byron and Shelley formal specs, the genesis key delegation mapping (dms) has type VKeyG |-> VKey. We will need to change these to hashes as well.

[JaredCorduan]

here are the changes I am expecting for the shelley formal spec:

• figure 8 - make the type of dms be KeyHash_gen |-> VKey
• figure 10 - same as above
• figure 16 - same as above
• beginning of section 9.2 change prose description of fdms and dms
• figure 24 - make the type of dms and fdms be KeyHash_gen |-> VKey
• figure 25
  • make a new let binding, something like hgk := hash gkey
  • check that hgk \in dom dms
  • override fdms with {(s', hgk) |-> vk}
• figure 30 - we probably want better names for "gkey" since it is now a hash of a key
• figure 55
  • gkeys should now have type P (KeyHash_gen)
  • osched should now have type Slot |-> KeyHash_gen
  • change other stuff in this table affected be the above two changes
• figure 65 - change types of dms and osched
• figure 66 - rule 37 (Active-OBFT) - this rule will make the connection between the hash inside dms and the full genesis verification key.
  • now check that bslot bhb |-> hk \in osched
  • now check that hk |-> vk \in dms
  • add a new check: hk = hash bvkcold bhb

Finally, we should probably also change the UTxO witness mapping to be a set.

[nc6]

Needs to be fixed in the Byron spec also

[dcoutts]

In the actual implementation for Byron we do not use verification keys in maps, except for the AVVM/redemption case, and the auditors signed off on that exception.

So for Byron the only thing to do is to check the specs agree with the impl about the use of keys vs key hashes.

For the Shelley rules, there's more to do, as Jared notes above.

[nc6]

@dcoutts Yes, sorry, should have been clearer above - the thing that needs doing for Byron is bringing the specs in line with the implementation

[dnadales]

I've created this issue for Byron https://github.com/input-output-hk/cardano-ledger-specs/issues/760