Language design axes: full implementation (25 steps across 6 axes)

Compiler/ABI.lean

@@ -22,6 +22,8 @@ private def abiTypeString : ParamType → String
   | .tuple _ => "tuple"
   | .array t => abiTypeString t ++ "[]"
   | .fixedArray t n => abiTypeString t ++ "[" ++ toString n ++ "]"
+  | .adt _ _ => "tuple"  -- ADTs are ABI-encoded as static tuples
+  | .newtypeOf _ baseType => abiTypeString baseType  -- Erased to base type
 
 -- Uses `fieldTypeToParamType` from CompilationModel (shared, not duplicated).
 -- Uses `isInteropEntrypointName` from CompilationModel for consistent filtering.
@@ -39,6 +41,13 @@ mutual
     | .tuple elems =>
         let rendered := elems.map (fun ty => renderParam "" ty none)
         some ("[" ++ String.intercalate ", " rendered ++ "]")
+    | .adt _ maxFields =>
+        -- ADTs encode as (uint8 tag, uint256 field₀, ..., uint256 fieldₙ)
+        let tagComponent := renderParam "tag" .uint8 none
+        let fieldComponents := List.range maxFields |>.map fun i =>
+          renderParam s!"field{i}" .uint256 none
+        some ("[" ++ String.intercalate ", " (tagComponent :: fieldComponents) ++ "]")
+    | .newtypeOf _ baseType => abiComponents? baseType
     | .array t => abiComponents? t
     | .fixedArray t _ => abiComponents? t
     | _ => none
@@ -126,4 +135,50 @@ def writeContractABIFile (outDir : String) (spec : CompilationModel) : IO Unit :
   let path := s!"{outDir}/{spec.name}.abi.json"
   IO.FS.writeFile path (emitContractABIJson spec)
 
+/-- Render the storage layout for a contract as a JSON object.
+    Includes EIP-7201 namespace when present (#1730, Axis 4 Step 4d).
+    The output is a JSON object with `"contract"`, `"storageNamespace"`,
+    and `"fields"` keys. -/
+def emitContractStorageLayoutJson (spec : CompilationModel) : String :=
+  let nsTerm := match spec.storageNamespace with
+    | some ns => jsonString (toString ns)
+    | none => "null"
+  let fieldEntries := renderFields spec.fields 0
+  "{" ++ joinJsonFields [
+    s!"\"contract\": {jsonString spec.name}",
+    s!"\"storageNamespace\": {nsTerm}",
+    s!"\"fields\": [{String.intercalate ", " fieldEntries}]"
+  ] ++ "}\n"
+where
+  renderFieldType : FieldType → String
+    | .uint256 => "uint256"
+    | .address => "address"
+    | .adt name maxFields => s!"adt({name},{maxFields})"
+    | .dynamicArray elemType => renderStorageArrayElemType elemType ++ "[]"
+    | .mappingTyped _ => "mapping"
+    | .mappingStruct _ _ => "mapping"
+    | .mappingStruct2 _ _ _ => "mapping"
+  renderStorageArrayElemType : StorageArrayElemType → String
+    | .uint256 => "uint256"
+    | .address => "address"
+    | .bool => "bool"
+    | .uint8 => "uint8"
+    | .bytes32 => "bytes32"
+  renderFields (fields : List Field) (idx : Nat) : List String :=
+    match fields with
+    | [] => []
+    | f :: rest =>
+        let slot := f.slot.getD idx
+        let entry := "{" ++ joinJsonFields [
+          s!"\"name\": {jsonString f.name}",
+          s!"\"slot\": {jsonString (toString slot)}",
+          s!"\"type\": {jsonString (renderFieldType f.ty)}"
+        ] ++ "}"
+        entry :: renderFields rest (idx + 1)
+
+def writeContractStorageLayoutFile (outDir : String) (spec : CompilationModel) : IO Unit := do
+  IO.FS.createDirAll outDir
+  let path := s!"{outDir}/{spec.name}.storage.json"
+  IO.FS.writeFile path (emitContractStorageLayoutJson spec)
+
 end Compiler.ABI

Compiler/CompilationModel.lean

@@ -7,6 +7,7 @@
 import Compiler.CompilationModel.Types
 import Compiler.CompilationModel.AbiHelpers
 import Compiler.CompilationModel.AbiTypeLayout
+import Compiler.CompilationModel.AdtStorageLayout
 import Compiler.CompilationModel.AbiEncoding
 import Compiler.CompilationModel.DynamicData
 import Compiler.CompilationModel.EcmAxiomCollection

Compiler/CompilationModel/AbiEncoding.lean

@@ -250,6 +250,25 @@ partial def compileUnindexedAbiEncode
             ])
           ], YulExpr.call "add" [YulExpr.lit 32, YulExpr.ident paddedName])
 
