Formalize integer division and CIntegers in the metatheory

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/addInteger/addInteger-overflow/addInteger-overflow.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/addInteger/addInteger-overflow/addInteger-overflow.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/addInteger/addInteger-underflow/addInteger-underflow.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/addInteger/addInteger-underflow/addInteger-underflow.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/divideInteger/divideInteger-overflow/divideInteger-overflow.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/divideInteger/divideInteger-overflow/divideInteger-overflow.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/divideInteger/divideInteger-underflow/divideInteger-underflow.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/divideInteger/divideInteger-underflow/divideInteger-underflow.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/lessThanEqualsInteger/lessThanEqualsInteger-overflow/lessThanEqualsInteger-overflow.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/lessThanEqualsInteger/lessThanEqualsInteger-overflow/lessThanEqualsInteger-overflow.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/lessThanEqualsInteger/lessThanEqualsInteger-underflow/lessThanEqualsInteger-underflow.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/lessThanEqualsInteger/lessThanEqualsInteger-underflow/lessThanEqualsInteger-underflow.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/lessThanInteger/lessThanInteger-overflow/lessThanInteger-overflow.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/lessThanInteger/lessThanInteger-overflow/lessThanInteger-overflow.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/lessThanInteger/lessThanInteger-underflow/lessThanInteger-underflow.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/lessThanInteger/lessThanInteger-underflow/lessThanInteger-underflow.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/modInteger/modInteger-overflow/modInteger-overflow.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/modInteger/modInteger-overflow/modInteger-overflow.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/modInteger/modInteger-underflow/modInteger-underflow.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/modInteger/modInteger-underflow/modInteger-underflow.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/multiplyInteger/multiplyInteger-overflow/multiplyInteger-overflow.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/multiplyInteger/multiplyInteger-overflow/multiplyInteger-overflow.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/multiplyInteger/multiplyInteger-underflow/multiplyInteger-underflow.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/multiplyInteger/multiplyInteger-underflow/multiplyInteger-underflow.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/quotientInteger/quotientInteger-overflow/quotientInteger-overflow.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/quotientInteger/quotientInteger-overflow/quotientInteger-overflow.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/quotientInteger/quotientInteger-underflow/quotientInteger-underflow.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/quotientInteger/quotientInteger-underflow/quotientInteger-underflow.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/remainderInteger/remainderInteger-overflow/remainderInteger-overflow.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/remainderInteger/remainderInteger-overflow/remainderInteger-overflow.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/remainderInteger/remainderInteger-underflow/remainderInteger-underflow.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/remainderInteger/remainderInteger-underflow/remainderInteger-underflow.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/subtractInteger/subtractInteger-overflow/subtractInteger-overflow.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/subtractInteger/subtractInteger-overflow/subtractInteger-overflow.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/subtractInteger/subtractInteger-underflow/subtractInteger-underflow.uplc.budget.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/subtractInteger/subtractInteger-underflow/subtractInteger-underflow.uplc.expected

@@ -0,0 +1 @@
+evaluation failure

plutus-metatheory/changelog.d/20260728_140222_ana.pantilie95_metatheory_cinteger.md

@@ -0,0 +1,5 @@
+### Added
+
+- Formalized `CInteger` and all of the `BuiltinInteger` functions which depend on it.
+- Removed the postulates for `divideInteger`, `modInteger`, `quotientInteger` and `remainderInteger`, they are now implemented in the metatheory.
+

plutus-metatheory/plutus-metatheory.cabal

@@ -158,8 +158,10 @@ library
     MAlonzo.Code.Algorithmic.RenamingSubstitution
     MAlonzo.Code.Algorithmic.Signature
     MAlonzo.Code.Builtin
+    MAlonzo.Code.Builtin.CInteger
     MAlonzo.Code.Builtin.Constant.AtomicType
     MAlonzo.Code.Builtin.Constant.Type
+    MAlonzo.Code.Builtin.Integer.Base
     MAlonzo.Code.Builtin.Signature
     MAlonzo.Code.Certifier
     MAlonzo.Code.CertifierReport

plutus-metatheory/src/Algorithmic/CEK.lagda.md

@@ -48,6 +48,9 @@ open Sig
 open Builtin.Signature.FromSig _⊢Nf⋆_ _⊢Ne⋆_ ne ` _·_ ^ con _⇒_   Π
     using (sig2type;⊢♯2TyNe♯;SigTy;sig2SigTy;saturatedSigTy;convSigTy)
 open SigTy
+
+import Builtin.CInteger as CInt
+open CInt using (CInteger; cInt)
 ```
 
 ````
@@ -186,6 +189,11 @@ discharge (V-con c)  = con c refl
 discharge (V-I⇒ b bt) = dischargeB bt
 discharge (V-IΠ b bt) = dischargeB bt
 discharge (V-constr i Tss s refl) = constr i Tss refl (dischargeStack s)
