Skip to content

Latest commit

 

History

History
52 lines (35 loc) · 1.32 KB

README.md

File metadata and controls

52 lines (35 loc) · 1.32 KB
Raw

This repository contains the supplementary code to this blog post.

hevm

BYTECODE=$(jq .deployedBytecode.object -r out/GaussSpec.sol/GaussSpec.json)
hevm symbolic --sig "check_equivalence(uint256)" --code $BYTECODE
BYTECODE=$(jq .deployedBytecode.object -r out/GaussSpec.sol/GaussSpec.json)
hevm symbolic --sig "check_sumToN_success(uint256)" --code $BYTECODE --assertions '[0x01, 0x11]'
BYTECODE=$(jq .deployedBytecode.object -r out/AssertTrueFalse.sol/AssertTrueFalse.json)
hevm symbolic --sig "test_assertFalse()" --code $BYTECODE

Halmos

halmos --match-contract GaussSpec --match-test equivalence

Certora

certoraRun src/Gauss.sol --verify Gauss:src/GaussCertora.spec --solc solc

Kontrol

kontrol build
kontrol prove --match-test GaussSpec.check_equivalence --bmc-depth 3

Kontrol Loop Invariant

kontrol build --require src/lemmas.k --module-import GaussSpec:GAUSS-LEMMAS --regen --rekompile

kprove --definition out/kompiled --spec-module LOOP-INVARIANTS src/lemmas.k

kontrol prove --match-test GaussSpec.check_equivalence --break-on-jumpi --bmc-depth 15

kontrol prove --match-test GaussSpec.check_equivalence --break-on-jumpi

kontrol show GaussSpec.check_equivalence