Fix SideCondition normalization error (again)

kore/src/Kore/Internal/SideCondition.hs

@@ -152,12 +152,11 @@ andCondition
     -> Condition variable
     -> SideCondition variable
 andCondition SideCondition { assumedTrue } newCondition =
-    assertNormalized result result
+    SideCondition
+    { representation = toRepresentationCondition merged
+    , assumedTrue = merged
+    }
   where
-    result = SideCondition
-        { representation = toRepresentationCondition merged
-        , assumedTrue = merged
-        }
     merged = assumedTrue `Condition.andCondition` newCondition
 
 assumeTrueCondition
@@ -209,11 +208,3 @@ toRepresentationCondition =
 
 isNormalized :: forall variable. Ord variable => SideCondition variable -> Bool
 isNormalized = Conditional.isNormalized . from @_ @(Condition variable)
-
-assertNormalized
-    :: forall variable a
-    .  HasCallStack
-    => Ord variable
-    => SideCondition variable
-    -> a -> a
-assertNormalized = Conditional.assertNormalized . from @_ @(Condition variable)

test/issue-2244/Makefile

@@ -0,0 +1 @@
+include $(CURDIR)/../include.mk

test/issue-2244/spec.kore

@@ -0,0 +1,20 @@
+[]
+module LISTSUM-SPEC
+
+// imports
+import VERIFICATION []
+
+
+// claims
+// 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])]
+  claim{} \implies{SortGeneratedTopCell{}} (
+      \and{SortGeneratedTopCell{}} (
+      \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{}} (
+       \exists{SortGeneratedTopCell{}} (Var'Ques'I:SortInt{}, 
+      \and{SortGeneratedTopCell{}} (
+      \equals{SortBool{},SortGeneratedTopCell{}}(
+        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{})),
+        \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{})))))
+  [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)")]
+
+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

@@ -0,0 +1,17 @@
+#!/bin/sh
+exec kore-exec \
+    vdefinition.kore \
+    --module VERIFICATION \
+    --strategy all \
+    --smt-timeout 40 \
+    --smt-reset-interval 100 \
+    --smt z3 \
+    --log-level \
+    warning \
+    --enable-log-timestamps \
+    --prove spec.kore \
+    --spec-module LISTSUM-SPEC \
+    --graph-search breadth-first \
+     \
+     \
+    "$@"

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

