Skip to content

Commit bc4c2d0

Browse files
authored
Costing for expModIntger, take two. (#7080)
* Costing for expModInteger, new branch * Bigger inputs * Update cost model * Update cost model files * WIP * WIP * WIP * Finalise cost model * Update test results * Update costing code in metatheory, disallow some conformance tests * Revise the R code slightly * Update conformance budgets, adjust R code * Update comment * Formatting * Update comment in Agda conformance tests * Reduce penalty margin * Fix Agda costing function * Remove stray comment * Use default size measure for expModInteger * Update conformance test results * Update comment * Update comment * Big data * Back to small data * Indentation * FIx golden files for typechecking * Double comment
1 parent b2bde08 commit bc4c2d0

File tree

31 files changed

+639
-96
lines changed

31 files changed

+639
-96
lines changed

plutus-conformance/agda/Spec.hs

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -147,9 +147,8 @@ failingEvaluationTests =
147147
-}
148148
failingBudgetTests :: [FilePath]
149149
failingBudgetTests =
150-
-- These currently fail because (a) the Agda code doesn't know about the
151-
-- IntegerCostedLiterally size measure used by `replicateByte`, and (b)
152-
-- GHC 8.0 can't deal with `dropList`.
150+
-- These currently fail because the Agda code doesn't know about the
151+
-- IntegerCostedLiterally size measure used by `replicateByte` and `dropList`.
153152
[ "test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-07"
154153
, "test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-09"
155154
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-01"
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,2 @@
1-
({cpu: 100000112100
2-
| mem: 100000000800})
1+
({cpu: 1004094
2+
| mem: 801})
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,2 @@
1-
({cpu: 100000112100
2-
| mem: 100000000800})
1+
({cpu: 1004094
2+
| mem: 801})
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,2 @@
1-
({cpu: 100000112100
2-
| mem: 100000000800})
1+
({cpu: 1004094
2+
| mem: 801})
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,2 @@
1-
({cpu: 100000112100
2-
| mem: 100000000800})
1+
({cpu: 1004094
2+
| mem: 801})
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,2 @@
1-
({cpu: 100000112100
2-
| mem: 100000000800})
1+
({cpu: 1004094
2+
| mem: 801})

plutus-core/cost-model/budgeting-bench/Benchmarks/Integers.hs

Lines changed: 44 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,10 +2,10 @@ module Benchmarks.Integers (makeBenchmarks) where
22

33
import Common
44
import Generators
5-
65
import PlutusCore
76

87
import Criterion.Main
8+
import GHC.Num.Integer
99
import System.Random (StdGen)
1010

1111
---------------- Integer builtins ----------------
@@ -43,6 +43,47 @@ benchSameTwoIntegers gen builtinName =
4343
createTwoTermBuiltinBenchElementwise builtinName [] $ pairWith copyInteger numbers
4444
where (numbers,_) = makeBiggerIntegerArgs gen
4545

46+
{- `expModInteger a e m` calculates `a^e` modulo `m`; if `e` is negative then the
47+
function fails unless gcd(a,m) = 1, in which case there is an integer `a'` such
48+
that `a*a'` is congruent to 1 modulo `m`, and then `expModInteger a e m` is
49+
defined to be `expModInteger a' (-e) m`. If `0 <= a <= m-1` and `e>=0` then the
50+
time taken by expModInteger varies linearly with the size of `e` (and the worst
51+
case is when `e` is one less than a power of two) and quadratically with the
52+
size of `m`. A good model can be obtained by fitting a function of the form A +
53+
Byz + Cyz^2 (y=size(e), z=size(m)) to the results of the benchmarks. For most
54+
values of `a` (except for things like 0 and 1), the time taken for
55+
exponentiation is independent of the size of `a` because many intermediate
56+
powers have to be calculated, and these quickly grow so that their size is
57+
similar to that of `m`. In the benchmarks we use `a = m div 3` to start with a
58+
value of reasonable size.
59+
60+
For exponents `e<0` a little extra time is required to perform an initial
61+
modular inversion, but this only adds a percent or two to the execution time so
62+
for simplicity we benchmark only with positive values of `e`. For values of `a`
63+
with `size(a)>size(m)` an extra modular reduction has to be performed before
64+
starting the main calculation. It is difficult to model the effect of this
65+
precisely, so we impose an extra charge by increasing the cost of
66+
`expModInteger` by 50% for values of `a` with large sizes; to avoid the penalty,
67+
call `modInteger` before calling `expModInteger`.
68+
-}
69+
benchExpModInteger :: StdGen -> Benchmark
70+
benchExpModInteger _gen =
71+
let fun = ExpModInteger
72+
pow (a::Integer) (b::Integer) = a^b
73+
moduli = fmap (\n -> pow 2 (32*n) - 11) [1, 3..31]
74+
-- ^ 16 entries, sizes = 4, 12, ..., 124 bytes (memoryUsage = 1,2,...,16)
75+
es = fmap (\n -> pow 2 (fromIntegral $ integerLog2 n) - 1) moduli
76+
-- ^ Largest number less than modulus with binary expansion 1111...1.
77+
-- This is the worst case.
78+
79+
in bgroup (show fun)
80+
[bgroup (showMemoryUsage (m `div` 3))
81+
[bgroup (showMemoryUsage e)
82+
[mkBM a e m | a <- [m `div` 3] ] | e <- es ] | m <- moduli ]
83+
where mkBM a e m =
84+
benchDefault (showMemoryUsage m) $
85+
mkApp3 ExpModInteger [] a e m
86+
4687
makeBenchmarks :: StdGen -> [Benchmark]
4788
makeBenchmarks gen =
4889
[benchTwoIntegers gen makeLargeIntegerArgs AddInteger]-- SubtractInteger behaves identically.
@@ -52,3 +93,5 @@ makeBenchmarks gen =
5293
, LessThanInteger
5394
, LessThanEqualsInteger
5495
])
96+
<> [-- benchExpModInteger gen,
97+
benchExpModInteger gen]

