feat: integrate trm assembly module

[DavePearce]

This integrates an assembly implementation of the trm module, including those constants necessary to distinguish the different numbers of precompiles in different forks.

Constraints (MIR)

Full constraints for this module:

(module trm)

(inputs
   (RAW_ADDRESS'0 u128 0x0)
   (RAW_ADDRESS'1 u128 0x0)
)

(outputs
   (ADDRESS_HI u32 0x0)
   (IS_PRECOMPILE u1 0x0)
)

(computed
   (low u128 0x0)
   (tmp u128 0x0)
   (high u96 0x0)
   (b u1 0x0)
)

(compute trm)
(range RAW_ADDRESS'0 u128)
(range RAW_ADDRESS'1 u128)
(range ADDRESS_HI u32)
(range IS_PRECOMPILE u1)
(range low u128)
(range tmp u128)
(range high u96)
(range b u1)

(vanish "trm:pc0"
   (∧ (== low RAW_ADDRESS'0) (== (+ ADDRESS_HI (* 2^32 high)) RAW_ADDRESS'1)
      (if (== ADDRESS_HI 0)
         (if (== low 0)
            (== IS_PRECOMPILE 0)
            (∧ (== tmp (+ low -8 (* 2^128 b))) (== IS_PRECOMPILE b)))
         (== IS_PRECOMPILE 0))))

---

Note

Integrates zkasm-based TRM function and updates lookups and fork-specific constants to the new RAW_ADDRESS/ADDRESS_HI interface.

• TRM:
  • Replace Lisp module (trm/columns.lisp, trm/constants.lisp, trm/constraints.lisp) and WCP lookup with zkasm implementation trm/trm.zkasm exposing trm(RAW_ADDRESS u256) -> (ADDRESS_HI u32, IS_PRECOMPILE u1).
• Lookups:
  • Update hub/*/lookups/hub_into_trm.lisp, rlpaddr/lookups/rlpaddr_into_trm.lisp, and rlptxn/cancun/lookups/rlptxn_into_trm.lisp to use trm.RAW_ADDRESS (combined HI/LO) and trm.ADDRESS_HI; remove legacy IOMF/per-word columns.
• Constants:
  • Migrate fork-specific MAX_PRC_ADDRESS to zkasm (constants/*/constants.zkasm), removing .lisp constants.
• Build:
  • Adjust Makefile to reference .zkasm constants and TRM := trm/trm.zkasm.

^{Written by Cursor Bugbot for commit 909def3. This will update automatically on new commits. Configure here.}

[DavePearce]

Constraints (AIR)

(module trm)

(inputs
   (RAW_ADDRESS'0 u128 0x0)
   (RAW_ADDRESS'1 u128 0x0)
)

(outputs
   (ADDRESS_HI u32 0x0)
   (IS_PRECOMPILE u1 0x0)
)

(computed
   (low u128 0x0)
   (tmp u128 0x0)
   (high u96 0x0)
   (b u1 0x0)
   ("(inv trm:ADDRESS_HI)" 𝔽 0x0)
   ("(inv trm:low)" 𝔽 0x0)
)

(compute trm)
(inv (trm:"(inv trm:ADDRESS_HI)" 𝔽) ADDRESS_HI)
(inv (trm:"(inv trm:low)" 𝔽) low)
;; types
(lookup "RAW_ADDRESS'0:u128" ((_ u128:V)) ((_ trm:RAW_ADDRESS'0)))
(lookup "RAW_ADDRESS'1:u128" ((_ u128:V)) ((_ trm:RAW_ADDRESS'1)))
(lookup "ADDRESS_HI:u32" ((_ u32:V)) ((_ trm:ADDRESS_HI)))
(vanish "trm:IS_PRECOMPILE:u1" (* IS_PRECOMPILE (- IS_PRECOMPILE 1)))
(lookup "low:u128" ((_ u128:V)) ((_ trm:low)))
(lookup "tmp:u128" ((_ u128:V)) ((_ trm:tmp)))
(lookup "high:u96" ((_ u96:V)) ((_ trm:high)))
;; constraints
(vanish "trm:b:u1" (* b (- b 1)))
(vanish "trm:(inv trm:ADDRESS_HI) <=" (* ADDRESS_HI (- 1 (* ADDRESS_HI "(inv trm:ADDRESS_HI)"))))
(vanish "trm:(inv trm:low) <=" (* low (- 1 (* low "(inv trm:low)"))))
(vanish "trm:pc0#0" (- low RAW_ADDRESS'0))
(vanish "trm:pc0#1" (- (+ ADDRESS_HI (* 2^32 high)) RAW_ADDRESS'1))
(vanish "trm:pc0#2" (* (- 1 (* ADDRESS_HI "(inv trm:ADDRESS_HI)")) (- 1 (* low "(inv trm:low)")) IS_PRECOMPILE))
(vanish "trm:pc0#3" (* (- 1 (* ADDRESS_HI "(inv trm:ADDRESS_HI)")) low (- tmp low -8 (* 2^128 b))))
(vanish "trm:pc0#4" (* (- 1 (* ADDRESS_HI "(inv trm:ADDRESS_HI)")) low (- IS_PRECOMPILE b)))
(vanish "trm:pc0#5" (* ADDRESS_HI IS_PRECOMPILE)

[letypequividelespoubelles]

This won't work for Osaka (soon ...) as it introduces a new precompiles at 0x100: https://eips.ethereum.org/EIPS/eip-7951

[DavePearce]

Ok, well that's good to know. But, we can update it to support that when the time comes easily enough.