From 37400b5db557dfc661d5153278f00dbd7f614dc2 Mon Sep 17 00:00:00 2001 From: rodrigogribeiro Date: Sun, 14 Jun 2026 16:59:52 -0300 Subject: [PATCH] ABI encode / decode for ADTs * Define ABI encode/decode in terms of sum-of-products representation of datatypes. * Adds tests --- std/ABIGeneric.solc | 103 +++++++++++++++++++-- std/Generic.solc | 117 ++---------------------- test/examples/dispatch/generic_sum.solc | 28 +++--- 3 files changed, 118 insertions(+), 130 deletions(-) diff --git a/std/ABIGeneric.solc b/std/ABIGeneric.solc index 02b6c0ef..ad87ac70 100644 --- a/std/ABIGeneric.solc +++ b/std/ABIGeneric.solc @@ -10,19 +10,110 @@ export { import std.{*}; import std.Generic.{*}; -// Top-level generic ABI encode. +function maxWord(a : word, b : word) -> word { + match gtWord(a, b) { + | true => return a; + | false => return b; + } +} + +// ─── ABIAttribs for the primitive sum(f, g) type ───────────────────────── +// headSize = 32 (tag word) + max(headSize(f), headSize(g)) + +forall f g . f:ABIAttribs, g:ABIAttribs => +instance sum(f, g) : ABIAttribs { + function headSize(ty : Proxy(sum(f, g))) -> word { + let pf : Proxy(f); + let pg : Proxy(g); + return 32 + maxWord(ABIAttribs.headSize(pf), ABIAttribs.headSize(pg)); + } + function isStatic(ty : Proxy(sum(f, g))) -> bool { + let pf : Proxy(f); + let pg : Proxy(g); + return and(ABIAttribs.isStatic(pf), ABIAttribs.isStatic(pg)); + } +} + +// ─── ABIEncode for sum(f, g) ───────────────────────────────────────────── +// Wire layout (static sums only): +// [offset + 0 .. offset + 31] : tag word (0 = inl, 1 = inr) +// [offset + 32 .. ] : encoded branch payload + +forall f g . f:ABIAttribs, f:ABIEncode, g:ABIAttribs, g:ABIEncode => +instance sum(f, g) : ABIEncode { + function encodeInto(x : sum(f, g), basePtr : word, offset : word, tail : word) -> word { + match x { + | inl(v) => + mstore(basePtr + offset, 0); + return ABIEncode.encodeInto(v, basePtr, offset + 32, tail); + | inr(v) => + mstore(basePtr + offset, 1); + return ABIEncode.encodeInto(v, basePtr, offset + 32, tail); + } + } +} + +// ─── ABIDecode for sum(f, g) ───────────────────────────────────────────── +// Reads the tag word at headOffset; dispatches to f or g decoder at headOffset + 32. + +forall f g reader . + reader : WordReader, + f : ABIAttribs, + ABIDecoder(f, reader) : ABIDecode(f), + ABIDecoder(g, reader) : ABIDecode(g) => +instance ABIDecoder(sum(f, g), reader) : ABIDecode(sum(f, g)) { + function decode(ptr : ABIDecoder(sum(f, g), reader), headOffset : word) -> sum(f, g) { + match ptr { + | ABIDecoder(rdr) => + let tag = WordReader.read(WordReader.advance(rdr, headOffset)); + match tag { + | 0 => + let dec_f : ABIDecoder(f, reader) = ABIDecoder(rdr); + return inl(ABIDecode.decode(dec_f, headOffset + 32)); + | _ => + let dec_g : ABIDecoder(g, reader) = ABIDecoder(rdr); + return inr(ABIDecode.decode(dec_g, headOffset + 32)); + } + } + } +} + +// ─── Default bridges: ABIAttribs and ABIEncode via Generic ─────────────── +// Any type 'a' with Generic(rep) inherits its ABI layout from rep. + +forall a rep . a:Generic(rep), rep:ABIAttribs => +default instance a : ABIAttribs { + function headSize(ty : Proxy(a)) -> word { + let prx : Proxy(rep); + return ABIAttribs.headSize(prx); + } + function isStatic(ty : Proxy(a)) -> bool { + let prx : Proxy(rep); + return ABIAttribs.isStatic(prx); + } +} + +forall a rep . a:Generic(rep), rep:ABIAttribs, rep:ABIEncode => +default instance a : ABIEncode { + function encodeInto(x : a, basePtr : word, offset : word, tail : word) -> word { + return ABIEncode.encodeInto(Generic.from(x), basePtr, offset, tail); + } +} + +// ─── Top-level generic encode function ─────────────────────────────────── // Serialises any 'a' that has a Generic(rep) instance. -// ABIEncode for 'a' is resolved via the default instance bridge in std.Generic. +// Only the Generic instance is required — ABIEncode is resolved via the bridge. + forall a rep . a:Generic(rep), rep:ABIAttribs, rep:ABIEncode => function encode(x : a, basePtr : word, offset : word, tail : word) -> word { let xrep : rep = Generic.from(x); return ABIEncode.encodeInto(xrep, basePtr, offset, tail); } -// Top-level generic ABI decode. -// Deserialises any 'a' whose representation type 'rep' is decodable. -// The caller supplies ABIDecoder(a, reader); the function wraps it in -// ABIDecoder(rep, reader), decodes the rep, then converts via Generic.to. +// ─── Top-level generic decode function ─────────────────────────────────── +// Deserialises any 'a' that has a Generic(rep) instance. +// Only the Generic instance is required — ABIDecode is resolved via the bridge. + forall a rep reader . a : Generic(rep), reader : WordReader, diff --git a/std/Generic.solc b/std/Generic.solc index 18b180bc..ba30049d 100644 --- a/std/Generic.solc +++ b/std/Generic.solc @@ -1,120 +1,17 @@ -pragma no-patterson-condition ABIAttribs, ABIEncode; -pragma no-bounded-variable-condition ABIAttribs, ABIEncode; +pragma no-patterson-condition; +pragma no-bounded-variable-condition; -export { - Sum(*), - Generic -}; +export { Generic }; import std.{*}; -// Binary tagged union: the only new representation type. -// Native () and (f, g) are reused as Unit and Prod respectively; -// they already have full ABIAttribs / ABIEncode / ABIDecode support in std.solc. -data Sum(f, g) = Inl(f) | Inr(g); - // MPTC: isomorphism between a user type and its SOP representation. -// Pattern mirrors Typedef(rep) in std.solc. +// The representation 'rep' is built from primitive Solcore types: +// sum(f, g) with constructors inl / inr +// (f, g) pair (product) +// () unit forall a rep. class a : Generic(rep) { function from(x : a) -> rep; function to(x : rep) -> a; } - -// Maximum of two words, used for Sum headSize. -function maxWord(a : word, b : word) -> word { - match gtWord(a, b) { - | true => return a; - | false => return b; - } -} - -// ABIAttribs for Sum: -// headSize = 32 (tag word) + max(headSize(f), headSize(g)) -forall f g . f:ABIAttribs, g:ABIAttribs => -instance Sum(f, g) : ABIAttribs { - function headSize(ty : Proxy(Sum(f, g))) -> word { - let pf : Proxy(f); - let pg : Proxy(g); - return 32 + maxWord(ABIAttribs.headSize(pf), ABIAttribs.headSize(pg)); - } - function isStatic(ty : Proxy(Sum(f, g))) -> bool { - let pf : Proxy(f); - let pg : Proxy(g); - return and(ABIAttribs.isStatic(pf), ABIAttribs.isStatic(pg)); - } -} - -// ABIEncode for Sum. -// Wire layout (static sums only): -// [offset + 0 .. offset + 31] : tag word (0 = Inl, 1 = Inr) -// [offset + 32 .. ] : encoded branch payload -// For uniform sums (headSize(f) == headSize(g)) no bytes are left uninitialised. -forall f g . f:ABIAttribs, f:ABIEncode, g:ABIAttribs, g:ABIEncode => -instance Sum(f, g) : ABIEncode { - function encodeInto(x : Sum(f, g), basePtr : word, offset : word, tail : word) -> word { - match x { - | Sum.Inl(v) => - mstore(basePtr + offset, 0); - return ABIEncode.encodeInto(v, basePtr, offset + 32, tail); - | Sum.Inr(v) => - mstore(basePtr + offset, 1); - return ABIEncode.encodeInto(v, basePtr, offset + 32, tail); - } - } -} - -// ABIDecode for Sum. -// Reads the tag word at headOffset; dispatches to the f or g decoder at headOffset + 32. -forall f g reader . - reader:WordReader, - f:ABIAttribs, - ABIDecoder(f, reader) : ABIDecode(f), - ABIDecoder(g, reader) : ABIDecode(g) => -instance ABIDecoder(Sum(f, g), reader) : ABIDecode(Sum(f, g)) { - function decode(ptr : ABIDecoder(Sum(f, g), reader), headOffset : word) -> Sum(f, g) { - match ptr { - | ABIDecoder(rdr) => - let tag = WordReader.read(WordReader.advance(rdr, headOffset)); - match tag { - | 0 => - let dec_f : ABIDecoder(f, reader) = ABIDecoder(rdr); - return Sum.Inl(ABIDecode.decode(dec_f, headOffset + 32)); - | _ => - let dec_g : ABIDecoder(g, reader) = ABIDecoder(rdr); - return Sum.Inr(ABIDecode.decode(dec_g, headOffset + 32)); - } - } - } -} - -// Bridge: any type with a Generic(rep) instance gains ABIAttribs automatically. -forall a rep . a:Generic(rep), rep:ABIAttribs => -default instance a : ABIAttribs { - function headSize(ty : Proxy(a)) -> word { - let prx : Proxy(rep); - return ABIAttribs.headSize(prx); - } - function isStatic(ty : Proxy(a)) -> bool { - let prx : Proxy(rep); - return ABIAttribs.isStatic(prx); - } -} - -// Bridge: any type with a Generic(rep) instance gains ABIEncode automatically. -forall a rep . a:Generic(rep), rep:ABIAttribs, rep:ABIEncode => -default instance a : ABIEncode { - function encodeInto(x : a, basePtr : word, offset : word, tail : word) -> word { - let r : rep = Generic.from(x); - return ABIEncode.encodeInto(r, basePtr, offset, tail); - } -} - -// Note: ABIDecode bridge omitted. The class head ABIDecoder(a, reader) is a type -// application, not a plain variable, so Solcore's "default instance" restriction -// makes automatic derivation impossible. To decode a Generic type, create an -// ABIDecoder for the representation type and call Generic.to on the result: -// -// let dec : ABIDecoder(Rep, MemoryWordReader) = ABIDecoder.ABIDecoder(reader); -// let rep : Rep = ABIDecode.decode(dec, offset); -// let val : MyType = Generic.to(rep); diff --git a/test/examples/dispatch/generic_sum.solc b/test/examples/dispatch/generic_sum.solc index abbf11ce..b1f8373e 100644 --- a/test/examples/dispatch/generic_sum.solc +++ b/test/examples/dispatch/generic_sum.solc @@ -9,19 +9,19 @@ pragma no-bounded-variable-condition; data Option(a) = None | Some(a); -// Generic instance using the Sum ADT from std.Generic as the representation. -// Sum((), uint256): Sum.Inl(()) = None, Sum.Inr(v) = Some(v) -instance Option(uint256) : Generic(Sum((), uint256)) { - function from(x : Option(uint256)) -> Sum((), uint256) { +// Only requirement: Generic instance using the primitive sum type. +// rep = sum((), uint256): inl(()) = None, inr(v) = Some(v) +instance Option(uint256) : Generic(sum((), uint256)) { + function from(x : Option(uint256)) -> sum((), uint256) { match x { - | Option.None => return Sum.Inl(()); - | Option.Some(v) => return Sum.Inr(v); + | Option.None => return inl(()); + | Option.Some(v) => return inr(v); } } - function to(r : Sum((), uint256)) -> Option(uint256) { + function to(r : sum((), uint256)) -> Option(uint256) { match r { - | Sum.Inl(_) => return Option.None; - | Sum.Inr(v) => return Option.Some(v); + | inl(_) => return Option.None; + | inr(v) => return Option.Some(v); } } } @@ -29,8 +29,8 @@ instance Option(uint256) : Generic(Sum((), uint256)) { contract GenericSum { constructor() {} - // Calls encode; returns the tag word at offset 0. - // None -> 0 (Sum.Inl) + // Calls encode; returns the tag word (first 32 bytes). + // None → 0 public function encodeNone() -> uint256 { let x : Option(uint256) = Option.None; let buf = allocate_zeroed_memory(64); @@ -38,8 +38,8 @@ contract GenericSum { return Typedef.abs(mload(buf)); } - // Calls encode; returns the tag word at offset 0. - // Some(n) -> 1 (Sum.Inr) + // Calls encode; returns the tag word (first 32 bytes). + // Some(n) → 1 public function encodeSomeTag(n : uint256) -> uint256 { let x : Option(uint256) = Option.Some(n); let buf = allocate_zeroed_memory(64); @@ -47,7 +47,7 @@ contract GenericSum { return Typedef.abs(mload(buf)); } - // Calls encode; returns the payload word at offset 32. + // Calls encode; returns the payload word (bytes 32-63). public function encodePayload(n : uint256) -> uint256 { let x : Option(uint256) = Option.Some(n); let buf = allocate_zeroed_memory(64);