+
+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))))
 ```
 
 ## Builtin Semantics
@@ -194,28 +202,48 @@ If a builtin returns a value, then this function produces a `Value`, otherwise i
 a type that could be used in constructing the error term.
 ```
 BUILTIN : ∀ b {A} → {Ab : saturatedSigTy (signature b) A} → BApp b A Ab → Either (∅ ⊢Nf⋆ *) (Value A)
-BUILTIN addInteger (base $ V-con i $ V-con i') = inj₂ (V-con (i + i'))
-BUILTIN subtractInteger (base $ V-con i $ V-con i') = inj₂ (V-con (i - i'))
-BUILTIN multiplyInteger (base $ V-con i $ V-con i') = inj₂ (V-con (i ** i'))
-BUILTIN divideInteger (base $ V-con i $ V-con i') = decIf
-  (i' ≟ ℤ.pos 0)
-  (inj₁ (con (ne (^ (atomic aInteger)))))
-  (inj₂ (V-con (div i i')))
-BUILTIN quotientInteger (base $ V-con i $ V-con i') = decIf
-  (i' ≟ ℤ.pos 0)
-  (inj₁ (con (ne (^ (atomic aInteger)))))
-  (inj₂ (V-con (quot i i')))
-BUILTIN remainderInteger (base $ V-con i $ V-con i') = decIf
-  (i' ≟ ℤ.pos 0)
-  (inj₁ (con (ne (^ (atomic aInteger)))))
-  (inj₂ (V-con (rem i i')))
-BUILTIN modInteger (base $ V-con i $ V-con i') = decIf
-  (i' ≟ ℤ.pos 0)
-   (inj₁ (con (ne (^ (atomic aInteger)))))
-  (inj₂ (V-con (mod i i')))
-BUILTIN lessThanInteger (base $ V-con i $ V-con i') = decIf (i <? i') (inj₂ (V-con true)) (inj₂ (V-con false))
-BUILTIN lessThanEqualsInteger (base $ V-con i $ V-con i') = decIf (i ≤? i') (inj₂ (V-con true)) (inj₂ (V-con false))
-BUILTIN equalsInteger (base $ V-con i $ V-con i') = decIf (i ≟ i') (inj₂ (V-con true)) (inj₂ (V-con false))
+BUILTIN addInteger (base $ V-con i $ V-con i') = do
+  i₁ ← mkCInteger i
+  i₂ ← mkCInteger i'
+  return (V-con (CInt.add i₁ i₂))
+BUILTIN subtractInteger (base $ V-con i $ V-con i') = do
+  i₁ ← mkCInteger i
+  i₂ ← mkCInteger i'
+  return (V-con (CInt.subtract i₁ i₂))
+BUILTIN multiplyInteger (base $ V-con i $ V-con i') = do
+  i₁ ← mkCInteger i
+  i₂ ← mkCInteger i'
+  return (V-con (CInt.multiply i₁ i₂))
+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₂)
+  return (V-con i₁/i₂)
+BUILTIN quotientInteger (base $ V-con i $ V-con i') = do
+  i₁ ← mkCInteger i
+  i₂ ← mkCInteger i'
+  i₁/i₂ ← maybeToEither (con (ne (^ (atomic aInteger)))) (CInt.quot i₁ i₂)
+  return (V-con i₁/i₂)
+BUILTIN remainderInteger (base $ V-con i $ V-con i') = do
+  i₁ ← mkCInteger i
+  i₂ ← mkCInteger i'
+  i₁%i₂ ← maybeToEither (con (ne (^ (atomic aInteger)))) (CInt.rem i₁ i₂)
+  return (V-con i₁%i₂)
+BUILTIN modInteger (base $ V-con i $ V-con i') = do
+  i₁ ← mkCInteger i
+  i₂ ← mkCInteger i'
+  i₁%i₂ ← maybeToEither (con (ne (^ (atomic aInteger)))) (CInt.mod i₁ i₂)
+  return (V-con i₁%i₂)
+BUILTIN lessThanInteger (base $ V-con i $ V-con i') = do
+  i₁ ← mkCInteger i
+  i₂ ← mkCInteger i'
+  return (V-con (CInt.lessThan i₁ i₂))
+BUILTIN lessThanEqualsInteger (base $ V-con i $ V-con i') = do
+  i₁ ← mkCInteger i
+  i₂ ← mkCInteger i'
+  return (V-con (CInt.lessThanEquals i₁ i₂))
+BUILTIN equalsInteger (base $ V-con i $ V-con i') =
+  decIf (i ≟ i') (inj₂ (V-con true)) (inj₂ (V-con false))
 BUILTIN appendByteString (base $ V-con b $ V-con b') = inj₂ (V-con (concat b b'))
 BUILTIN lessThanByteString (base $ V-con b $ V-con b') = inj₂ (V-con (B< b b'))
 BUILTIN lessThanEqualsByteString (base $ V-con b $ V-con b') = inj₂ (V-con (B<= b b'))

plutus-metatheory/src/Builtin.lagda.md

@@ -506,10 +506,6 @@ whose semantics are provided by a Haskell function.
 postulate
   lengthBS                    : ByteString → Int
   index                       : ByteString → Int → Int
-  div                         : Int → Int → Int
-  quot                        : Int → Int → Int
-  rem                         : Int → Int → Int
-  mod                         : Int → Int → Int
 
   TRACE                       : {a : Set} → String → a → a
 
@@ -604,12 +600,10 @@ postulate
 -- no binding needed for addition
 -- no binding needed for subtract
 -- no binding needed for multiply
-
-{-# COMPILE GHC div  = div  #-}
-{-# COMPILE GHC quot = quot #-}
-{-# COMPILE GHC rem  = rem  #-}
-{-# COMPILE GHC mod  = mod  #-}
-
+-- no binding needed for divide
+-- no binding needed for quotient
+-- no binding needed for remainder
+-- no binding needed for mod
 -- no binding needed for lessthan
 -- no binding needed for lessthaneq
 -- no binding needed for equals

plutus-metatheory/src/Builtin/CInteger.lagda.md

@@ -0,0 +1,99 @@
+---
+title: CInteger
+layout: page
+---
+
+This module contains the formalisation of Cardano Integers.
+
+```
+module Builtin.CInteger where
+```
+
+## Imports
+
+```
+open import Data.Integer.Properties using (_≟_; _<?_; _≤?_)
+open import Relation.Nullary using (Dec; yes; no; isYes)
+open import Data.Integer.Base
+open import Data.Nat.Base as ℕ using (ℕ)
+open import Data.Sign.Base as S using (Sign)
+open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
+open import Data.Maybe using (Maybe; just; nothing; map)
+import Data.Maybe.Effectful as MaybeEff
+open import Effect.Monad using (RawMonad)
+import Agda.Primitive as Level
+open RawMonad {f = Level.lzero} MaybeEff.monad
+open import Relation.Binary.PropositionalEquality 
+open import Data.Maybe.Properties using (≡-dec)
+import Builtin.Integer.Base as Bℤ
+open import Data.Bool using (Bool)
+
+```
+
+## The CInteger type
+
+The `CInteger` type is a restriction of the `ℤ` type to the range of integers specified by `minBound` and `maxBound`.
+
+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.
+
+```
+minBound : ℤ
+minBound = - ((+ 2) ^ 262143)
+maxBound : ℤ
+maxBound = ((+ 2) ^ 262143) - (+ 1)
+
+data CInteger : Set where
+  cInt
+    : (i : ℤ)
+    → i ≥ minBound
+    → i ≤ maxBound
+    → CInteger
+```
+
+## CInteger operations
+
+```
+add : CInteger → CInteger → ℤ
+add (cInt i _ _) (cInt j _ _) = i + j
+
+subtract : CInteger → CInteger → ℤ
+subtract (cInt i _ _) (cInt j _ _) = i - j
+
+multiply : CInteger → CInteger → ℤ
+multiply (cInt i _ _) (cInt j _ _) = i * j
+
+quot : CInteger → CInteger → Maybe ℤ
+quot (cInt n _ _) (cInt d _ _) with d ≟ + 0
+... | yes _ = nothing
+... | no d≢0 = just (Bℤ.quot n d)
+  where instance
+    _ = ≢-nonZero d≢0
+
+rem : CInteger → CInteger → Maybe ℤ
+rem (cInt n _ _) (cInt d _ _) with d ≟ + 0
+... | yes _ = nothing
+... | no d≢0 = just (Bℤ.rem n d)
+  where instance
+    _ = ≢-nonZero d≢0
+
+divMod : CInteger → CInteger → Maybe (ℤ × ℤ)
+divMod (cInt n _ _) (cInt d _ _) with d ≟ + 0
+... | yes _ = nothing
+... | no d≢0 = just (Bℤ.divMod n d)
+  where instance
+    _ = ≢-nonZero d≢0
+
+div : CInteger → CInteger → Maybe ℤ
+div n d = map proj₁ (divMod n d)
+
+mod : CInteger → CInteger → Maybe ℤ
+mod n d = map proj₂ (divMod n d)
+
+lessThan : CInteger → CInteger → Bool
+lessThan (cInt i _ _) (cInt j _ _) = isYes (i <? j)
+
+lessThanEquals : CInteger → CInteger → Bool
+lessThanEquals (cInt i _ _) (cInt j _ _) = isYes (i ≤? j)
+```