I hereby claim:
- I am livnev on github.
- I am livnev (https://keybase.io/livnev) on keybase.
- I have a public key ASChcdP5lQhsrdgdcIu880EEPsZ2Td3LuBDP0gqUEu4pggo
To claim this, I am signing this object:
I hereby claim:
To claim this, I am signing this object:
behaviour | |
HEAD DELTAC | |
├ 0 ¬( 0 < ABI_dink ) | |
│ ├ 0 ¬( ABI_dink < 0 ) |
behaviour | |
HEAD DELTAC | |
├ 0 ╭ Can == 1 | |
│ │ │ ¬( ( 0 <= Rate + ABI_rate andBool Rate + ABI_rate <= 11579208923731619542357098500868790785326998466 |
behaviour | |
HEAD DELTAC | |
├ 0 ¬( 0 < ABI_dink ) | |
│ ├ 0 ¬( ABI_dink < 0 ) |
aimed at tune.sol.json | |
behaviour | |
HEAD DELTAC | |
├ 0 ¬( 0 < ABI_dink ) | |
│ ├ 0 ¬( ABI_dink < 0 ) |
requires "edsl.k" | |
requires "evm.k" | |
module RULES | |
imports EVM | |
imports EDSL | |
// VERIFICATION.k | |
syntax Int ::= nthbyteof ( Int , Int , Int ) [function, smtlib(smt_nthbyteof)] |
module Main where | |
import System.Environment | |
import Distribution.Simple.Utils (lowercase) | |
import qualified Data.Map.Strict as Map | |
import Data.List (intersperse, elem) | |
import Text.Read (readMaybe) | |
answer2Bool :: String -> Maybe Bool | |
answer2Bool "y" = Just True | |
answer2Bool "yes" = Just True |
nixpkgs.overlays = [ (self: super: { | |
mu = with self; stdenv.lib.overrideDerivation | |
(super.mu.override { gmime = gmime3; }) (attrs: rec { | |
src = super.fetchFromGitHub { | |
owner = "djcb"; | |
repo = "mu"; | |
rev = "53c1b0a06956a151b9176cb8cce26261c1420c76"; | |
sha256 = "02x7fqv3xdjsw44ks5z1z764hpsx645gjljh824cbvf6macksilj"; | |
}; | |
}); |
requires "../rules.k" | |
module CALLEE_TEMPDELTA_FAIL | |
imports ETHEREUM-SIMULATION | |
imports EVM | |
imports RULES | |
// Callee_tempDelta | |
rule | |
<k> #execute ~> CONTINUATION => #halt ~> CONTINUATION </k> |
{"node":"KApply","label":"#if_#then_#else_#fi_K-EQUAL","variable":false,"arity":3,"args":[{"node":"KToken","sort":"K","token":"VGas >=Int 0 ==K true"},{"node":"KApply","label":"#if_#then_#else_#fi_K-EQUAL","variable":false,"arity":3,"args":[{"node":"KToken","sort":"K","token":"VGas >=Int 3 ==K true"},{"node":"KApply","label":"#if_#then_#else_#fi_K-EQUAL","variable":false,"arity":3,"args":[{"node":"KToken","sort":"K","token":"VGas -Int 3 >=Int 3 ==K true"},{"node":"KApply","label":"#if_#then_#else_#fi_K-EQUAL","variable":false,"arity":3,"args":[{"node":"KToken","sort":"K","token":"VGas -Int 6 >=Int 9 ==K true"},{"node":"KApply","label":"#if_#then_#else_#fi_K-EQUAL","variable":false,"arity":3,"args":[{"node":"KToken","sort":"K","token":"VGas -Int 15 >=Int 3 ==K true"},{"node":"KApply","label":"#if_#then_#else_#fi_K-EQUAL","variable":false,"arity":3,"args":[{"node":"KToken","sort":"K","token":"VGas -Int 18 >=Int 3 ==K true"},{"node":"KApply","label":"#if_#then_#else_#fi_K-EQUAL","variable":false,"arity":3,"args" |