Skip to content

Commit 80fb0d9

Browse files
ana-pantilieana-pantilie
authored
Add casing on builtins to the metatheory (#7895)
* Add casing on builtins to the metatheory * Address review comment
1 parent 1ef8970 commit 80fb0d9

8 files changed

Lines changed: 238 additions & 107 deletions

File tree

‎plutus-conformance/agda/Spec.hs‎

Lines changed: 31 additions & 66 deletions
Original file line numberDiff line numberDiff line change
@@ -158,44 +158,6 @@ agdaEvalUplcProg WithoutCosting =
158158
error $ "deBruijnTerm (agdaEvalUplcProg WithoutCosting): " <> show err
159159
Right namedTerm -> EvalSuccess $ UPLC.Program () version namedTerm
160160

161-
{-| A list of evaluation tests which are currently expected to fail. Once a fix
162-
for a test is pushed, the test will succeed and should be removed from the
163-
list. The entries of the list are paths from the root of plutus-conformance to
164-
the directory containing the test, eg
165-
"test-cases/uplc/evaluation/builtin/semantics/addInteger/addInteger1" -}
166-
failingEvaluationTests :: [FilePath]
167-
failingEvaluationTests =
168-
[ -- These "constant casing" tests fail because Agda metatheory does not yet
169-
-- implement casing on constant values.
170-
-- TODO: remove these tests once casing on constant is added to Agda metatheory.
171-
"test-cases/uplc/evaluation/term/constant-case/bool/bool-01"
172-
, "test-cases/uplc/evaluation/term/constant-case/bool/bool-02"
173-
, "test-cases/uplc/evaluation/term/constant-case/bool/bool-03"
174-
, "test-cases/uplc/evaluation/term/constant-case/bool/bool-04"
175-
, "test-cases/uplc/evaluation/term/constant-case/bool/bool-05"
176-
, "test-cases/uplc/evaluation/term/constant-case/bool/bool-06"
177-
, "test-cases/uplc/evaluation/term/constant-case/bool/bool-07"
178-
, "test-cases/uplc/evaluation/term/constant-case/integer/integer-01"
179-
, "test-cases/uplc/evaluation/term/constant-case/integer/integer-02"
180-
, "test-cases/uplc/evaluation/term/constant-case/integer/integer-03"
181-
, "test-cases/uplc/evaluation/term/constant-case/integer/integer-04"
182-
, "test-cases/uplc/evaluation/term/constant-case/list/list-01"
183-
, "test-cases/uplc/evaluation/term/constant-case/list/list-02"
184-
, "test-cases/uplc/evaluation/term/constant-case/list/list-03"
185-
, "test-cases/uplc/evaluation/term/constant-case/list/list-04"
186-
, "test-cases/uplc/evaluation/term/constant-case/list/list-05"
187-
, "test-cases/uplc/evaluation/term/constant-case/list/list-06"
188-
, "test-cases/uplc/evaluation/term/constant-case/list/list-07"
189-
, "test-cases/uplc/evaluation/term/constant-case/pair/pair-01"
190-
, "test-cases/uplc/evaluation/term/constant-case/pair/pair-02"
191-
, "test-cases/uplc/evaluation/term/constant-case/pair/pair-03"
192-
, "test-cases/uplc/evaluation/term/constant-case/pair/pair-04"
193-
, "test-cases/uplc/evaluation/term/constant-case/pair/pair-05"
194-
, "test-cases/uplc/evaluation/term/constant-case/unit/unit-01"
195-
, "test-cases/uplc/evaluation/term/constant-case/unit/unit-02"
196-
, "test-cases/uplc/evaluation/term/constant-case/unit/unit-03"
197-
]
198-
199161
{-| A list of budget tests which are currently expected to fail. Once a fix for
200162
a test is pushed, the test will succeed and should be removed from the list.
201163
The entries of the list are paths from the root of plutus-conformance to the
@@ -207,34 +169,37 @@ failingEvaluationTests =
207169
fail too), so this is built on top of that list rather than including copies of
208170
all of the entries here. -}
209171
failingBudgetTests :: [FilePath]
210-
failingBudgetTests = failingEvaluationTests ++ budgetOnlyFailures
211-
where
212-
-- These fail their budget test only (evaluation succeeds), currently
213-
-- because the Agda code doesn't know about the IntegerCostedLiterally
214-
-- size measure used by `replicateByte` and `dropList`.
215-
budgetOnlyFailures =
216-
[ "test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-07"
217-
, "test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-09"
218-
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-01"
219-
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-02"
220-
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-03"
221-
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-04"
222-
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-05"
223-
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-06"
224-
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-07"
225-
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-08"
226-
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-09"
227-
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-10"
228-
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-11"
229-
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-12"
230-
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-13"
231-
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-14"
232-
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-15"
233-
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-16"
234-
, "test-cases/uplc/evaluation/builtin/semantics/appendString"
235-
, "test-cases/uplc/evaluation/builtin/semantics/encodeUtf8"
236-
, "test-cases/uplc/evaluation/builtin/semantics/equalsString/equalsString-02"
237-
]
172+
failingBudgetTests =
173+
-- These fail their budget test only (evaluation succeeds), currently
174+
-- because the Agda code doesn't know about the IntegerCostedLiterally
175+
-- size measure used by `replicateByte` and `dropList`.
176+
[ "test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-07"
177+
, "test-cases/uplc/evaluation/builtin/semantics/replicateByte/case-09"
178+
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-01"
179+
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-02"
180+
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-03"
181+
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-04"
182+
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-05"
183+
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-06"
184+
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-07"
185+
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-08"
186+
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-09"
187+
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-10"
188+
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-11"
189+
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-12"
190+
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-13"
191+
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-14"
192+
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-15"
193+
, "test-cases/uplc/evaluation/builtin/semantics/dropList/dropList-16"
194+
, "test-cases/uplc/evaluation/builtin/semantics/appendString"
195+
, "test-cases/uplc/evaluation/builtin/semantics/encodeUtf8"
196+
, "test-cases/uplc/evaluation/builtin/semantics/equalsString/equalsString-02"
197+
]
198+
199+
{-| A list of evaluation tests which are currently expected to fail. Once a fix
200+
for a test is pushed, the test will succeed and should be removed from the list. -}
201+
failingEvaluationTests :: [FilePath]
202+
failingEvaluationTests = []
238203

