slotPacking.dfy

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');               // []
  }


}