@@ -0,0 +1,202 @@
+/* Created: Kore.Internal.OrPattern.toTermLike */
+/* Spc */
+\and{SortGeneratedTopCell{}}(
+    /* Created: Kore.Internal.OrPattern.toTermLike */
+    /* Spc */
+    \and{SortGeneratedTopCell{}}(
+        /* Fl Fn D Sfc */
+        Lbl'-LT-'generatedTop'-GT-'{}(
+            /* Fl Fn D Sfc */
+            Lbl'-LT-'michelsonTop'-GT-'{}(
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'paramtype'-GT-'{}(
+                    /* Fl Fn D Sfa */ Var'Unds'24:SortPreType{}
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'paramvalue'-GT-'{}(
+                    /* Fl Fn D Sfa */ Var'Unds'25:SortPreData{}
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'storagetype'-GT-'{}(
+                    /* Fl Fn D Sfa */ Var'Unds'26:SortPreType{}
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'storagevalue'-GT-'{}(
+                    /* Fl Fn D Sfa */ Var'Unds'27:SortPreData{}
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'mybalance'-GT-'{}(
+                    /* Fl Fn D Sfa */ Var'Unds'28:SortMutez{}
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'myamount'-GT-'{}(
+                    /* Fl Fn D Sfa */ Var'Unds'29:SortMutez{}
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'mynow'-GT-'{}(
+                    /* Fl Fn D Sfa */
+                    Lbl'Hash'Timestamp'LParUndsRParUnds'MICHELSON-COMMON'Unds'Timestamp'Unds'Int{}(
+                        /* Fl Fn D Sfa */ Var'Unds'30:SortInt{}
+                    )
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'myaddr'-GT-'{}(
+                    /* Fl Fn D Sfa */ Var'Unds'31:SortAddress{}
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'knownaddrs'-GT-'{}(
+                    /* Fl Fn D Sfa */ Var'Unds'32:SortMap{}
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'sourceaddr'-GT-'{}(
+                    /* Fl Fn D Sfa */ Var'Unds'33:SortAddress{}
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'senderaddr'-GT-'{}(
+                    /* Fl Fn D Sfa */ Var'Unds'34:SortAddress{}
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'mychainid'-GT-'{}(
+                    /* Fl Fn D Sfa */
+                    Lbl'Hash'ChainId'LParUndsRParUnds'MICHELSON-COMMON'Unds'ChainId'Unds'MichelsonBytes{}(
+                        /* Fl Fn D Sfa */ Var'Unds'35:SortMichelsonBytes{}
+                    )
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'nonce'-GT-'{}(
+                    /* Fl Fn D Sfa */
+                    Lbl'Hash'Nonce'LParUndsRParUnds'MICHELSON-COMMON'Unds'OperationNonce'Unds'Int{}(
+                        /* Fl Fn D Sfa */ Var'Unds'36:SortInt{}
+                    )
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'bigmaps'-GT-'{}(
+                    /* Fl Fn D Sfa */ Var'Unds'37:SortMap{}
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'script'-GT-'{}(
+                    /* Fl Fn D Sfa */ Var'Unds'38:SortPreData{}
+                ),
+                /* Fl Fn D Sfa Cl */
+                Lbl'-LT-'k'-GT-'{}(/* Fl Fn D Sfa Cl */ dotk{}()),
+                /* Fl Fn D Sfc */
+                Lbl'-LT-'stack'-GT-'{}(
+                    /* Fl Fn D Sfc */
+                    /* Inj: */ inj{SortStack{}, SortInternalStack{}}(
+                        /* Fl Fn D Sfc */
+                        Lbl'UndsSClnUndsUnds'MICHELSON-COMMON'Unds'Stack'Unds'StackElement'Unds'Stack{}(
+                            /* Fl Fn D Sfc */
+                            Lbl'LSqBUndsUndsRSqBUnds'MICHELSON-COMMON'Unds'StackElement'Unds'TypeName'Unds'Data{}(
+                                /* Fl Fn D Sfa Cli */
+                                /* Inj: */ inj{SortNumTypeName{}, SortTypeName{}}(
+                                    /* Fl Fn D Sfa Cl */
+                                    Lblint'Unds'MICHELSON-COMMON-SYNTAX'Unds'NumTypeName{}()
+                                ),
+                                /* Fl Fn D Sfc */
+                                /* Inj: */ inj{SortInt{}, SortData{}}(
+                                    /* Fl Fn D Sfa */
+                                    Lbl'UndsPlus'Int'Unds'{}(
+                                        /* Fl Fn D Sfa */
+                                        Lblsize'LParUndsCommUndsRParUnds'MICHELSON-COMMON'Unds'Int'Unds'InternalList'Unds'Int{}(
+                                            /* Fl Fn D Sfa */
+                                            VarL:SortInternalList{},
+                                            /* Fl Fn D Sfa Cl */
+                                            /* builtin: */ \dv{SortInt{}}("0")
+                                        ),
+                                        /* Fl Fn D Sfa */
+                                        Lbl'UndsPlus'Int'Unds'{}(
+                                            /* Fl Fn D Sfa */ VarI:SortInt{},
+                                            /* Fl Fn D Sfa Cl */
+                                            /* builtin: */ \dv{SortInt{}}("1")
+                                        )
+                                    )
+                                )
+                            ),
+                            /* Fl Fn D Sfa Cl */
+                            Lbl'Stop'List'LBraQuotUndsSClnUndsUnds'MICHELSON-COMMON'Unds'Stack'Unds'StackElement'Unds'Stack'QuotRBraUnds'Stack{}()
+                        )
+                    )
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'inputstack'-GT-'{}(
+                    /* Fl Fn D Sfa */
+                    Lbl'LBraUndsRBraUnds'UNIT-TEST-COMMON-SYNTAX'Unds'LiteralStack'Unds'StackElementList{}(
+                        /* Fl Fn D Sfa */ Var'Unds'39:SortStackElementList{}
+                    )
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'expected'-GT-'{}(
+                    /* Fl Fn D Sfa */ Var'Unds'40:SortOutputStack{}
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'pre'-GT-'{}(
+                    /* Fl Fn D Sfa */ Var'Unds'41:SortBlockList{}
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'post'-GT-'{}(
+                    /* Fl Fn D Sfa */ Var'Unds'42:SortBlockList{}
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'invs'-GT-'{}(/* Fl Fn D Sfa */ Var'Unds'43:SortMap{}),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'symbols'-GT-'{}(
+                    /* Fl Fn D Sfa */ Var'Unds'44:SortMap{}
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'returncode'-GT-'{}(
+                    /* Fl Fn D Sfa */ Var'Unds'45:SortInt{}
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'assumeFailed'-GT-'{}(
+                    /* Fl Fn D Sfa */ Var'Unds'46:SortBool{}
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'-LT-'trace'-GT-'{}(/* Fl Fn D Sfa */ Var'Unds'47:SortK{})
+            ),
+            /* Fl Fn D Sfa */
+            Lbl'-LT-'generatedCounter'-GT-'{}(
+                /* Fl Fn D Sfa */ Var'Unds'DotVar1:SortInt{}
+            )
+        ),
+        /* Sfa */
+        \not{SortGeneratedTopCell{}}(
+            /* Sfa */
+            \equals{SortInt{}, SortGeneratedTopCell{}}(
+                /* Fl Fn D Sfa */
+                Lbl'UndsPlus'Int'Unds'{}(
+                    /* Fl Fn D Sfa */
+                    Lblsize'LParUndsCommUndsRParUnds'MICHELSON-COMMON'Unds'Int'Unds'InternalList'Unds'Int{}(
+                        /* Fl Fn D Sfa */ VarL:SortInternalList{},
+                        /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("0")
+                    ),
+                    /* Fl Fn D Sfa */
+                    Lbl'UndsPlus'Int'Unds'{}(
+                        /* Fl Fn D Sfa */ VarI:SortInt{},
+                        /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("1")
+                    )
+                ),
+                /* Fl Fn D Sfa */
+                Lbl'UndsPlus'Int'Unds'{}(
+                    /* Fl Fn D Sfa */
+                    Lblsize'LParUndsCommUndsRParUnds'MICHELSON-COMMON'Unds'Int'Unds'InternalList'Unds'Int{}(
+                        /* Fl Fn D Sfa */ VarL:SortInternalList{},
+                        /* Fl Fn D Sfa Cl */ /* builtin: */ \dv{SortInt{}}("1")
+                    ),
+                    /* Fl Fn D Sfa */ VarI:SortInt{}
+                )
+            )
+        )
+    ),
+    /* Spa */
+    \equals{SortInternalList{}, SortGeneratedTopCell{}}(
+        /* Fl Fn D Sfa */ VarIntList:SortInternalList{},
+        /* Fl Fn D Sfa */
+        Lbl'UndsSClnSClnUndsUnds'MICHELSON-COMMON'Unds'InternalList'Unds'WrappedData'Unds'InternalList{}(
+            /* Fl Fn D Sfa */
+            Lbl'LSqBUndsRSqBUnds'MICHELSON-COMMON'Unds'WrappedData'Unds'Data{}(
+                /* Fl Fn D Sfa */ VarE:SortData{}
+            ),
+            /* Fl Fn D Sfa */ VarL:SortInternalList{}
+        )
+    )
+)