Skip to content

Commit 8ddc349

Browse files
RaoulSchaffranekRaoulSchaffranek
committed
Remove manual selector rules
1 parent 273ae8f commit 8ddc349

3 files changed

Lines changed: 2 additions & 272 deletions

File tree

‎tests/specs/examples/erc20-bin-runtime.k‎

Lines changed: 0 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -102,33 +102,6 @@ module ERC20-CONTRACT
102102
andBool ( #rangeUInt ( 256 , V2_amount )
103103
)))
104104

105-
106-
rule ( selector ( "allowance(address,address)" ) => 3714247998 )
107-
108-
109-
rule ( selector ( "approve(address,uint256)" ) => 157198259 )
110-
111-
112-
rule ( selector ( "balanceOf(address)" ) => 1889567281 )
113-
114-
115-
rule ( selector ( "decimals()" ) => 826074471 )
116-
117-
118-
rule ( selector ( "name()" ) => 117300739 )
119-
120-
121-
rule ( selector ( "symbol()" ) => 2514000705 )
122-
123-
124-
rule ( selector ( "totalSupply()" ) => 404098525 )
125-
126-
127-
rule ( selector ( "transfer(address,uint256)" ) => 2835717307 )
128-
129-
130-
rule ( selector ( "transferFrom(address,address,uint256)" ) => 599290589 )
131-
132105

133106
endmodule
134107

‎tests/specs/examples/erc721-bin-runtime.k‎

Lines changed: 1 addition & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -134,46 +134,7 @@ module ERC721-CONTRACT
134134
andBool ( #rangeAddress ( V1_to )
135135
andBool ( #rangeUInt ( 256 , V2_tokenId )
136136
)))
137-
138-
139-
rule ( selector ( "approve(address,uint256)" ) => 157198259 )
140-
141-
142-
rule ( selector ( "balanceOf(address)" ) => 1889567281 )
143-
144-
145-
rule ( selector ( "getApproved(uint256)" ) => 135795452 )
146-
147-
148-
rule ( selector ( "isApprovedForAll(address,address)" ) => 3917867461 )
149-
150-
151-
rule ( selector ( "name()" ) => 117300739 )
152-
153-
154-
rule ( selector ( "ownerOf(uint256)" ) => 1666326814 )
155-
156-
157-
rule ( selector ( "safeTransferFrom(address,address,uint256)" ) => 1115958798 )
158-
159-
160-
rule ( selector ( "safeTransferFrom(address,address,uint256,bytes)" ) => 3096268766 )
161-
162-
163-
rule ( selector ( "setApprovalForAll(address,bool)" ) => 2720838757 )
164-
165-
166-
rule ( selector ( "supportsInterface(bytes4)" ) => 33540519 )
167-
168-
169-
rule ( selector ( "symbol()" ) => 2514000705 )
170-
171-
172-
rule ( selector ( "tokenURI(uint256)" ) => 3363526365 )
173-
174-
175-
rule ( selector ( "transferFrom(address,address,uint256)" ) => 599290589 )
176-
137+
177138

178139
endmodule
179140

‎tests/specs/examples/storage-bin-runtime.k‎

Lines changed: 1 addition & 205 deletions
Original file line numberDiff line numberDiff line change
@@ -708,211 +708,7 @@ module Storage-CONTRACT
708708

