livnev

## keybase.md

      
              1 file
            
          
              0 forks
            
          
              0 comments
            
          
              0 stars
            
          
                livnev
                / keybase.md
            
            
              Created
              February 6, 2016 19:29
            
              
                Keybase Proof
              
          
    Keybase proof

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:

  
## tune-fail-tree
behaviour
  HEAD                        DELTAC

  ├ 0                         ¬( 0 < ABI_dink )
  │ ├ 0                       ¬( ABI_dink < 0 )

## fold_fail
behaviour
  HEAD                DELTAC

  ├ 0                 ╭ Can == 1
  │ │                 │ ¬( ( 0 <= Rate + ABI_rate andBool Rate + ABI_rate <= 11579208923731619542357098500868790785326998466

## Vat_tune_succ.out
behaviour
  HEAD            DELTAC

  ├ 0             ¬( 0 < ABI_dink )
  │ ├ 0           ¬( ABI_dink < 0 )

## Vat_grab_succ.out
aimed at tune.sol.json

behaviour
  HEAD            DELTAC

  ├ 0             ¬( 0 < ABI_dink )
  │ ├ 0           ¬( ABI_dink < 0 )

## rules.k
requires "edsl.k"
requires "evm.k"

module RULES
    imports EVM
    imports EDSL

// VERIFICATION.k

    syntax Int ::= nthbyteof ( Int , Int , Int ) [function, smtlib(smt_nthbyteof)]

## tictactoe.hs
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

## mu-overlay
  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";
      };
    });

## Callee_tempDelta_fail.k
requires "../rules.k"

module CALLEE_TEMPDELTA_FAIL
  imports ETHEREUM-SIMULATION
  imports EVM
  imports RULES

// Callee_tempDelta
rule
  <k> #execute ~> CONTINUATION => #halt ~> CONTINUATION </k>

## Callee_tempDelta_fail.raw.kast.json
{"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"
	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
	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>