Skip to content

Instantly share code, notes, and snippets.

@gaxiiiiiiiiiiii
Last active January 5, 2024 11:18
Show Gist options
  • Save gaxiiiiiiiiiiii/e5bd68fb0afc987cdd27740e472beeef to your computer and use it in GitHub Desktop.
Save gaxiiiiiiiiiiii/e5bd68fb0afc987cdd27740e472beeef to your computer and use it in GitHub Desktop.
include "evm-dafny/src/dafny/core/memory.dfy"
include "evm-dafny/src/dafny/util/int.dfy"
include "evm-dafny/src/dafny/util/bytes.dfy"
include "evm-dafny/src/dafny/bytecode.dfy"
include "evm-dafny/src/dafny/evm.dfy"
// include "evm-dafny/libs/DafnyCrypto/src/dafny/util/math.dfy"
module slotPacking {
import opened Int
import opened Opcode
import opened Bytecode
import EVM
import opened EvmState
import ByteUtils
// Implemented a custom Pow function, as MathUtils.Pow was not tail-recursive.
function PowAux(n: nat, k: nat, acc: nat): nat
{ if k == 0 then acc else PowAux(n, k - 1, n * acc) }
function Pow(n: nat, k: nat): nat
{ PowAux(n, k, 1) }
lemma PowAux_lemma (n : nat, k : nat, acc : nat)
ensures PowAux(n, k, acc) == acc * PowAux(n, k, 1)
{}
lemma pow_succ (n : nat, k : nat)
ensures Pow(n,k+1) == n * Pow(n,k)
{ PowAux_lemma(n, k, n); }
lemma pow_le (n : nat, x : nat, y : nat)
requires 0 < n
requires x <= y
ensures Pow(n,x) <= Pow(n,y)
{
var i := x;
while i < y
decreases y - i
invariant i <= y
invariant Pow(n,x) <= Pow(n,i)
{
pow_succ(n, i);
i := i + 1;
}
}
lemma pow_positive (n : nat, k : nat)
requires 0 < n
ensures 0 < Pow(n, k)
{
if k == 0 {} else {
pow_positive(n, k - 1);
pow_succ(n, k - 1);
}
}
// representation of storage
ghost function U256toBytesAux (w : u256, n : nat) : (l : seq<u8>)
ensures |l| == n
{
if n == 0 then []
else [(w % 0x100) as u8] + U256toBytesAux(w / 0x100, n - 1)
}
ghost function u256ToBytes (w : u256) : (l : seq<u8>)
ensures |l| == 32
{ U256toBytesAux(w, 32) }
method u256ToBytes_test () {
var w : u256 := 0x12345678;
var l : seq<u8> := u256ToBytes(w);
assert l[0] == 0x78;
assert l[1] == 0x56;
assert l[2] == 0x34;
assert l[3] == 0x12;
}
method PartialLoad (st : ExecutingState, n : u256, k : nat, l : nat)
returns( st' : ExecutingState)
requires k + l < 32
requires st.PC() == 0 && st.Capacity() >= 3 && st.Fork() == EvmFork.BERLIN
ensures st'.Operands() >= 1
ensures u256ToBytes(st.Load(n))[k..k+l] == u256ToBytes(st'.Peek(0))[..l]
{
pow_le(256,l,31);
pow_positive(256,l);
assert Pow(256, 31) < MAX_U256;
var mask := (Pow(256,l) - 1) as u256;
st' := PushN(st, 32, n); // [n]
st' := SLoad(st'); // [storage]
st' := Push1(st', k as u8); // [k, storage]
st' := Push2(st', 0x100); // [address, storage]
st' := Bytecode.Div(st'); // [storage']
st' := PushN(st', 32, mask); // [mask, storage']
st' := And(st'); // [data]
}
method PartialStore(st : ExecutingState, n : u256, k : nat, l : nat, data : u256)
returns (st' : ExecutingState)
requires k + l < 32
requires 0 < l
requires st.PC() == 0 && st.Capacity() >= 4 && st.Fork() == EvmFork.BERLIN && st.WritesPermitted()
ensures u256ToBytes(data)[..l] == u256ToBytes(st'.Load(n))[k..k+l]
{
pow_le(256,l,31);
pow_positive(256,l);
assert Pow(256, 31) < MAX_U256;
assert 0 <= Pow(256, l) <= Pow(256, 31) < MAX_U256;
assert 0 <= Pow(256, l) - 1 < MAX_U256;
var mask := (Pow(256,l) - 1) as u256;
// filter
st' := Push2(st, 0x100); // [0x100]
st' := Push1(st', k as u8); // [k, 0x100]
st' := Mul(st'); // [size]
st' := Dup(st',1); // [size, size]
st' := PushN(st', 32, mask); // [mask,size,size]
st' := Mul(st'); // [pre_filter, size];
st' := Not(st'); // [filter, size];
// initialize
st' := PushN(st', 32, n); // [n, filter, size]
st' := SLoad(st'); // [storage, filter, size]
st' := And(st'); // [storage', size]
// verify the size of input data
st' := Swap(st',1); // [size, storage']
st' := PushN(st', 32, data); // [data, size, storage']
st' := PushN(st', 32, mask); // [mask, data, size, storage']
// new data
st' := And(st'); // [data', size, storage']
st' := Mul(st'); // [data'', storage']
st' := Or(st');
// // store
st' := PushN(st', 32, n); // [n, data'']
assert st'.Operands() >= 2;
assert st'.WritesPermitted();
st' := SStore(st'); // []
}
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment