Skip to content

Commit 7f5571e

Browse files
ttuegelttuegel
authored
Fix SideCondition normalization error (again) (#2246)
* Add test/issue-2244 * Remove Kore.Internal.SideCondition.assertNormalized The normalization check doesn't seem to serve any purpose: it is regularly violated, and the only thing we can do with the SideCondition is send it to the solver, which doesn't care about our definition of normalization.
1 parent a8c05ac commit 7f5571e

File tree

6 files changed

+37988
-13
lines changed

6 files changed

+37988
-13
lines changed

‎kore/src/Kore/Internal/SideCondition.hs

Lines changed: 4 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -152,12 +152,11 @@ andCondition
152152
-> Condition variable
153153
-> SideCondition variable
154154
andCondition SideCondition { assumedTrue } newCondition =
155-
assertNormalized result result
155+
SideCondition
156+
{ representation = toRepresentationCondition merged
157+
, assumedTrue = merged
158+
}
156159
where
157-
result = SideCondition
158-
{ representation = toRepresentationCondition merged
159-
, assumedTrue = merged
160-
}
161160
merged = assumedTrue `Condition.andCondition` newCondition
162161

163162
assumeTrueCondition
@@ -209,11 +208,3 @@ toRepresentationCondition =
209208

210209
isNormalized :: forall variable. Ord variable => SideCondition variable -> Bool
211210
isNormalized = Conditional.isNormalized . from @_ @(Condition variable)
212-
213-
assertNormalized
214-
:: forall variable a
215-
. HasCallStack
216-
=> Ord variable
217-
=> SideCondition variable
218-
-> a -> a
219-
assertNormalized = Conditional.assertNormalized . from @_ @(Condition variable)

‎test/issue-2244/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
include $(CURDIR)/../include.mk

‎test/issue-2244/spec.kore

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
[]
2+
module LISTSUM-SPEC
3+
4+
// imports
5+
import VERIFICATION []
6+
7+
8+
// claims
9+
// claim `<generatedTop>`(`<michelsonTop>`(_0,_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14,`<k>`(inj{Instruction,KItem}(`ITER___MICHELSON-COMMON-SYNTAX_Instruction_AnnotationList_Block`(`.List{"___MICHELSON-COMMON-SYNTAX_AnnotationList_Annotation_AnnotationList"}_AnnotationList`(.KList),`{_}_MICHELSON-COMMON-SYNTAX_Block_DataList`(`_;__MICHELSON-COMMON-SYNTAX_DataList_Data_DataList`(inj{Instruction,Data}(`DROP__MICHELSON-COMMON-SYNTAX_Instruction_AnnotationList`(`.List{"___MICHELSON-COMMON-SYNTAX_AnnotationList_Annotation_AnnotationList"}_AnnotationList`(.KList))),`_;__MICHELSON-COMMON-SYNTAX_DataList_Data_DataList`(inj{Instruction,Data}(`PUSH____MICHELSON-COMMON-SYNTAX_Instruction_AnnotationList_Type_Data`(`.List{"___MICHELSON-COMMON-SYNTAX_AnnotationList_Annotation_AnnotationList"}_AnnotationList`(.KList),`___MICHELSON-COMMON-SYNTAX_Type_NullaryTypeName_AnnotationList`(inj{NumTypeName,NullaryTypeName}(`int_MICHELSON-COMMON-SYNTAX_NumTypeName`(.KList)),`.List{"___MICHELSON-COMMON-SYNTAX_AnnotationList_Annotation_AnnotationList"}_AnnotationList`(.KList)),inj{Int,Data}(#token("1","Int")))),inj{Instruction,DataList}(`ADD__MICHELSON-COMMON-SYNTAX_Instruction_AnnotationList`(`.List{"___MICHELSON-COMMON-SYNTAX_AnnotationList_Annotation_AnnotationList"}_AnnotationList`(.KList))))))))),`<stack>`(inj{Stack,InternalStack}(`_;__MICHELSON-COMMON_Stack_StackElement_Stack`(`[__]_MICHELSON-COMMON_StackElement_TypeName_Data`(`___MICHELSON-COMMON_TypeName_UnaryTypeName_TypeName`(`list_MICHELSON-COMMON-SYNTAX_UnaryTypeName`(.KList),inj{NumTypeName,TypeName}(`int_MICHELSON-COMMON-SYNTAX_NumTypeName`(.KList))),inj{InternalList,Data}(IntList)),`_;__MICHELSON-COMMON_Stack_StackElement_Stack`(`[__]_MICHELSON-COMMON_StackElement_TypeName_Data`(inj{NumTypeName,TypeName}(`int_MICHELSON-COMMON-SYNTAX_NumTypeName`(.KList)),inj{Int,Data}(I)),`.List{"_;__MICHELSON-COMMON_Stack_StackElement_Stack"}_Stack`(.KList))))),_15,_16,_17,_18,_19,_20,_21,_22,_23),_DotVar0)=>`<generatedTop>`(`<michelsonTop>`(_0,_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14,`<k>`(.K),`<stack>`(inj{Stack,InternalStack}(`_;__MICHELSON-COMMON_Stack_StackElement_Stack`(`[__]_MICHELSON-COMMON_StackElement_TypeName_Data`(inj{NumTypeName,TypeName}(`int_MICHELSON-COMMON-SYNTAX_NumTypeName`(.KList)),inj{Int,Data}(?I)),`.List{"_;__MICHELSON-COMMON_Stack_StackElement_Stack"}_Stack`(.KList)))),_15,_16,_17,_18,_19,_20,_21,_22,_23),_DotVar0) requires #token("true","Bool") ensures `_==Int_`(?I,`_+Int_`(`size(_,_)_MICHELSON-COMMON_Int_InternalList_Int`(IntList,#token("0","Int")),I)) [contentStartColumn(8), contentStartLine(10), org.kframework.attributes.Location(Location(10,8,12,46)), org.kframework.attributes.Source(Source(/Users/skeirik/work/michelson-semantics/././tests/proofs/listsum-spec.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "ensures" Bool [klabel(#ruleEnsures), symbol])]
10+
claim{} \implies{SortGeneratedTopCell{}} (
11+
\and{SortGeneratedTopCell{}} (
12+
\top{SortGeneratedTopCell{}}(), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'michelsonTop'-GT-'{}(Var'Unds'0:SortParamtypeCell{},Var'Unds'1:SortParamvalueCell{},Var'Unds'2:SortStoragetypeCell{},Var'Unds'3:SortStoragevalueCell{},Var'Unds'4:SortMybalanceCell{},Var'Unds'5:SortMyamountCell{},Var'Unds'6:SortMynowCell{},Var'Unds'7:SortMyaddrCell{},Var'Unds'8:SortKnownaddrsCell{},Var'Unds'9:SortSourceaddrCell{},Var'Unds'10:SortSenderaddrCell{},Var'Unds'11:SortMychainidCell{},Var'Unds'12:SortNonceCell{},Var'Unds'13:SortBigmapsCell{},Var'Unds'14:SortScriptCell{},Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortInstruction{}, SortKItem{}}(LblITER'UndsUndsUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'AnnotationList'Unds'Block{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'MICHELSON-COMMON-SYNTAX'Unds'AnnotationList'Unds'Annotation'Unds'AnnotationList'QuotRBraUnds'AnnotationList{}(),Lbl'LBraUndsRBraUnds'MICHELSON-COMMON-SYNTAX'Unds'Block'Unds'DataList{}(Lbl'UndsSClnUndsUnds'MICHELSON-COMMON-SYNTAX'Unds'DataList'Unds'Data'Unds'DataList{}(inj{SortInstruction{}, SortData{}}(LblDROP'UndsUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'AnnotationList{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'MICHELSON-COMMON-SYNTAX'Unds'AnnotationList'Unds'Annotation'Unds'AnnotationList'QuotRBraUnds'AnnotationList{}())),Lbl'UndsSClnUndsUnds'MICHELSON-COMMON-SYNTAX'Unds'DataList'Unds'Data'Unds'DataList{}(inj{SortInstruction{}, SortData{}}(LblPUSH'UndsUndsUndsUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'AnnotationList'Unds'Type'Unds'Data{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'MICHELSON-COMMON-SYNTAX'Unds'AnnotationList'Unds'Annotation'Unds'AnnotationList'QuotRBraUnds'AnnotationList{}(),Lbl'UndsUndsUnds'MICHELSON-COMMON-SYNTAX'Unds'Type'Unds'NullaryTypeName'Unds'AnnotationList{}(inj{SortNumTypeName{}, SortNullaryTypeName{}}(Lblint'Unds'MICHELSON-COMMON-SYNTAX'Unds'NumTypeName{}()),Lbl'Stop'List'LBraQuotUndsUndsUnds'MICHELSON-COMMON-SYNTAX'Unds'AnnotationList'Unds'Annotation'Unds'AnnotationList'QuotRBraUnds'AnnotationList{}()),inj{SortInt{}, SortData{}}(\dv{SortInt{}}("1")))),inj{SortInstruction{}, SortDataList{}}(LblADD'UndsUnds'MICHELSON-COMMON-SYNTAX'Unds'Instruction'Unds'AnnotationList{}(Lbl'Stop'List'LBraQuotUndsUndsUnds'MICHELSON-COMMON-SYNTAX'Unds'AnnotationList'Unds'Annotation'Unds'AnnotationList'QuotRBraUnds'AnnotationList{}()))))))),dotk{}())),Lbl'-LT-'stack'-GT-'{}(inj{SortStack{}, SortInternalStack{}}(Lbl'UndsSClnUndsUnds'MICHELSON-COMMON'Unds'Stack'Unds'StackElement'Unds'Stack{}(Lbl'LSqBUndsUndsRSqBUnds'MICHELSON-COMMON'Unds'StackElement'Unds'TypeName'Unds'Data{}(Lbl'UndsUndsUnds'MICHELSON-COMMON'Unds'TypeName'Unds'UnaryTypeName'Unds'TypeName{}(Lbllist'Unds'MICHELSON-COMMON-SYNTAX'Unds'UnaryTypeName{}(),inj{SortNumTypeName{}, SortTypeName{}}(Lblint'Unds'MICHELSON-COMMON-SYNTAX'Unds'NumTypeName{}())),inj{SortInternalList{}, SortData{}}(VarIntList:SortInternalList{})),Lbl'UndsSClnUndsUnds'MICHELSON-COMMON'Unds'Stack'Unds'StackElement'Unds'Stack{}(Lbl'LSqBUndsUndsRSqBUnds'MICHELSON-COMMON'Unds'StackElement'Unds'TypeName'Unds'Data{}(inj{SortNumTypeName{}, SortTypeName{}}(Lblint'Unds'MICHELSON-COMMON-SYNTAX'Unds'NumTypeName{}()),inj{SortInt{}, SortData{}}(VarI:SortInt{})),Lbl'Stop'List'LBraQuotUndsSClnUndsUnds'MICHELSON-COMMON'Unds'Stack'Unds'StackElement'Unds'Stack'QuotRBraUnds'Stack{}())))),Var'Unds'15:SortInputstackCell{},Var'Unds'16:SortExpectedCell{},Var'Unds'17:SortPreCell{},Var'Unds'18:SortPostCell{},Var'Unds'19:SortInvsCell{},Var'Unds'20:SortSymbolsCell{},Var'Unds'21:SortReturncodeCell{},Var'Unds'22:SortAssumeFailedCell{},Var'Unds'23:SortTraceCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{})), weakAlwaysFinally{SortGeneratedTopCell{}} (
13+
\exists{SortGeneratedTopCell{}} (Var'Ques'I:SortInt{},
14+
\and{SortGeneratedTopCell{}} (
15+
\equals{SortBool{},SortGeneratedTopCell{}}(
16+
Lbl'UndsEqlsEqls'Int'Unds'{}(Var'Ques'I:SortInt{},Lbl'UndsPlus'Int'Unds'{}(Lblsize'LParUndsCommUndsRParUnds'MICHELSON-COMMON'Unds'Int'Unds'InternalList'Unds'Int{}(VarIntList:SortInternalList{},\dv{SortInt{}}("0")),VarI:SortInt{})),
17+
\dv{SortBool{}}("true")), Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'michelsonTop'-GT-'{}(Var'Unds'0:SortParamtypeCell{},Var'Unds'1:SortParamvalueCell{},Var'Unds'2:SortStoragetypeCell{},Var'Unds'3:SortStoragevalueCell{},Var'Unds'4:SortMybalanceCell{},Var'Unds'5:SortMyamountCell{},Var'Unds'6:SortMynowCell{},Var'Unds'7:SortMyaddrCell{},Var'Unds'8:SortKnownaddrsCell{},Var'Unds'9:SortSourceaddrCell{},Var'Unds'10:SortSenderaddrCell{},Var'Unds'11:SortMychainidCell{},Var'Unds'12:SortNonceCell{},Var'Unds'13:SortBigmapsCell{},Var'Unds'14:SortScriptCell{},Lbl'-LT-'k'-GT-'{}(dotk{}()),Lbl'-LT-'stack'-GT-'{}(inj{SortStack{}, SortInternalStack{}}(Lbl'UndsSClnUndsUnds'MICHELSON-COMMON'Unds'Stack'Unds'StackElement'Unds'Stack{}(Lbl'LSqBUndsUndsRSqBUnds'MICHELSON-COMMON'Unds'StackElement'Unds'TypeName'Unds'Data{}(inj{SortNumTypeName{}, SortTypeName{}}(Lblint'Unds'MICHELSON-COMMON-SYNTAX'Unds'NumTypeName{}()),inj{SortInt{}, SortData{}}(Var'Ques'I:SortInt{})),Lbl'Stop'List'LBraQuotUndsSClnUndsUnds'MICHELSON-COMMON'Unds'Stack'Unds'StackElement'Unds'Stack'QuotRBraUnds'Stack{}()))),Var'Unds'15:SortInputstackCell{},Var'Unds'16:SortExpectedCell{},Var'Unds'17:SortPreCell{},Var'Unds'18:SortPostCell{},Var'Unds'19:SortInvsCell{},Var'Unds'20:SortSymbolsCell{},Var'Unds'21:SortReturncodeCell{},Var'Unds'22:SortAssumeFailedCell{},Var'Unds'23:SortTraceCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{})))))
18+
[org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/Users/skeirik/work/michelson-semantics/././tests/proofs/listsum-spec.k)"), org'Stop'kframework'Stop'definition'Stop'Production{}(), contentStartLine{}(), contentStartColumn{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(10,8,12,46)")]
19+
20+
endmodule [org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(7,1,14,9)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/Users/skeirik/work/michelson-semantics/././tests/proofs/listsum-spec.k)")]

‎test/issue-2244/test-issue-2244.sh

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
#!/bin/sh
2+
exec kore-exec \
3+
vdefinition.kore \
4+
--module VERIFICATION \
5+
--strategy all \
6+
--smt-timeout 40 \
7+
--smt-reset-interval 100 \
8+
--smt z3 \
9+
--log-level \
10+
warning \
11+
--enable-log-timestamps \
12+
--prove spec.kore \
13+
--spec-module LISTSUM-SPEC \
14+
--graph-search breadth-first \
15+
\
16+
\
17+
"$@"

‎test/issue-2244/test-issue-2244.sh.out.golden

Lines changed: 202 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,202 @@
1+
/* Created: Kore.Internal.OrPattern.toTermLike */
2+
/* Spc */
3+
\and{SortGeneratedTopCell{}}(
4+
/* Created: Kore.Internal.OrPattern.toTermLike */
5+
/* Spc */
6+
\and{SortGeneratedTopCell{}}(
7+
/* Fl Fn D Sfc */
8+
Lbl'-LT-'generatedTop'-GT-'{}(
9+
/* Fl Fn D Sfc */
10+
Lbl'-LT-'michelsonTop'-GT-'{}(
11+
/* Fl Fn D Sfa */
12+
Lbl'-LT-'paramtype'-GT-'{}(
13+
/* Fl Fn D Sfa */ Var'Unds'24:SortPreType{}
14+
),
15+
/* Fl Fn D Sfa */
16+
Lbl'-LT-'paramvalue'-GT-'{}(
17+
/* Fl Fn D Sfa */ Var'Unds'25:SortPreData{}
18+
),
19+
/* Fl Fn D Sfa */
20+
Lbl'-LT-'storagetype'-GT-'{}(
21+
/* Fl Fn D Sfa */ Var'Unds'26:SortPreType{}
22+
),
23+
/* Fl Fn D Sfa */
24+
Lbl'-LT-'storagevalue'-GT-'{}(
25+
/* Fl Fn D Sfa */ Var'Unds'27:SortPreData{}
26+
),
27+
/* Fl Fn D Sfa */
28+
Lbl'-LT-'mybalance'-GT-'{}(
29+
/* Fl Fn D Sfa */ Var'Unds'28:SortMutez{}
30+
),
31+
/* Fl Fn D Sfa */
32+
Lbl'-LT-'myamount'-GT-'{}(
33+
/* Fl Fn D Sfa */ Var'Unds'29:SortMutez{}
34+
),
35+
/* Fl Fn D Sfa */
36+
Lbl'-LT-'mynow'-GT-'{}(
37+
/* Fl Fn D Sfa */
38+
Lbl'Hash'Timestamp'LParUndsRParUnds'MICHELSON-COMMON'Unds'Timestamp'Unds'Int{}(
39+
/* Fl Fn D Sfa */ Var'Unds'30:SortInt{}
40+
)
41+
),
42+
/* Fl Fn D Sfa */
43+
Lbl'-LT-'myaddr'-GT-'{}(
44+
/* Fl Fn D Sfa */ Var'Unds'31:SortAddress{}
45+
),
46+
/* Fl Fn D Sfa */
47+
Lbl'-LT-'knownaddrs'-GT-'{}(
48+
/* Fl Fn D Sfa */ Var'Unds'32:SortMap{}
49+
),
50+
/* Fl Fn D Sfa */
51+
Lbl'-LT-'sourceaddr'-GT-'{}(
52+
/* Fl Fn D Sfa */ Var'Unds'33:SortAddress{}
53+
),
54+
/* Fl Fn D Sfa */
55+
Lbl'-LT-'senderaddr'-GT-'{}(
56+
/* Fl Fn D Sfa */ Var'Unds'34:SortAddress{}
57+
),
58+
/* Fl Fn D Sfa */
59+
Lbl'-LT-'mychainid'-GT-'{}(
60+
/* Fl Fn D Sfa */
61+
Lbl'Hash'ChainId'LParUndsRParUnds'MICHELSON-COMMON'Unds'ChainId'Unds'MichelsonBytes{}(
62+
/* Fl Fn D Sfa */ Var'Unds'35:SortMichelsonBytes{}
63+
)
64+
),
65+
/* Fl Fn D Sfa */
66+
Lbl'-LT-'nonce'-GT-'{}(
67+
/* Fl Fn D Sfa */
68+
Lbl'Hash'Nonce'LParUndsRParUnds'MICHELSON-COMMON'Unds'OperationNonce'Unds'Int{}(
69+
/* Fl Fn D Sfa */ Var'Unds'36:SortInt{}
70+
)
71+
),
72+
/* Fl Fn D Sfa */
73+
Lbl'-LT-'bigmaps'-GT-'{}(
74+
/* Fl Fn D Sfa */ Var'Unds'37:SortMap{}
75+
),
76+
/* Fl Fn D Sfa */
77+
Lbl'-LT-'script'-GT-'{}(
78+
/* Fl Fn D Sfa */ Var'Unds'38:SortPreData{}
79+
),
80+
/* Fl Fn D Sfa Cl */
81+
Lbl'-LT-'k'-GT-'{}(/* Fl Fn D Sfa Cl */ dotk{}()),
82+
/* Fl Fn D Sfc */
83+
Lbl'-LT-'stack'-GT-'{}(
84+
/* Fl Fn D Sfc */
85+
/* Inj: */ inj{SortStack{}, SortInternalStack{}}(
86+
/* Fl Fn D Sfc */
87+
Lbl'UndsSClnUndsUnds'MICHELSON-COMMON'Unds'Stack'Unds'StackElement'Unds'Stack{}(
88+
/* Fl Fn D Sfc */
89+
Lbl'LSqBUndsUndsRSqBUnds'MICHELSON-COMMON'Unds'StackElement'Unds'TypeName'Unds'Data{}(
90+
/* Fl Fn D Sfa Cli */
91+
/* Inj: */ inj{SortNumTypeName{}, SortTypeName{}}(
92+
/* Fl Fn D Sfa Cl */
93+
Lblint'Unds'MICHELSON-COMMON-SYNTAX'Unds'NumTypeName{}()
94+
),
95+
/* Fl Fn D Sfc */
96+
/* Inj: */ inj{SortInt{}, SortData{}}(
97+
/* Fl Fn D Sfa */
98+
Lbl'UndsPlus'Int'Unds'{}(
99+
/* Fl Fn D Sfa */
100+
Lblsize'LParUndsCommUndsRParUnds'MICHELSON-COMMON'Unds'Int'Unds'InternalList'Unds'Int{}(
101+
/* Fl Fn D Sfa */
102+
VarL:SortInternalList{},
103+
/* Fl Fn D Sfa Cl */
104+
/* builtin: */ \dv{SortInt{}}("0")
105+
),
106+
/* Fl Fn D Sfa */
107+
Lbl'UndsPlus'Int'Unds'{}(
108+
/* Fl Fn D Sfa */ VarI:SortInt{},
109+
/* Fl Fn D Sfa Cl */
110+
/* builtin: */ \dv{SortInt{}}("1")
111+
)
112+
)
113+
)
114+
),
115+
/* Fl Fn D Sfa Cl */
116+
Lbl'Stop'List'LBraQuotUndsSClnUndsUnds'MICHELSON-COMMON'Unds'Stack'Unds'StackElement'Unds'Stack'QuotRBraUnds'Stack{}()
117+
)
118+
)
119+
),
120+
/* Fl Fn D Sfa */
121+
Lbl'-LT-'inputstack'-GT-'{}(
122+
/* Fl Fn D Sfa */
123+
Lbl'LBraUndsRBraUnds'UNIT-TEST-COMMON-SYNTAX'Unds'LiteralStack'Unds'StackElementList{}(
124+
/* Fl Fn D Sfa */ Var'Unds'39:SortStackElementList{}
125+
)
126+
),
127+
/* Fl Fn D Sfa */
128+
Lbl'-LT-'expected'-GT-'{}(
129+
/* Fl Fn D Sfa */ Var'Unds'40:SortOutputStack{}
130+
),
131+
/* Fl Fn D Sfa */
132+
Lbl'-LT-'pre'-GT-'{}(
133+
/* Fl Fn D Sfa */ Var'Unds'41:SortBlockList{}
134+
),
135+
/* Fl Fn D Sfa */
136+
Lbl'-LT-'post'-GT-'{}(
137+
/* Fl Fn D Sfa */ Var'Unds'42:SortBlockList{}
138+
),
139+
/* Fl Fn D Sfa */
140+
Lbl'-LT-'invs'-GT-'{}(/* Fl Fn D Sfa */ Var'Unds'43:SortMap{}),
141+
/* Fl Fn D Sfa */
142+
Lbl'-LT-'symbols'-GT-'{}(
143+
/* Fl Fn D Sfa */ Var'Unds'44:SortMap{}
144+
),
145+
/* Fl Fn D Sfa */
146+
Lbl'-LT-'returncode'-GT-'{}(
147+
/* Fl Fn D Sfa */ Var'Unds'45:SortInt{}
148+
),
149+
/* Fl Fn D Sfa */
150+
Lbl'-LT-'assumeFailed'-GT-'{}(
151+
/* Fl Fn D Sfa */ Var'Unds'46:SortBool{}
152+
),
153+
/* Fl Fn D Sfa */
154+
Lbl'-LT-'trace'-GT-'{}(/* Fl Fn D Sfa */ Var'Unds'47:SortK{})
155+
),
156+
/* Fl Fn D Sfa */
157+
Lbl'-LT-'generatedCounter'-GT-'{}(
158+
/* Fl Fn D Sfa */ Var'Unds'DotVar1:SortInt{}
159+
)
160+
),
161+
/* Sfa */
162+
\not{SortGeneratedTopCell{}}(
163+
/* Sfa */
164+
\equals{SortInt{}, SortGeneratedTopCell{}}(
165+
/* Fl Fn D Sfa */
166+
Lbl'UndsPlus'Int'Unds'{}(
167+
/* Fl Fn D Sfa */
168+
Lblsize'LParUndsCommUndsRParUnds'MICHELSON-COMMON'Unds'Int'Unds'InternalList'Unds'Int{}(
169+
/* Fl Fn D Sfa */ VarL:SortInternalList{},
170+
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0")
171+
),
172+
/* Fl Fn D Sfa */
173+
Lbl'UndsPlus'Int'Unds'{}(
174+
/* Fl Fn D Sfa */ VarI:SortInt{},
175+
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("1")
176+
)
177+
),
178+
/* Fl Fn D Sfa */
179+
Lbl'UndsPlus'Int'Unds'{}(
180+
/* Fl Fn D Sfa */
181+
Lblsize'LParUndsCommUndsRParUnds'MICHELSON-COMMON'Unds'Int'Unds'InternalList'Unds'Int{}(
182+
/* Fl Fn D Sfa */ VarL:SortInternalList{},
183+
/* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("1")
184+
),
185+
/* Fl Fn D Sfa */ VarI:SortInt{}
186+
)
187+
)
188+
)
189+
),
190+
/* Spa */
191+
\equals{SortInternalList{}, SortGeneratedTopCell{}}(
192+
/* Fl Fn D Sfa */ VarIntList:SortInternalList{},
193+
/* Fl Fn D Sfa */
194+
Lbl'UndsSClnSClnUndsUnds'MICHELSON-COMMON'Unds'InternalList'Unds'WrappedData'Unds'InternalList{}(
195+
/* Fl Fn D Sfa */
196+
Lbl'LSqBUndsRSqBUnds'MICHELSON-COMMON'Unds'WrappedData'Unds'Data{}(
197+
/* Fl Fn D Sfa */ VarE:SortData{}
198+
),
199+
/* Fl Fn D Sfa */ VarL:SortInternalList{}
200+
)
201+
)
202+
)

0 commit comments

Comments
 (0)