239204
-- Run the tests: see Note [Evaluation with and without costing] above.
240205
main :: IO ()

‎plutus-metatheory/changelog.d/20260813_120000_ana.pantilie95_case_on_builtin_types.md‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
### Added
2+
3+
- Added casing on constants of builtin types (unit, bool, integer, list, pair)
4+
to the untyped CEK machine, mirroring the Haskell `CaseBuiltin DefaultUni`
5+
instance. The corresponding conformance tests now pass.

‎plutus-metatheory/src/MAlonzo/Code/Evaluator/Program.hs‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -271,7 +271,7 @@ d_executePLC_80 v0 v1
271271
MAlonzo.Code.Utils.du_withE_352
272272
(coe MAlonzo.Code.Evaluator.Base.C_runtimeError_20)
273273
(coe
274-
MAlonzo.Code.Untyped.CEK.d_stepper_1468
274+
MAlonzo.Code.Untyped.CEK.d_stepper_1562
275275
(coe MAlonzo.Code.Evaluator.Base.d_maxsteps_72)
276276
(coe
277277
MAlonzo.Code.Untyped.CEK.C__'894'_'9659'__222
@@ -992,7 +992,7 @@ du_executeUPLCwithMP_144 v0 v1 v2 v3
992992
(coe
993993
MAlonzo.Code.Utils.d_wrvalue_384
994994
(coe
995-
MAlonzo.Code.Untyped.CEKWithCost.du_stepperC_338
995+
MAlonzo.Code.Untyped.CEKWithCost.du_stepperC_342
996996
(coe v1 (coe MAlonzo.Code.Utils.C__'44'__450 (coe v4) (coe v7)))
997997
(coe MAlonzo.Code.Evaluator.Base.d_maxsteps_72)
998998
(coe
@@ -1014,7 +1014,7 @@ du_executeUPLCwithMP_144 v0 v1 v2 v3
10141014
v2
10151015
(MAlonzo.Code.Utils.d_accum_386
10161016
(coe
1017-
MAlonzo.Code.Untyped.CEKWithCost.du_stepperC_338
1017+
MAlonzo.Code.Untyped.CEKWithCost.du_stepperC_342
10181018
(coe
10191019
v1
10201020
(coe
@@ -1057,7 +1057,7 @@ d_executeUPLC_192 v0 v1
10571057
MAlonzo.Code.Utils.du_withE_352
10581058
(coe MAlonzo.Code.Evaluator.Base.C_runtimeError_20)
10591059
(coe
1060-
MAlonzo.Code.Untyped.CEK.d_stepper_1468
1060+
MAlonzo.Code.Untyped.CEK.d_stepper_1562
10611061
(coe MAlonzo.Code.Evaluator.Base.d_maxsteps_72)
10621062
(coe
10631063
MAlonzo.Code.Untyped.CEK.C__'894'_'9659'__222 (coe (0 :: Integer))

‎plutus-metatheory/src/MAlonzo/Code/Evaluator/Term.hs‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -819,7 +819,7 @@ d_runUValue_186 v0
819819
MAlonzo.Code.Utils.du_withE_352
820820
(coe MAlonzo.Code.Evaluator.Base.C_runtimeError_20)
821821
(coe
822-
MAlonzo.Code.Untyped.CEK.d_stepper_1468
822+
MAlonzo.Code.Untyped.CEK.d_stepper_1562
823823
(coe MAlonzo.Code.Evaluator.Base.d_maxsteps_72)
824824
(coe
825825
MAlonzo.Code.Untyped.CEK.C__'894'_'9659'__222 (coe (0 :: Integer))
@@ -1338,7 +1338,7 @@ d_runUCounting_202 v0 v1
13381338
(coe
13391339
MAlonzo.Code.Utils.d_wrvalue_384
13401340
(coe
1341-
MAlonzo.Code.Untyped.CEKWithCost.du_stepperC_338
1341+
MAlonzo.Code.Untyped.CEKWithCost.du_stepperC_342
13421342
(coe
13431343
MAlonzo.Code.Cost.d_machineParameters_150
13441344
(coe MAlonzo.Code.Utils.C__'44'__450 (coe v2) (coe v5)))
@@ -1376,7 +1376,7 @@ d_runUCounting_202 v0 v1
13761376
(coe
13771377
MAlonzo.Code.Utils.d_accum_386
13781378
(coe
1379-
MAlonzo.Code.Untyped.CEKWithCost.du_stepperC_338
1379+
MAlonzo.Code.Untyped.CEKWithCost.du_stepperC_342
13801380
(coe
13811381
MAlonzo.Code.Cost.d_machineParameters_150
13821382
(coe
@@ -1397,7 +1397,7 @@ d_runUCounting_202 v0 v1
13971397
(coe
13981398
MAlonzo.Code.Utils.d_accum_386
13991399
(coe
1400-
MAlonzo.Code.Untyped.CEKWithCost.du_stepperC_338
1400+
MAlonzo.Code.Untyped.CEKWithCost.du_stepperC_342
14011401
(coe
14021402
MAlonzo.Code.Cost.d_machineParameters_150
14031403
(coe

0 commit comments

Comments
 (0)