plutus-core/cost-model/budgeting-bench/Common.hs

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -277,6 +277,29 @@ createTwoTermBuiltinBenchWithFlag fun tys flag ys zs =
277277
[bgroup (showMemoryUsage y) [mkBM y z | z <- zs] | y <- ys]]
278278
where mkBM y z = benchDefault (showMemoryUsage z) $ mkApp3 fun tys flag y z
279279

280+
{- | Given a builtin function f of type a * b -> _ together with lists xs::[a] and
281+
ys::[b], create a collection of benchmarks which run f on all pairs in
282+
{(x,y}: x in xs, y in ys}. -}
283+
createTwoTermBuiltinBenchWithWrappers
284+
:: ( fun ~ DefaultFun
285+
, uni ~ DefaultUni
286+
, uni `HasTermLevel` a
287+
, uni `HasTermLevel` b
288+
, ExMemoryUsage a'
289+
, ExMemoryUsage b'
290+
, NFData a
291+
, NFData b
292+
)
293+
=> (a -> a', b-> b')
294+
-> fun
295+
-> [Type tyname uni ()]
296+
-> [a]
297+
-> [b]
298+
-> Benchmark
299+
createTwoTermBuiltinBenchWithWrappers (wrapX, wrapY) fun tys xs ys =
300+
bgroup (show fun) [bgroup (showMemoryUsage (wrapX x)) [mkBM x y | y <- ys] | x <- xs]
301+
where mkBM x y = benchDefault (showMemoryUsage (wrapY y)) $ mkApp2 fun tys x y
302+
280303
{- | Given a builtin function f of type a * b -> _ together with a list of (a,b)
281304
pairs, create a collection of benchmarks which run f on all of the pairs in
282305
the list. This can be used when the worst-case execution time of a
@@ -379,3 +402,32 @@ createThreeTermBuiltinBenchElementwiseWithWrappers (wrapX, wrapY, wrapZ) fun tys
379402
)
380403
inputs
381404
where mkBM x y z = benchDefault (showMemoryUsage $ wrapZ z) $ mkApp3 fun tys x y z
405+
406+
407+
createThreeTermBuiltinBenchWithWrappers
408+
:: ( fun ~ DefaultFun
409+
, uni ~ DefaultUni
410+
, uni `HasTermLevel` a
411+
, uni `HasTermLevel` b
412+
, uni `HasTermLevel` c
413+
, ExMemoryUsage a'
414+
, ExMemoryUsage b'
415+
, ExMemoryUsage c'
416+
, NFData a
417+
, NFData b
418+
, NFData c
419+
)
420+
=> (a -> a', b-> b', c -> c')
421+
-> fun
422+
-> [Type tyname uni ()]
423+
-> [a]
424+
-> [b]
425+
-> [c]
426+
-> Benchmark
427+
createThreeTermBuiltinBenchWithWrappers (wrapX, wrapY, wrapZ) fun tys xs ys zs =
428+
bgroup (show fun)
429+
[bgroup (showMemoryUsage (wrapX x))
430+
[bgroup (showMemoryUsage (wrapY y))
431+
[mkBM x y z | z <- zs] | y <- ys] | x <- xs]
432+
where mkBM x y z = benchDefault (showMemoryUsage (wrapZ z)) $ mkApp3 fun tys x y z
433+

plutus-core/cost-model/create-cost-model/BuiltinMemoryModels.hs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -160,7 +160,7 @@ builtinMemoryModels = BuiltinCostModelBase
160160
, paramWriteBits = Id $ ModelThreeArgumentsLinearInX identityFunction
161161
-- The empty bytestring has memory usage 1, so we add an extra memory unit here to make sure that
162162
-- the memory cost of `replicateByte` is always nonzero. That means that we're charging one unit
163-
-- ore than we perhaps should for nonempty bytestrings, but that's negligible (plus there's some
163+
-- more than we perhaps should for nonempty bytestrings, but that's negligible (plus there's some
164164
-- overhead for bytesrings anyway). Note also that `replicateByte`'s argument is costed as a
165165
-- literal size.
166166
, paramReplicateByte = Id $ ModelTwoArgumentsLinearInX $ OneVariableLinearFunction 1 1
@@ -169,7 +169,7 @@ builtinMemoryModels = BuiltinCostModelBase
169169
, paramCountSetBits = Id $ ModelOneArgumentConstantCost 1
170170
, paramFindFirstSetBit = Id $ ModelOneArgumentConstantCost 1
171171
, paramRipemd_160 = Id $ hashMemModel Hash.ripemd_160
172-
, paramExpModInteger = Id $ ModelThreeArgumentsConstantCost 100000000000 -- FIXME: stub
172+
, paramExpModInteger = Id $ ModelThreeArgumentsLinearInZ identityFunction
173173
-- paramCaseList
174174
-- paramCaseData
175175
, paramDropList = Id $ ModelTwoArgumentsConstantCost 4

