IntersectMBO / IntersectMBO/formal-ledger-specifications
Use a hash function to compute the script integrity hash check
- Dominant language
- Agda
- Stars
- 52
- Forks
- 20
- Avg merge
- 6d 14h
- Merged PRs (30d)
- 7
Description
The ledger specification provides an abstract function to compute the script integrity hash
https://github.com/IntersectMBO/formal-ledger-specifications/blob/2eb52686f48329113e71fcac1965f32ba40e7e15/src/Ledger/Conway/Specification/Transaction.lagda.md?plain=1#L110-L116
this is used in
https://github.com/IntersectMBO/formal-ledger-specifications/blob/2eb52686f48329113e71fcac1965f32ba40e7e15/src/Ledger/Conway/Specification/Utxow.lagda.md?plain=1#L108-L118
which is then used in the UTXOW rule
https://github.com/IntersectMBO/formal-ledger-specifications/blob/2eb52686f48329113e71fcac1965f32ba40e7e15/src/Ledger/Conway/Specification/Utxow.lagda.md?plain=1#L170-L175
The script integrity hash check was added in #1039.
Probably `Hashable-ScriptIntegrity` should use the the same hash function that is used on the Haskell side for this purpose. At the moment, it is instantiated to `const 0`:
https://github.com/IntersectMBO/formal-ledger-specifications/blob/2eb52686f48329113e71fcac1965f32ba40e7e15/src/Ledger/Conway/Foreign/HSLedger/ExternalStructures.agda#L106
Contributor guide
Assessment
This issue has not been assessed yet.