From d6e5a3e466d0ed2cc35ca932d9c44f1767abc5d7 Mon Sep 17 00:00:00 2001
From: makemake <vukasin@gostovic.me>
Date: Thu, 26 Feb 2026 17:42:33 +0100
Subject: [PATCH 1/2] feat: add spec stuff

---
 src/Assertion.sol    | 13 +++++++++++++
 src/SpecRecorder.sol | 29 +++++++++++++++++++++++++++++
 2 files changed, 42 insertions(+)
 create mode 100644 src/SpecRecorder.sol

diff --git a/src/Assertion.sol b/src/Assertion.sol
index 3e9559f..f18e5ef 100644
--- a/src/Assertion.sol
+++ b/src/Assertion.sol
@@ -3,6 +3,7 @@ pragma solidity ^0.8.13;
 
 import {Credible} from "./Credible.sol";
 import {TriggerRecorder} from "./TriggerRecorder.sol";
+import {SpecRecorder, AssertionSpec} from "./SpecRecorder.sol";
 import {StateChanges} from "./StateChanges.sol";
 
 /// @title Assertion
@@ -30,6 +31,10 @@ abstract contract Assertion is Credible, StateChanges {
     /// @dev Address is derived from a deterministic hash for consistency
     TriggerRecorder constant triggerRecorder = TriggerRecorder(address(uint160(uint256(keccak256("TriggerRecorder")))));
 
+    /// @notice The spec recorder precompile for registering the assertion spec
+    /// @dev Address is derived from keccak256("cats dining table")
+    SpecRecorder constant specRecorder = SpecRecorder(address(uint160(uint256(keccak256("cats dining table")))));
+
     /// @notice Used to record fn selectors and their triggers.
     function triggers() external view virtual;
 
@@ -65,4 +70,12 @@ abstract contract Assertion is Credible, StateChanges {
     function registerBalanceChangeTrigger(bytes4 fnSelector) internal view {
         triggerRecorder.registerBalanceChangeTrigger(fnSelector);
     }
+
+    /// @notice Registers the desired assertion spec. Must be called within the constructor.
+    /// The assertion spec defines what subset of precompiles are available.
+    /// Can only be called once. For an assertion to be valid, it needs a defined spec.
+    /// @param spec The desired AssertionSpec.
+    function registerAssertionSpec(AssertionSpec spec) internal view {
+        specRecorder.registerAssertionSpec(spec);
+    }
 }
diff --git a/src/SpecRecorder.sol b/src/SpecRecorder.sol
new file mode 100644
index 0000000..145fad6
--- /dev/null
+++ b/src/SpecRecorder.sol
@@ -0,0 +1,29 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.13;
+
+/// @notice The assertion spec defines what subset of precompiles are available.
+/// All new specs derive and expose all precompiles from the old definitions,
+/// unless specified otherwise.
+enum AssertionSpec {
+    /// @notice Standard set of PhEvm precompiles available at launch.
+    Legacy,
+    /// @notice Contains tx object precompiles.
+    Reshiram,
+    /// @notice Unrestricted access to all available precompiles. May be untested and dangerous.
+    Experimental
+}
+
+/// @title SpecRecorder
+/// @author Phylax Systems
+/// @notice Precompile interface for registering the desired assertion spec
+/// @dev Used within the constructor of assertion contracts to specify which
+/// subset of PhEvm precompiles should be available during assertion execution.
+/// You can only call registerAssertionSpec once per assertion.
+interface SpecRecorder {
+    /// @notice Called within the constructor to set the desired assertion spec.
+    /// The assertion spec defines what subset of precompiles are available.
+    /// You can only call this function once. For an assertion to be valid,
+    /// it needs to have a defined spec.
+    /// @param spec The desired AssertionSpec.
+    function registerAssertionSpec(AssertionSpec spec) external view;
+}

From ef88aecd1d72995a8e6a838c352a83a4270aafa8 Mon Sep 17 00:00:00 2001
From: makemake <vukasin@gostovic.me>
Date: Fri, 27 Feb 2026 13:48:58 +0100
Subject: [PATCH 2/2] fix: update specRecorder address

---
 src/Assertion.sol | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Assertion.sol b/src/Assertion.sol
index f18e5ef..1496ddc 100644
--- a/src/Assertion.sol
+++ b/src/Assertion.sol
@@ -32,8 +32,8 @@ abstract contract Assertion is Credible, StateChanges {
     TriggerRecorder constant triggerRecorder = TriggerRecorder(address(uint160(uint256(keccak256("TriggerRecorder")))));
 
     /// @notice The spec recorder precompile for registering the assertion spec
-    /// @dev Address is derived from keccak256("cats dining table")
-    SpecRecorder constant specRecorder = SpecRecorder(address(uint160(uint256(keccak256("cats dining table")))));
+    /// @dev Address is derived from keccak256("SpecRecorder")
+    SpecRecorder constant specRecorder = SpecRecorder(address(uint160(uint256(keccak256("SpecRecorder")))));
 
     /// @notice Used to record fn selectors and their triggers.
     function triggers() external view virtual;