MrChico
MrChico
/ supposedToBeFlattened.json
Created
February 25, 2019 12:58
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| { | |
| "node": "KApply", | |
| "label": "<storage>", | |
| "variable": false, | |
| "arity": 1, | |
| "args": [ | |
| { | |
| "node": "KApply", | |
| "label": "_Map_", | |
| "variable": false, |
MrChico
/ safeadd_fail first time
Created
February 24, 2019 19:26
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| requires "../rules.k" | |
| module SAFEADD_ADD_FAIL | |
| imports ETHEREUM-SIMULATION | |
| imports EVM | |
| imports RULES | |
| // SafeAdd_add | |
| rule | |
| <k> #execute ~> CONTINUATION => #halt ~> CONTINUATION </k> |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| requires "domains.k" | |
| requires "edsl.k" | |
| requires "evm.k" | |
| module RULES | |
| imports EVM | |
| imports EDSL | |
| // VERIFICATION.k |
MrChico
/ gist:93726011057c215beca321210e93e5d1
Created
February 18, 2019 22:31
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| requires "../rules.k" | |
| module TOKEN_TRANSFER_PASS_ROUGH | |
| imports ETHEREUM-SIMULATION | |
| imports EVM | |
| imports RULES | |
| // Token_transfer | |
| rule | |
| <k> #execute ~> CONTINUATION => #halt ~> CONTINUATION </k> |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (set-option :auto-config false) | |
| (set-option :smt.mbqi false) | |
| ;(set-option :smt.mbqi.max_iterations 15) | |
| ;; pow256 and pow255 | |
| (define-fun pow256 () Int | |
| 115792089237316195423570985008687907853269984665640564039457584007913129639936) | |
| (define-fun pow255 () Int | |
| 57896044618658097711785492504343953926634992332820282019728792003956564819968) | |
| ;; weird declaration trick (doesn't seem to be needed currently) |
MrChico
/ Uint.callIt
Created
February 13, 2019 12:54
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| requires "../rules.k" | |
| module UINT_CALLIT_PASS_ROUGH | |
| imports ETHEREUM-SIMULATION | |
| imports EVM | |
| imports RULES | |
| // Uint_callIt | |
| rule | |
| <k> #execute ~> CONTINUATION => #halt ~> CONTINUATION </k> |
MrChico
/ gist:86d40e111c52e790bc4b8ca329df8c2e
Created
December 19, 2018 21:37
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| requires "../rules.k" | |
| module CALLEE_TEMPDELTA_PASS_ROUGH | |
| imports ETHEREUM-SIMULATION | |
| imports EVM | |
| imports RULES | |
| // Callee_tempDelta | |
| rule | |
| <k> #execute ~> CONTINUATION => #halt ~> CONTINUATION </k> |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (set-option :auto-config false) | |
| (set-option :smt.mbqi false) | |
| ;(set-option :smt.mbqi.max_iterations 15) | |
| ;; pow256 and pow255 | |
| (define-fun pow256 () Int | |
| 115792089237316195423570985008687907853269984665640564039457584007913129639936) | |
| (define-fun pow255 () Int | |
| 57896044618658097711785492504343953926634992332820282019728792003956564819968) | |
| ;; weird declaration trick (doesn't seem to be needed currently) |
MrChico
/ gist:3277d21600894dba44cd2c0a94864533
Created
December 14, 2018 17:19
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ehildenb 5:08 PM | |
| WRT: https://github.com/kframework/k/pull/208#issuecomment-447368596 | |
| github.com | |
| add IMAP builtin module by daejunpark · Pull Request #208 · kframework/k | |
| This is an algebraic map theory that allows the symbolic map reasoning in the K level. Currently, it is a monomorphic, and here IMAP is a map from Int to Int. But it is quite sufficient for many lo... | |
| Doesn't the spec still make sense with `K0 == K1` or with `K0 =/= K1`? In either case, the final value of `V1 + V2`, regardless of what everything underneath the outer `store` is. | |
| The extra side condition will prevent normalization, not enable more normalization. | |
| mrchico 5:10 PM |
MrChico
/ token_example.k
Created
December 14, 2018 16:35
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| requires "../rules.k" | |
| module TOKEN_TRANSFER_PASS_ROUGH | |
| imports ETHEREUM-SIMULATION | |
| imports EVM | |
| imports RULES | |
| // Token_transfer | |
| rule | |
| <k> #execute ~> CONTINUATION => #halt ~> CONTINUATION </k> |