MrChico

import "./RLP.sol";
import "./RLPW.sol";

library Lambda {
    using RLP for bytes;
    using RLP for RLP.RLPItem;
    using RLP for RLP.Iterator;
    /*  Takes an annotated ast as input, and returns a fully reduced ast
        Each node in the ast one of the three following formats:
        [1, function, argument] - Application

MrChico

Keybase proof

I hereby claim:

• I am mrchico on github.
• I am mr_chico (https://keybase.io/mr_chico) on keybase.
• I have a public key ASDBM_MHuVu3S0Bbs8758xObWX0WFQrkuml92a4AOoBvnQo

To claim this, I am signing this object:

MrChico

requires "abstract-semantics.k"
requires "verification.k"

module PROOF-SPEC
  imports ETHEREUM-SIMULATION
  imports ABSTRACT-SEMANTICS
  imports VERIFICATION

  // rmul
  rule

MrChico

requires "abstract-semantics.k"
requires "verification.k"

module PROOF-SPEC
  imports ETHEREUM-SIMULATION
  imports ABSTRACT-SEMANTICS
  imports VERIFICATION

  // updateVal
  rule

MrChico

{
    "format":"KAST",
    "version":1,
    "term":{
        "node":"KApply",
        "label":"<generatedTop>",
        "variable":false,
        "arity":6,
        "args":[

MrChico

const fs = require("fs");

let pre = "/private/var/folders/fb/0m3l_cnn4w57fhsv7q_lx5780000gn/T/klab/cfb53897/nodes/1103642064.json"
let post = "/private/var/folders/fb/0m3l_cnn4w57fhsv7q_lx5780000gn/T/klab/cfb53897/nodes/563029515.json"


const getTerm = nodePath => {
    let read = fs.readFileSync(nodePath).toString()
    return JSON.parse(read).term
}

MrChico

(set-option :auto-config false)
(set-option :smt.mbqi false)
;(set-option :smt.mbqi.max_iterations 15)

(declare-fun pow256 () Int)
(assert (= pow256 115792089237316195423570985008687907853269984665640564039457584007913129639936))
; (assert (>= pow256 115792089237316195423570985008687907853269984665640564039457584007913129639936))
; (assert (<= pow256 115792089237316195423570985008687907853269984665640564039457584007913129639936))

;

MrChico

Contracts

• Vat
  • Heal
• Vow
  • Heal

Vat

Description and comments go here. All headings as below can be referenced. manipulating bad debt and surplus

MrChico

requires "../rules.k"

module PROOF-VOW_HEAL_SUCC
  imports ETHEREUM-SIMULATION
  imports EVM
  imports RULES

// heal-success of Vow
rule
  <k> #execute => #halt </k>

MrChico

requires "../rules.k"

module PROOF-EASYNEST_CALLING_SUCC
  imports ETHEREUM-SIMULATION
  imports EVM
  imports RULES

// NaN_calling
rule
  <k> #execute ~> _ => #halt ~> _ </k>