+  | ParamType.adt _ maxFields =>
+      -- ADTs are ABI-encoded as (uint8 tag, uint256 field0, ..., uint256 fieldN)
+      -- Tag word: load and mask to uint8
+      let tagLoaded := dynamicWordLoad dynamicSource srcBase
+      let tagStore := YulStmt.expr (YulExpr.call "mstore" [
+        dstBase, YulExpr.call "and" [tagLoaded, YulExpr.lit 0xFF]
+      ])
+      -- Field words: load consecutive words from source
+      let fieldStores := (List.range maxFields).map fun i =>
+        let srcOff := YulExpr.call "add" [srcBase, YulExpr.lit ((i + 1) * 32)]
+        let dstOff := YulExpr.call "add" [dstBase, YulExpr.lit ((i + 1) * 32)]
+        YulStmt.expr (YulExpr.call "mstore" [dstOff, dynamicWordLoad dynamicSource srcOff])
+      let totalBytes := 32 * (1 + maxFields)
+      pure (tagStore :: fieldStores, YulExpr.lit totalBytes)
+
+  | ParamType.newtypeOf _ baseType =>
+      -- Newtypes erased to base type (#1727 Step 3b)
+      compileUnindexedAbiEncode dynamicSource baseType srcBase dstBase stem
+
 def revertWithCustomError (dynamicSource : DynamicDataSource)
     (errorDef : ErrorDef) (sourceArgs : List Expr) (args : List YulExpr) :
     Except String (List YulStmt) := do
@@ -282,6 +301,25 @@ def revertWithCustomError (dynamicSource : DynamicDataSource)
     | ParamType.uint256 | ParamType.int256 | ParamType.uint8 | ParamType.address | ParamType.bool | ParamType.bytes32 =>
         let encoded ← encodeStaticCustomErrorArg errorDef.name ty argExpr
         pure [YulStmt.expr (YulExpr.call "mstore" [YulExpr.lit headOffset, encoded])]
+    | ParamType.adt _ maxFields =>
+        match srcExpr with
+        | Expr.param name =>
+            let tagStore := YulStmt.expr (YulExpr.call "mstore" [
+              YulExpr.lit headOffset,
+              YulExpr.call "and" [argExpr, YulExpr.lit 0xFF]
+            ])
+            let fieldStores := (List.range maxFields).map fun fieldIdx =>
+              YulStmt.expr (YulExpr.call "mstore" [
+                YulExpr.lit (headOffset + (fieldIdx + 1) * 32),
+                YulExpr.ident s!"{name}_f{fieldIdx}"
+              ])
+            pure (tagStore :: fieldStores)
+        | _ =>
+            throw s!"Compilation error: custom error '{errorDef.name}' parameter of type {repr ty} currently requires direct parameter reference ({issue586Ref})."
+    | ParamType.newtypeOf _ baseType =>
+        -- Newtypes erased to base type (#1727 Step 3b)
+        let encoded ← encodeStaticCustomErrorArg errorDef.name baseType argExpr
+        pure [YulStmt.expr (YulExpr.call "mstore" [YulExpr.lit headOffset, encoded])]
     | ParamType.tuple _ | ParamType.fixedArray _ _ =>
         match srcExpr with
         | Expr.param name =>

Compiler/CompilationModel/AbiHelpers.lean

@@ -56,6 +56,10 @@ mutual
     | ParamType.array t => paramTypeToSolidityString t ++ "[]"
     | ParamType.fixedArray t n => paramTypeToSolidityString t ++ "[" ++ toString n ++ "]"
     | ParamType.bytes => "bytes"
+    | ParamType.adt _name maxFields =>
+        -- ABI-encoded as static tuple: (uint8, uint256, ..., uint256)
+        "(" ++ String.intercalate "," ("uint8" :: List.replicate maxFields "uint256") ++ ")"
+    | ParamType.newtypeOf _ baseType => paramTypeToSolidityString baseType  -- Erased to base type
 
   private def paramTypeListToSolidityStrings : List ParamType → List String
     | [] => []
@@ -79,6 +83,7 @@ def storageArrayElemTypeToParamType : StorageArrayElemType → ParamType
 def fieldTypeToParamType : FieldType → ParamType
   | FieldType.uint256 => ParamType.uint256
   | FieldType.address => ParamType.address
+  | FieldType.adt name maxFields => ParamType.adt name maxFields
   | FieldType.dynamicArray elemType => ParamType.array (storageArrayElemTypeToParamType elemType)
   | FieldType.mappingTyped _ => ParamType.uint256
   | FieldType.mappingStruct _ _ => ParamType.uint256

Compiler/CompilationModel/AbiTypeLayout.lean

@@ -17,6 +17,8 @@ mutual
     | ParamType.bytes => true
     | ParamType.fixedArray elemTy _ => isDynamicParamType elemTy
     | ParamType.tuple elemTys => isDynamicParamTypeList elemTys
+    | ParamType.adt _ _ => false  -- ADTs are statically-sized tagged unions
+    | ParamType.newtypeOf _ baseType => isDynamicParamType baseType  -- Erased to base type
   termination_by ty => sizeOf ty
 
   def isDynamicParamTypeList : List ParamType → Bool
@@ -43,6 +45,8 @@ mutual
         if isDynamicParamType elemTy then 32 else n * paramHeadSize elemTy
     | ParamType.tuple elemTys =>
         if isDynamicParamTypeList elemTys then 32 else paramHeadSizeList elemTys
+    | ParamType.adt _ maxFields => 32 * (1 + maxFields)  -- ADTs: uint8 tag word + maxFields field words (#1727 Step 5e)
+    | ParamType.newtypeOf _ baseType => paramHeadSize baseType  -- Erased to base type
   termination_by ty => sizeOf ty
 
   def paramHeadSizeList : List ParamType → Nat

Compiler/CompilationModel/AdtStorageLayout.lean

@@ -0,0 +1,75 @@
+/-
+  Compiler.CompilationModel.AdtStorageLayout: Storage layout helpers for ADTs
+
+  ADT storage encoding uses a tagged-union layout:
+  - Slot 0 (relative): tag byte (uint8, identifies the variant)
+  - Slots 1..N (relative): max-width fields in consecutive slots
+
+  The total storage footprint is 1 + max(variant field counts).
+  All variants share the same field slots — unused trailing slots
+  are simply not read/written for shorter variants.
+
+  (#1727, Phase 5 Steps 5c+5d)
+-/
+import Compiler.CompilationModel.Types
+
+namespace Compiler.CompilationModel
+
+open Compiler.Yul
+
+/-- Look up an ADT type definition by name. -/
+def lookupAdtTypeDef (adtTypes : List AdtTypeDef) (name : String) :
+    Except String AdtTypeDef :=
+  match adtTypes.find? (·.name == name) with
+  | some def_ => pure def_
+  | none => throw s!"Compilation error: unknown ADT type '{name}'"
+
+/-- Look up a variant within an ADT type definition by name. -/
+def lookupAdtVariant (def_ : AdtTypeDef) (variantName : String) :
+    Except String AdtVariant :=
+  match def_.variants.find? (·.name == variantName) with
+  | some v => pure v
+  | none => throw s!"Compilation error: unknown variant '{variantName}' in ADT '{def_.name}'"
+
+/-- Maximum number of field slots across all variants. -/
+def adtMaxFieldSlots (def_ : AdtTypeDef) : Nat :=
+  def_.variants.foldl (fun acc v => max acc v.fields.length) 0
+
+/-! ### Yul compilation helpers for ADT storage operations
+
+These generate Yul AST fragments for reading/writing ADT values
+stored in contract storage. The caller provides the base slot
+(resolved from the contract's field list) and the ADT type info.
+-/
+
+/-- Read the tag byte from an ADT's storage slot.
+    `baseSlot` is the Yul expression for the ADT field's first slot. -/
+def compileAdtTagRead (baseSlot : YulExpr) : YulExpr :=
+  -- Tag is stored as a full word in the base slot (mask to uint8)
+  YulExpr.call "and" [
+    YulExpr.call "sload" [baseSlot],
+    YulExpr.lit 0xFF
+  ]
+
+/-- Write the tag byte to an ADT's storage base slot. -/
+def compileAdtTagWrite (baseSlot : YulExpr) (tagValue : Nat) : YulStmt :=
+  YulStmt.expr (YulExpr.call "sstore" [baseSlot, YulExpr.lit tagValue])
+
+/-- Read a field from an ADT variant in storage.
+    `baseSlot` is the ADT's first slot, `fieldIndex` is 0-based within the variant.
+    Fields occupy slots base+1, base+2, ... -/
+def compileAdtFieldRead (baseSlot : YulExpr) (fieldIndex : Nat) : YulExpr :=
+  YulExpr.call "sload" [
+    YulExpr.call "add" [baseSlot, YulExpr.lit (fieldIndex + 1)]
+  ]
+
+/-- Write a field value into an ADT variant's storage slot.
+    `baseSlot` is the ADT's first slot, `fieldIndex` is 0-based. -/
+def compileAdtFieldWrite (baseSlot : YulExpr) (fieldIndex : Nat)
+    (valueExpr : YulExpr) : YulStmt :=
+  YulStmt.expr (YulExpr.call "sstore" [
+    YulExpr.call "add" [baseSlot, YulExpr.lit (fieldIndex + 1)],
+    valueExpr
+  ])
+
+end Compiler.CompilationModel