709709
rule ( S2KStorage . S2KsetMyBool ( V0_newBool : bool ) => #abiCallData ( "setMyBool" , #bool ( V0_newBool ) , .TypedArgs ) )
710710
ensures #rangeBool ( V0_newBool )
711-
712-
713-
rule ( selector ( "myBool()" ) => 1844366782 )
714-
715-
716-
rule ( selector ( "myBytes()" ) => 1898923522 )
717-
718-
719-
rule ( selector ( "myInt104()" ) => 3769717327 )
720-
721-
722-
rule ( selector ( "myInt112()" ) => 1361874479 )
723-
724-
725-
rule ( selector ( "myInt120()" ) => 2449055983 )
726-
727-
728-
rule ( selector ( "myInt128()" ) => 1171335287 )
729-
730-
731-
rule ( selector ( "myInt136()" ) => 1921575036 )
732-
733-
734-
rule ( selector ( "myInt144()" ) => 3031097123 )
735-
736-
737-
rule ( selector ( "myInt152()" ) => 2183556540 )
738-
739-
740-
rule ( selector ( "myInt16()" ) => 1716680015 )
741-
742-
743-
rule ( selector ( "myInt160()" ) => 2880209597 )
744-
745-
746-
rule ( selector ( "myInt168()" ) => 64341664 )
747-
748-
749-
rule ( selector ( "myInt176()" ) => 2473962370 )
750-
751-
752-
rule ( selector ( "myInt184()" ) => 933893415 )
753-
754-
755-
rule ( selector ( "myInt192()" ) => 3902309668 )
756-
757-
758-
rule ( selector ( "myInt200()" ) => 2002425666 )
759-
760-
761-
rule ( selector ( "myInt208()" ) => 103289144 )
762-
763-
764-
rule ( selector ( "myInt216()" ) => 4128675402 )
765-
766-
767-
rule ( selector ( "myInt224()" ) => 1054187961 )
768-
769-
770-
rule ( selector ( "myInt232()" ) => 1299236373 )
771-
772-
773-
rule ( selector ( "myInt24()" ) => 180311096 )
774-
775-
776-
rule ( selector ( "myInt240()" ) => 193999351 )
777-
778-
779-
rule ( selector ( "myInt248()" ) => 1172761411 )
780-
781-
782-
rule ( selector ( "myInt256()" ) => 930181817 )
783-
784-
785-
rule ( selector ( "myInt32()" ) => 652237467 )
786-
787-
788-
rule ( selector ( "myInt40()" ) => 2688242429 )
789-
790-
791-
rule ( selector ( "myInt48()" ) => 294352996 )
792-
793-
794-
rule ( selector ( "myInt56()" ) => 1426573562 )
795-
796-
797-
rule ( selector ( "myInt64()" ) => 1826080093 )
798-
799-
800-
rule ( selector ( "myInt72()" ) => 1358599558 )
801-
802-
803-
rule ( selector ( "myInt8()" ) => 1855112094 )
804-
805-
806-
rule ( selector ( "myInt80()" ) => 2607424367 )
807-
808-
809-
rule ( selector ( "myInt88()" ) => 4237602313 )
810-
811-
812-
rule ( selector ( "myInt96()" ) => 1140454608 )
813-
814-
815-
rule ( selector ( "myString()" ) => 1227618840 )
816-
817-
818-
rule ( selector ( "myUint104()" ) => 2562905582 )
819-
820-
821-
rule ( selector ( "myUint112()" ) => 2312572821 )
822-
823-
824-
rule ( selector ( "myUint120()" ) => 3068336510 )
825-
826-
827-
rule ( selector ( "myUint128()" ) => 2127339145 )
828-
829-
830-
rule ( selector ( "myUint136()" ) => 4173203025 )
831-
832-
833-
rule ( selector ( "myUint144()" ) => 4035797251 )
834-
835-
836-
rule ( selector ( "myUint152()" ) => 360190854 )
837-
838-
839-
rule ( selector ( "myUint16()" ) => 2385363659 )
840-
841-
842-
rule ( selector ( "myUint160()" ) => 1383333939 )
843-
844-
845-
rule ( selector ( "myUint168()" ) => 1009580974 )
846-
847-
848-
rule ( selector ( "myUint176()" ) => 2404840593 )
849-
850-
851-
rule ( selector ( "myUint184()" ) => 407000813 )
852-
853-
854-
rule ( selector ( "myUint192()" ) => 229692326 )
855-
856-
857-
rule ( selector ( "myUint200()" ) => 161744886 )
858-
859-
860-
rule ( selector ( "myUint208()" ) => 3633238487 )
861-
862-
863-
rule ( selector ( "myUint216()" ) => 3288289344 )
864-
865-
866-
rule ( selector ( "myUint224()" ) => 1934302803 )
867-
868-
869-
rule ( selector ( "myUint232()" ) => 2569544816 )
870-
871-
872-
rule ( selector ( "myUint24()" ) => 946970341 )
873-
874-
875-
rule ( selector ( "myUint240()" ) => 2223697895 )
876-
877-
878-
rule ( selector ( "myUint248()" ) => 1057386179 )
879-
880-
881-
rule ( selector ( "myUint256()" ) => 2816200220 )
882-
883-
884-
rule ( selector ( "myUint32()" ) => 302881183 )
885-
886-
887-
rule ( selector ( "myUint40()" ) => 2133099158 )
888-
889-
890-
rule ( selector ( "myUint48()" ) => 2035097050 )
891-
892-
893-
rule ( selector ( "myUint56()" ) => 3099541938 )
894-
895-
896-
rule ( selector ( "myUint64()" ) => 1056558741 )
897-
898-
899-
rule ( selector ( "myUint72()" ) => 329837525 )
900-
901-
902-
rule ( selector ( "myUint8()" ) => 3802444463 )
903-
904-
905-
rule ( selector ( "myUint80()" ) => 2279010072 )
906-
907-
908-
rule ( selector ( "myUint88()" ) => 101404465 )
909-
910-
911-
rule ( selector ( "myUint96()" ) => 2823172538 )
912-
913-
914-
rule ( selector ( "setMyBool(bool)" ) => 3944427737 )
915-
711+
916712

917713
endmodule
918714

0 commit comments

Comments
 (0)