Formalize integer division and CIntegers in the metatheory - #7864
Formalize integer division and CIntegers in the metatheory#7864ana-pantilie wants to merge 16 commits into
Conversation
ana-pantilie
changed the title
| ## Quotient and remainder | ||
|
|
||
| The `quot` and `rem` functions are based on the Haskell `quot` and `rem` functions, which perform truncated division. | ||
| This follows the implementation of Haskell's `integerQuotRem#`. |
There was a problem hiding this comment.
For this to do the right thing it's important here that Agda's / and % behave identically to Haskell's quot and rem for positive arguments. Can we safely assume that this is true, or should we try to test it somehow? Maybe not: the proved properties later are helpful, and the conformance tests give us some extra assurance, and we're planning to convert more extensive Haskell property tests like these into conformance tests, which should make things a lot better.
There was a problem hiding this comment.
There was actually a bug in the implementation which was uncovered when porting the Haskell property tests to Agda proofs. I also added a property test suite which checks that the Agda semantics of the division operators is equivalent to the Haskell semantics.
|
|
||
| This type constitutes the denotational semantics of the Cardano `BuiltinInteger` type for all of the inputs to the `BuiltinInteger` builtin functions, except `equalsInteger` and `expModInteger`. | ||
|
|
||
| The inputs to `equalsInteger` are of the unrestricted `ℤ` type. The `expModInteger` function is not yet formalised and is left as future work. |
There was a problem hiding this comment.
expModInteger is an interesting case. We could implement it in Agda easily enough (exponentiate using square-and-multiply and then use %), but that might be pretty slow. On the other hand, the Haskell version uses integerPowMod#, which I think ultimately uses this C code in GMP, and it'd be out of the question to formalise that in Agda (although we could try asking Claude just to see how it reacts ...). I suppose we'll have to try something not too complicated and see if it performs reasonably.
There was a problem hiding this comment.
I opened an issue about this, thanks. https://github.com/IntersectMBO/plutus-private/issues/2381
2 participants
Fixes https://github.com/IntersectMBO/plutus-private/issues/2356