Skip to content

Instantly share code, notes, and snippets.

{
"contracts": {
"/Users/martinlundfall/test2/multipleCalls/src/easyNest.sol:Callee": {
"asm": {
".code": [
{
"begin": 24,
"end": 253,
"name": "PUSH",
"value": "80"
{
"contracts": {
"/Users/martinlundfall/multipleCalls/src/easyNest.sol:Callee": {
"asm": {
".code": [
{
"begin": 26,
"end": 255,
"name": "PUSH",
"value": "80"
{
"contracts": {
"src/easyNest.sol:Callee": {
"asm": {
".code": [
{
"begin": 26,
"end": 255,
"name": "PUSH",
"value": "80"
{
"contracts": {
"src/easyNest.sol:Callee": {
"asm": {
".code": [
{
"begin": 26,
"end": 255,
"name": "PUSH",
"value": "80"
{
"contracts": {
"src/easyNest.sol:Callee": {
"asm": {
".code": [
{
"begin": 26,
"end": 255,
"name": "PUSH",
"value": "80"
requires "edsl.k"
module DAI_PERMIT_TYPEHASH_PASS_ROUGH
imports ETHEREUM-SIMULATION
imports EVM
imports EDSL
// imports RULES
// Dai_PERMIT_TYPEHASH
rule
requires "../rules.k"
module DAI_TRANSFERFROM-DIFF_FAIL
imports ETHEREUM-SIMULATION
imports EVM
imports RULES
// Dai_transferFrom-diff
rule
<k> #execute ~> CONTINUATION => #halt ~> CONTINUATION </k>
requires "../rules.k"
module SAFEADD_ADD_PASS
imports ETHEREUM-SIMULATION
imports EVM
imports RULES
// SafeAdd_add
rule
<k> #execute ~> CONTINUATION => #halt ~> CONTINUATION </k>

Intro

When I was asked to come back and speak at ethcc again I initially said I would be speaking about formal verification, since this is the topic I've spent most of last year thinking about.

But I've also been talking about it a lot already, I can almost do in on autopilot by now.

So I wanted to do something different for ethcc. Especially since this is a little bit of a different conference. It's not less technical than other conferences, but it is definitely more political.

What in the end inspired me to change the topic of my talk was a presentation at CCC, the chaos communication congress in Leipzig on Ethics in mathematics by Maurice Chiodo. In his talk he outlined the extreme influence that the work of mathematicians have in the real world, and how unwilling mathematicians are to accept that there is any ethical aspect to their work.

requires "../rules.k"
module SAFEADD_ADD_FAIL
imports ETHEREUM-SIMULATION
imports EVM
imports RULES
// SafeAdd_add
rule
<k> #execute ~> CONTINUATION => #halt ~> CONTINUATION </k>