MrChico

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; SBV: Starting at 2021-01-18 16:51:54.626121 CET
;;;
;;;           Solver    : CVC4
;;;           Executable: /nix/store/4vm8vn16cjf0pxfm2j0g6kqi3a7vyn3m-cvc4-1.8-prerelease/bin/cvc4
;;;           Options   : --lang=smt --incremental --interactive --no-interactive-prompt --model-witness-value --tlimit-per=30000
;;;
;;; This file is an auto-generated loadable SMT-Lib file.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

MrChico

;; overflow checking words vs. checking explicit bounds
;; x * y / y == x     <==>
;; x * y does not overflow


;; max value of (_ BitVec 256)
(define-fun pow256 () Int
  115792089237316195423570985008687907853269984665640564039457584007913129639936)

;; x * y / y == x

MrChico

time hevm symbolic --code $(<noidea.bin-runtime) --solver cvc4 --get-models
checking postcondition...
Q.E.D.
Explored: 53 branches without assertion violations
However, 2 branch(es) errored while exploring:
["Unexpected symbolic argument at opcode: OpExtcodesize. Not supported (yet!)","Unexpected symbolic argument at opcode: OpCalldatacopy. Not supported (yet!)"]
-- Branch (1/53) --
Calldata:
0x06973ccf
Caller:

MrChico

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; SBV: Starting at 2020-06-02 17:05:41.766748 CEST
;;;
;;;           Solver    : Z3
;;;           Executable: /nix/store/ac646i28c44y2s3p5wy0zlhrlcx0x039-z3-4.8.5/bin/z3
;;;           Options   : -nw -in -smt2
;;;
;;; This file is an auto-generated loadable SMT-Lib file.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

MrChico

pragma solidity ^0.6.0;

import "../deposit_contract.sol";

contract DepositContractFactory {
  bool public deployed;
  uint public deploymentTime;
  DepositContract depositContract;

  constructor(uint _deploymentTime) public {

MrChico

;; Proof of concept implementation of a simple stack machine
;; implementing PUSH1, ADD and STOP using the smt 
;; It reads a "codestring", which is translated to opcodes according
;; to the following table:
;; 0 -> STOP
;; 1 -> PUSH1
;; 2 -> ADD
;;
;; It does not deal with integer overflow or with stack overflow
;; but it does handle stack underflow.

MrChico

-- data types for the parsed syntax.
-- Has the correct basic structure, but doesn't necessarily type check
-- It is also equipped with position information for extra debugging xp

module RawAst where

newtype Id = Id String
  deriving (Eq, Ord, Show, Read)

data Act = Main [RawBehaviour]

MrChico

behaviour mint of UniswapV2Exchange
interface mint(address to)

for all

    LockState : bool

    Token0 : address UniswapV2Exchange
    Token1 : address UniswapV2Exchange

MrChico

behaviour init of Token
interface constructor(string _symbol, string _name, string _version, uint _totalSupply)

creates Token
    string name         := _name
    string symbol       := _symbol
    uint256 totalSupply := _totalSupply

    mapping(address => uint) balanceOf :=  [CALLER := _totalSupply]
    mapping(address=>mapping(address=>uint)) allowance := []

MrChico

boot.loader.efi.canTouchEfiVariables = true;
  boot.loader.efi.efiSysMountPoint = "/boot/efi";
  boot.loader.grub = {
    enable = true;
    device = "nodev";
    version = 2;
    efiSupport = true;
    enableCryptodisk = true;
    extraInitrd = /boot/initrd.keys.gz;
  };