Formalize integer division and CIntegers in the metatheory - #7864
Formalize integer division and CIntegers in the metatheory#7864ana-pantilie wants to merge 5 commits into
Conversation
ana-pantilie
changed the title
| mkCInteger : ℤ → Either (∅ ⊢Nf⋆ *) CInteger | ||
| mkCInteger i with CInt.minBound ≤? i | i ≤? CInt.maxBound | ||
| mkCInteger i | yes p | yes q = return (cInt i p q) | ||
| mkCInteger i | _ | _ = inj₁ (con (ne (^ (atomic aInteger)))) |
There was a problem hiding this comment.
(con (ne (^ (atomic aInteger)))) shows up multiple times. Would it be worth defining some shorthand form, or is that against the spirit of Agda?
| BUILTIN divideInteger (base $ V-con i $ V-con i') = do | ||
| i₁ ← mkCInteger i | ||
| i₂ ← mkCInteger i' | ||
| i₁/i₂ ← maybeToEither (con (ne (^ (atomic aInteger)))) (CInt.div i₁ i₂) |
There was a problem hiding this comment.
Maybe using a name like that looks like an operation could lead to confusion, especially where i₁%i₂ means two different things, both different from Agda's i₁ % i₂. Just call the results r or something? I don't really mind all that much though.
| { (app (app base (V-con integer i)) (V-con integer i')) -> do | ||
| i₁ ← mkCInteger i | ||
| i₂ ← mkCInteger i' | ||
| i₁/i₂ ← maybeToEither userError (CInt.div i₁ i₂) |
There was a problem hiding this comment.
Same comment about names as for Algorithmic/CEK.lagda.md.
| ## 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.
|
|
||
| ``` | ||
| quot : (n d : ℤ) .{{_ : NonZero d}} → ℤ | ||
| quot n d = ((sign n S.* sign d) ◃ (∣ n ∣ ℕ./ ∣ d ∣)) |
There was a problem hiding this comment.
I worried for a bit about what sign 0 is. It's + though (unlike Haskell's signum, which is 0) , so I think this is OK.
| open import Data.Product.Base using (_×_; _,_; proj₁; proj₂) | ||
| ``` | ||
|
|
||
| ## Properties |
There was a problem hiding this comment.
I didn't check all of the details of the proofs, but if Agda says they're OK I'm willing to believe it.
There was a problem hiding this comment.
|
|
||
| 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.
2 participants
Fixes https://github.com/IntersectMBO/plutus-private/issues/2356
Also adds some new conformance tests which check the integer bounds as well. I believe that since these are conformance tests, they should be as exhaustive as possible. So I should have added underflow tests for all inputs (not just the first), overflow tests for all inputs (not just the second) and tests which check that when the inputs are equal to the lower/upper bound the scripts don't error. @kwxm what do you think? I can add them as a separate PR if you agree.