plutus-core/cost-model/create-cost-model/CreateBuiltinCostModel.hs

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -361,6 +361,14 @@ readTwoVariableQuadraticFunction var1 var2 e = do
361361
c02 <- Coefficient02 <$> getCoeff (printf "I(%s^2)" var2) e
362362
pure $ TwoVariableQuadraticFunction minVal c00 c10 c01 c20 c11 c02
363363

364+
-- Specialised version of readTwoVariableQuadraticFunction for a*YZ^2 + b*YZ
365+
readExpModCostingFunction :: MonadR m => String -> String -> SomeSEXP (Region m) -> m ExpModCostingFunction
366+
readExpModCostingFunction var1 var2 e = do
367+
c00 <- Coefficient00 <$> getCoeff "(Intercept)" e
368+
c11 <- Coefficient11 <$> getCoeff (printf "I(%s * %s)" var1 var2) e
369+
c12 <- Coefficient12 <$> getCoeff (printf "I(%s * %s^2)" var1 var2) e
370+
pure $ ExpModCostingFunction c00 c11 c12
371+
364372
-- | A two-variable costing function which is constant on one region of the
365373
-- plane and something else elsewhere.
366374
readTwoVariableFunConstOr :: MonadR m => SomeSEXP (Region m) -> m ModelConstantOrTwoArguments
@@ -429,6 +437,7 @@ readCF3 e = do
429437
"quadratic_in_z" -> ModelThreeArgumentsQuadraticInZ <$> readOneVariableQuadraticFunction "z_mem" e
430438
"linear_in_y_and_z" -> ModelThreeArgumentsLinearInYAndZ <$> readTwoVariableLinearFunction "y_mem" "z_mem" e
431439
"literal_in_y_or_linear_in_z" -> ModelThreeArgumentsLiteralInYOrLinearInZ <$> error "literal"
440+
"exp_mod_cost" -> ModelThreeArgumentsExpModCost <$> readExpModCostingFunction "y_mem" "z_mem" e
432441
_ -> error $ "Unknown three-variable model type: " ++ ty
433442

434443
readCF6 :: MonadR m => SomeSEXP (Region m) -> m ModelSixArguments

0 commit comments

Comments
 (0)