Skip to content

Commit fd1c05b

Browse files
ramsay-tramsay-t
authored
Fix force delay test failures (#7091)
* WIP * Converted to the Zipper form with a much clearer relation. * With the tests turned on! * Cleanup * This also fixes the len test * Fix Typo * Fix comment on new Force Delay for ifThenElse * ForceDelay tests WIP * Added some tests with constructor annotations * Temporary MAlonzo update * More negative tests * Re-ordered for clarity * generate MAlonzo * Typo * Comments * Issue link
1 parent ffdcada commit fd1c05b

File tree

15 files changed

+5259
-8772
lines changed

15 files changed

+5259
-8772
lines changed

‎plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/ForceDelay.hs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -132,11 +132,11 @@
132132
133133
We also turn
134134
135-
> force (force ifThenElse (delay x) (delay y))
135+
> (force [ (force (builtin ifThenElse)) b (delay x) (delay y) ] )
136136
137137
into
138138
139-
> force ifThenElse x y
139+
> [ (force (builtin ifThenElse)) b x y ]
140140
141141
if both @x@ and @y@ are pure and work-free.
142142
-}

‎plutus-executables/test/certifier/Golden/len.golden

Lines changed: 168 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -3,31 +3,187 @@
33
(force
44
[
55
[
6-
(lam s-451 [ s-451 s-451 ])
76
(lam
8-
s-452
7+
f-2750
8+
[
9+
(lam
10+
s-2751
11+
[
12+
f-2750
13+
(lam
14+
x-2752
15+
[
16+
[
17+
f-2750
18+
(lam
19+
x-2753
20+
[
21+
[
22+
f-2750
23+
(lam
24+
x-2754
25+
[
26+
[
27+
f-2750
28+
(lam
29+
x-2755
30+
[
31+
[
32+
f-2750
33+
(lam
34+
x-2756
35+
[
36+
[
37+
f-2750
38+
(lam
39+
x-2757
40+
[
41+
[
42+
f-2750
43+
(lam
44+
x-2758
45+
[
46+
[
47+
f-2750
48+
(lam
49+
x-2759
50+
[
51+
[
52+
f-2750
53+
(lam
54+
x-2760
55+
[
56+
[
57+
f-2750
58+
(lam
59+
x-2761
60+
[
61+
[
62+
f-2750
63+
(lam
64+
x-2762
65+
[
66+
[
67+
f-2750
68+
(lam
69+
x-2763
70+
[
71+
[
72+
f-2750
73+
(lam
74+
x-2764
75+
[
76+
[
77+
f-2750
78+
(lam
79+
x-2765
80+
[
81+
[
82+
f-2750
83+
(lam
84+
x-2766
85+
[
86+
[
87+
f-2750
88+
(lam
89+
x-2781
90+
[
91+
[
92+
s-2751
93+
s-2751
94+
]
95+
x-2781
96+
]
97+
)
98+
]
99+
x-2766
100+
]
101+
)
102+
]
103+
x-2765
104+
]
105+
)
106+
]
107+
x-2764
108+
]
109+
)
110+
]
111+
x-2763
112+
]
113+
)
114+
]
115+
x-2762
116+
]
117+
)
118+
]
119+
x-2761
120+
]
121+
)
122+
]
123+
x-2760
124+
]
125+
)
126+
]
127+
x-2759
128+
]
129+
)
130+
]
131+
x-2758
132+
]
133+
)
134+
]
135+
x-2757
136+
]
137+
)
138+
]
139+
x-2756
140+
]
141+
)
142+
]
143+
x-2755
144+
]
145+
)
146+
]
147+
x-2754
148+
]
149+
)
150+
]
151+
x-2753
152+
]
153+
)
154+
]
155+
x-2752
156+
]
157+
)
158+
]
159+
)
160+
(lam s-2767 [ f-2750 (lam x-2768 [ [ s-2767 s-2767 ] x-2768 ]) ])
161+
]
162+
)
163+
(lam
164+
incList-2769
9165
(lam
10-
arg-453
166+
arg-2770
11167
(delay
12168
(lam
13-
ds-454
169+
ds-2771
14170
(force
15171
(case
16-
ds-454
172+
ds-2771
17173
(delay (constr 0))
18174
(lam
19-
x-455
175+
x-2772
20176
(lam
21-
xs-456
177+
xs-2773
22178
(delay
23179
(constr
24180
1
25-
[ [ (builtin addInteger) x-455 ] (con integer 1) ]
181+
[ [ (builtin addInteger) x-2772 ] (con integer 1) ]
26182
[
27183
(force
28-
[ [ s-452 s-452 ] (delay (lam x-457 x-457)) ]
184+
[ incList-2769 (delay (lam x-2774 x-2774)) ]
29185
)
30-
xs-456
186+
xs-2773
31187
]
32188
)
33189
)
@@ -40,8 +196,8 @@
40196
)
41197
)
42198
]
43-
(delay (lam x-458 x-458))
199+
(delay (lam x-2775 x-2775))
44200
]
45201
)
46202
)
47-
The compilation was not successfully certified. Please open a bug report at https://www.github.com/IntersectMBO/plutus and attach the faulty certificate.
203+
The compilation was successfully certified.

‎plutus-executables/test/certifier/Test/Certifier/Executable.hs

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -153,10 +153,7 @@ fixedPath = "test/certifier/"
153153
srcTests :: [ String ]
154154
srcTests =
155155
[ "inc"
156-
-- TODO: This is currently failing to certify. This will be fixed
157-
-- after the PR that covers counter example tracing.
158-
-- Tracked by https://github.com/IntersectMBO/plutus-private/issues/1555.
159-
-- , "len"
156+
, "len"
160157
, "MinBS"
161158
, "AA2-CSE"
162159
]

‎plutus-metatheory/plutus-metatheory.cabal

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -407,6 +407,7 @@ test-suite test-certifier
407407
hs-source-dirs: test/certifier
408408
other-modules:
409409
Test.Certifier.AST
410+
Test.Certifier.AST.ForceDelay
410411
Test.Certifier.Optimizer
411412

412413
build-depends:

‎plutus-metatheory/src/MAlonzo/Code/Untyped.hs

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -597,3 +597,19 @@ du_toWellScoped_358 ::
597597
MAlonzo.Code.Scoped.T_ScopeError_576 T__'8866'_14
598598
du_toWellScoped_358
599599
= coe du_scopeCheckU_238 (coe du_buildDebruijnEncoding_350)
600+
-- Untyped.make-integer
601+
d_make'45'integer_360 ::
602+
MAlonzo.Code.Builtin.Signature.T__'8866''9839'_4
603+
d_make'45'integer_360
604+
= coe
605+
MAlonzo.Code.RawU.du_tag2TyTag_206
606+
(coe MAlonzo.Code.RawU.C_integer_30)
607+
-- Untyped.con-integer
608+
d_con'45'integer_364 :: () -> Integer -> T__'8866'_14
609+
d_con'45'integer_364 ~v0 v1 = du_con'45'integer_364 v1
610+
du_con'45'integer_364 :: Integer -> T__'8866'_14
611+
du_con'45'integer_364 v0
612+
= coe
613+
C_con_28
614+
(coe
615+
MAlonzo.Code.RawU.C_tmCon_202 (coe d_make'45'integer_360) (coe v0))

0 commit comments

Comments
 (0)