Proposal for a library for defining packed records

[rodrigogribeiro]

Packed Records via Generic Programming (SOP)

Motivation

In Solidity, packed records are structs whose fields fit within a single
256-bit EVM storage slot. Core Solidity currently has no generic mechanism for
describing or deriving the bit layout of such structures. This proposal uses the
sum-of-products (SOP) representation, which the compiler already uses
internally in Hull, to derive encode/decode operations generically.

Core design

The system has three layers:

1. Generic(rep): a multi-parameter type class that captures the
   isomorphism between a user-defined type and its SOP representation. Users
   write this instance manually; it is the only instance they ever need to write
   for a new type.

2. Packable: a single-parameter type class with structural instances for
   all SOP building blocks ((), bool, word, products, sums). A bridge
   instance makes every type with a Generic instance automatically
   Packable.

3. Storable: a type class for EVM storage read/write, derived
   automatically from Packable.

Components

1. The Generic class (std/Generic.solc)

forall a rep. class a : Generic(rep) {
    function from(x : a)   -> rep;
    function to(x   : rep) -> a;
}

This is a multi-parameter type class (MPTC) in the same style as Typedef. For
each user-defined data type, one instance is written mapping the type to its
nested binary sum-of-products representation.

2. The Packable class (std/Packable.solc)

forall a. class a : Packable {
    function bitWidth(x : a) -> word;   -- number of bits occupied
    function pack(x : a)     -> word;   -- encode into bits 0..bitWidth(x)-1
    function unpack(w : word) -> a;     -- decode from bits 0..bitWidth(x)-1
}

3. Bit helpers (std/Bits.solc)

Low-level word operations used by Packable:

function band(a : word, b : word) -> word;   -- bitwise AND
function bor(a : word, b : word)  -> word;   -- bitwise OR
function bxor(a : word, b : word) -> word;   -- bitwise XOR
function bnot(a : word)           -> word;   -- bitwise NOT
function shl_(n : word, x : word) -> word;   -- shift left  (x << n)
function shr_(n : word, x : word) -> word;   -- shift right (x >> n)
function mask(n : word)           -> word;   -- (1 << n) - 1
function maxWord(a : word, b : word) -> word;
function addWord(a : word, b : word) -> word;

4. Fixed-width integer types (std/Uint.solc)

Since the type system lacks dependent integers, common widths are explicit
newtypes:

data Uint8   = MkUint8(word);
data Uint16  = MkUint16(word);
data Uint32  = MkUint32(word);
data Uint64  = MkUint64(word);
data Uint128 = MkUint128(word);
data Address = MkAddress(word);   -- 160 bits (Ethereum address)

instance Uint32 : Packable {
    function bitWidth(x : Uint32) -> word { return 32; }
    function pack(x : Uint32) -> word {
        match x { | MkUint32(w) => return band(w, mask(32)); }
    }
    function unpack(w : word) -> Uint32 { return MkUint32(band(w, mask(32))); }
}
-- (analogous instances for Uint8, Uint16, Uint64, Uint128, Address)

5. EVM storage (std/Storage.solc)

forall a. a : Packable =>
class a : Storable {
    function sload(slot : word) -> a;
    function sstore(slot : word, v : a) -> ();
}

pragma no-patterson-condition Storable;
pragma no-bounded-variable-condition Storable;
forall a. a : Packable =>
default instance a : Storable {
    function sload(slot : word) -> a {
        let raw : word;
        assembly { raw := sload(slot) }
        return Packable.unpack(raw);
    }
    function sstore(slot : word, v : a) -> () {
        let w : word = Packable.pack(v);
        assembly { sstore(slot, w) }
    }
}

For types with bitWidth > 256, the user writes a specialised Storable
instance that distributes the value across multiple slots using derived slot
addresses.

[mbenke]

What's the difference between Generic and Typedef?

[rodrigogribeiro]

What's the difference between Generic and Typedef?

Basically, the same. Since I wanted to make it self contained, I decided to follow the standard of Haskell libraries and use Generic for the class denoting the isomorphism between a type and its sum-of-products representation.