certusone
/
wormhole
mirror of https://github.com/certusone/wormhole.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
wormhole/ethereum/wormhole-lemmas.k

241 lines
10 KiB
Plaintext
Raw Permalink Blame History

requires "evm.md"
requires "foundry.md"
module WORMHOLE-LEMMAS
imports FOUNDRY
imports INFINITE-GAS
imports SET-SYMBOLIC
syntax StepSort ::= Int
| Bool
| Bytes
| Set
// ------------------------
syntax KItem ::= runLemma ( StepSort )
| doneLemma( StepSort )
// --------------------------------------
syntax Int ::= "notMaxUInt8" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF00 */
| "notMaxUInt16" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF0000 */
| "notMaxUInt32" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF00000000 */
| "notMaxUInt64" [alias] /* FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF0000000000000000 */
| "notMaxUInt240" [alias] /* FFFF000000000000000000000000000000000000000000000000000000000000 */
| "notMaxUInt248" [alias] /* FF00000000000000000000000000000000000000000000000000000000000000 */
// ------------------------------------------------------------------------------------------------------------
rule notMaxUInt8 => 115792089237316195423570985008687907853269984665640564039457584007913129639680
rule notMaxUInt16 => 115792089237316195423570985008687907853269984665640564039457584007913129574400
rule notMaxUInt32 => 115792089237316195423570985008687907853269984665640564039457584007908834672640
rule notMaxUInt64 => 115792089237316195423570985008687907853269984665640564039439137263839420088320
rule notMaxUInt240 => 115790322390251417039241401711187164934754157181743688420499462401711837020160
rule notMaxUInt248 => 115339776388732929035197660848497720713218148788040405586178452820382218977280
rule <k> runLemma(T) => doneLemma(T) ... </k>
rule notMaxUInt248 &Int ( X <<Int 248 ) => X <<Int 248
requires #rangeUInt ( 8 , X )
[simplification]
rule notMaxUInt240 &Int ( X <<Int 240 ) => X <<Int 240
requires #rangeUInt ( 16 , X )
[simplification]
rule 4294901760 &Int ( X <<Int 16 ) => X <<Int 16
requires #rangeUInt ( 16 , X )
[simplification]
rule maxUInt16 &Int ( ( ( X *Int pow16 ) |Int ( 115792089237316195423570985008687907853269984665640564039457584007908834738175 &Int _ ) ) >>Int 16 ) => X
requires #rangeUInt ( 16 , X )
[simplification]
rule maxUInt16 &Int ( ( ( X <<Int 16 ) |Int ( 115792089237316195423570985008687907853269984665640564039457584007908834738175 &Int _ ) ) /Int pow16 ) => X
requires #rangeUInt ( 16 , X )
[simplification]
rule maxUInt8 &Int ( X |Int ( notMaxUInt8 &Int _ ) ) => X
requires #rangeUInt ( 8 , X )
[simplification]
rule maxUInt16 &Int ( X |Int ( notMaxUInt16 &Int _ ) ) => X
requires #rangeUInt ( 16 , X )
[simplification]
rule maxUInt32 &Int ( X |Int ( notMaxUInt32 &Int _ ) ) => X
requires #rangeUInt ( 32 , X )
[simplification]
rule maxUInt64 &Int ( X |Int ( notMaxUInt64 &Int _ ) ) => X
requires #rangeUInt ( 64 , X )
[simplification]
rule notMaxUInt16 &Int X => 0
requires #rangeUInt ( 16 , X )
[simplification]
rule notMaxUInt32 &Int X => 0
requires #rangeUInt ( 32 , X )
[simplification]
rule notMaxUInt64 &Int X => 0
requires #rangeUInt ( 64 , X )
[simplification]
rule maxUInt32 &Int X => X
requires #rangeUInt ( 32 , X )
[simplification]
rule #lookup ( MAP [ KEY1 <- _ ] , KEY2 ) => #lookup ( MAP , KEY2 )
requires KEY1 =/=Int KEY2
[simplification]
rule chop ( I:Int ) => I modInt pow256 [simplification, smt-lemma]
rule A &Int B => B &Int A
[symbolic(A), concrete(B), simplification]
// Not being able to generalize this for some reason
rule (X <<Int 248) <Int pow256 => true
requires #rangeUInt ( 8 , X )
[simplification]
rule (X <<Int 240) <Int pow256 => true
requires #rangeUInt ( 16 , X )
[simplification]
rule (X <<Int 16) <Int pow256 => true
requires #rangeUInt ( 240 , X )
[simplification]
rule 0 <=Int (X <<Int Y) => true
requires 0 <=Int X andBool 0 <=Int Y
[simplification]
rule ( ( X modInt N ) +Int Y ) modInt N => (X +Int Y) modInt N
[simplification]
rule X xorInt maxUInt256 => maxUInt256 -Int X
requires #rangeUInt ( 256 , X )
[simplification]
rule X <=Int 115792089237316195423570985008687907853269984665640564039457584007913129639934 => X =/=Int maxUInt256
requires #rangeUInt ( 256 , X )
[simplification]
rule keccak ( _ ) ==Int maxUInt256 => false
[simplification]
rule 1 |Int _ ==Int 0 => false
[simplification]
rule (A |Int B) ==Int (B |Int A) => true
[simplification, smt-lemma]
rule maxUInt8 &Int #asWord ( X ) => #asWord ( #range ( X , 31 , 1 ) )
requires lengthBytes ( X ) ==Int 32
[simplification]
rule maxUInt16 &Int #asWord ( X ) => #asWord ( #range ( X , 30 , 2 ) )
requires lengthBytes ( X ) ==Int 32
[simplification]
rule #buf ( 32 , #asWord ( X ) ) => X
requires lengthBytes ( X ) ==Int 32
[simplification]
rule #buf ( 32 , X <<Int 248 ) => #buf ( 1 , X ) +Bytes #buf ( 31 , 0 )
requires #rangeUInt ( 8 , X )
[simplification]
rule #buf ( 32 , X <<Int 240 ) => #buf ( 2 , X ) +Bytes #buf ( 30 , 0 )
requires #rangeUInt ( 16 , X )
[simplification]
rule #range ( X , S1 , W1 ) +Bytes #range ( X , S2 , W2 ) => #range ( X , S1 , W1 +Int W2 )
requires S1 +Int W1 ==Int S2
andBool S2 +Int W2 <=Int lengthBytes ( X )
[simplification]
rule ( X <<Int 16 ) ==Int ( X *Int pow16 ) => true
requires 0 <=Int X
[simplification, smt-lemma]
endmodule
module WORMHOLE-LEMMAS-SPEC
imports WORMHOLE-LEMMAS
claim [lowest-32-bits]: <k> runLemma ( VV0_index_114b9705:Int ==Int ( maxUInt32 &Int ( VV0_index_114b9705:Int |Int ( notMaxUInt32 &Int #lookup ( _STORAGE:Map , 11 ) ) ) ) )
=> doneLemma ( true ) ... </k>
requires #rangeUInt ( 32 , VV0_index_114b9705 )
claim [chop-successor-key]: <k> runLemma ( #lookup ( STORAGE [ chop ( KEY +Int 1 ) <- _ ] , KEY ) )
=> doneLemma ( #lookup ( STORAGE , KEY ) ) ... </k>
claim [chop-successor]: <k> runLemma ( chop ( KEY +Int 1 ) =/=Int KEY )
=> doneLemma ( true ) ... </k>
claim [bits-16-to-31]: <k> runLemma ( ( 65535 &Int ( ( ( ( ( VV0_newChainId_114b9705:Int <<Int 16 ) modInt 115792089237316195423570985008687907853269984665640564039457584007913129639936 ) &Int 4294901760 ) /Int 65536 ) &Int 65535 ) ) ==Int VV0_newChainId_114b9705:Int )
=> doneLemma ( true ) ... </k>
requires #rangeUInt ( 16 , VV0_newChainId_114b9705 )
claim [bits-16-to-31-2]: <k> runLemma ( ( maxUInt16 &Int ( ( ( 4294901760 &Int ( VV0_newChainId_114b9705:Int <<Int 16 ) ) |Int ( 115792089237316195423570985008687907853269984665640564039457584007908834738175 &Int #lookup ( _STORAGE:Map , 8 ) ) ) /Int pow16 ) ) ==Int VV0_newChainId_114b9705:Int ) => doneLemma ( true ) ... </k>
requires #rangeUInt ( 16 , VV0_newChainId_114b9705 )
claim [bits-16-to-31-3]: <k> runLemma ( maxUInt16 &Int ( ( ( ( ( X <<Int 16 ) modInt pow256 ) &Int 4294901760 ) /Int pow16 ) &Int maxUInt16 ) ) => doneLemma ( X ) ... </k>
requires #rangeUInt ( 16 , X )
claim [bits-16-to-31-4]: <k> runLemma ( ( X *Int pow16 ) |Int Y ==Int ( ( ( ( X <<Int 16 ) modInt pow256 ) &Int 4294901760 ) |Int Y ) ) => doneLemma ( true ) ... </k>
requires #rangeUInt ( 16 , X )
claim [bits-16-to-31-5]: <k> runLemma ( ( ( X *Int pow16 ) |Int ( 115792089237316195423570985008687907853269984665640564039457584007908834738175 &Int Y ) ) ==Int ( ( 115792089237316195423570985008687907853269984665640564039457584007908834738175 &Int Y ) |Int ( 4294901760 &Int ( ( X <<Int 16 ) modInt pow256 ) ) ) ) => doneLemma ( true ) ... </k>
requires #rangeUInt ( 16 , X )
andBool #rangeUInt ( 256 , Y )
claim [shift-mask]: <k> runLemma ( ( ( VV0_newChainId_114b9705:Int *Int pow16 ) |Int Y ==Int ( ( ( ( VV0_newChainId_114b9705:Int <<Int 16 ) modInt pow256 ) &Int 4294901760 ) |Int Y ) ) )
=> doneLemma ( true ) ... </k>
requires #rangeUInt ( 16 , VV0_newChainId_114b9705 )
claim [shift-range]: <k> runLemma ( #rangeUInt ( 256 , X <<Int 16 ) ) => doneLemma ( true ) ... </k>
requires #rangeUInt ( 16 , X )
claim [shift-mod]: <k> runLemma ( ( X <<Int 16 ) modInt pow256 ) => doneLemma ( X <<Int 16 ) ... </k>
requires #rangeUInt ( 16 , X )
claim [lowest-8-bits]: <k> runLemma ( maxUInt8 &Int #asWord ( #range ( #buf ( 32 , X ) , 1 , 31 ) +Bytes #range ( #buf ( 32 , #asWord ( b"\x01" +Bytes #range ( #buf ( 32 , Y ) , 0 , 2 ) +Bytes #range ( #buf ( 32 , Z ) , 0 , 29 ) ) ) , 0 , 1 ) ) )
=> doneLemma ( 1 ) ... </k>
requires #rangeUInt ( 256 , X )
andBool #rangeUInt ( 256 , Y )
andBool #rangeUInt ( 256 , Z )
claim [highest-8-bits]: <k> runLemma ( maxUInt8 &Int #asWord ( #range ( #buf ( 32 , ( notMaxUInt248 &Int ( ( X <<Int 248 ) modInt pow256 ) ) ) , 0 , 1 ) ) )
=> doneLemma ( X ) ... </k>
requires #rangeUInt ( 8 , X )
claim [highest-16-bits]: <k> runLemma ( maxUInt16 &Int #asWord ( #range ( #buf ( 32 , X ) , 3 , 29 ) +Bytes b"\x01" +Bytes #range ( #buf ( 32 , ( notMaxUInt240 &Int ( ( Y <<Int 240 ) modInt pow256 ) ) ) , 0 , 2 ) ) )
=> doneLemma ( Y ) ... </k>
requires #rangeUInt ( 256 , X )
andBool #rangeUInt ( 16 , Y )
claim [one-byte-range]: <k> runLemma ( #asWord ( #range ( #buf ( 32 , notMaxUInt248 &Int ( X <<Int 248 ) modInt pow256 ) , 0 , 1 ) ) <Int pow8 )
=> doneLemma ( true ) ... </k>
requires #rangeUInt ( 8 , X )
claim [shift-248]: <k> runLemma ( ( X <<Int 248 ) <Int pow256 )
=> doneLemma ( true ) ... </k>
requires #rangeUInt ( 8 , X )
claim [length-concat]: <k> runLemma ( lengthBytes ( #range ( #buf ( 32 , _X ) , 3 , 29 ) +Bytes b"\x01" +Bytes #buf ( 2 , Y ) ) )
=> doneLemma ( 32 ) ... </k>
requires #rangeUInt ( 16 , Y )
claim [concat-ranges]: <k> runLemma ( #asWord ( #range ( #buf ( 32 , X ) , 0 , 29 ) +Bytes #range ( #buf ( 32 , X ) , 29 , 3 ) ) )
=> doneLemma ( X ) ... </k>
requires #rangeUInt ( 256 , X )
endmodule
Reference in New Issue View Git Blame Copy Permalink