specs: Adds Certora specs for Scribe

specs/README.md

@@ -0,0 +1,37 @@
+# Certora Specification
+
+This directory provides specifications for the `Scribe` oracle contract symbolically proven by the [Certora Prover](https://www.certora.com/prover).
+
+## Usage
+
+The specification is written in `CVL`, the Certora Verification Language.
+
+### Prerequisites
+
+1. Install the Certora Prover CLI:
+```bash
+$ pip install certora-cli
+```
+
+2. Set your Certora key:
+```bash
+$ export CERTORAKEY=<your-certora-key>
+```
+
+### Running Specifications
+
+Run individual specifications using `certoraRun` with the corresponding `.conf` file:
+
+```bash
+# Auth invariants
+$ certoraRun specs/ScribeAuth.conf
+
+# Feed management invariants
+$ certoraRun specs/ScribeFeedManagement.conf
+
+# Poke invariants
+$ certoraRun specs/ScribePoke.conf
+
+# Toll invariants
+$ certoraRun specs/ScribeToll.conf
+```

specs/ScribeAuth.conf

@@ -0,0 +1,19 @@
+{
+    "files": [
+        "src/Scribe.sol"
+    ],
+    "verify": "Scribe:specs/ScribeAuth.spec",
+    "optimistic_loop": true,
+    "loop_iter": 3,
+    "rule_sanity": "basic",
+    "msg": "Scribe Auth Invariants",
+    "packages": [
+        "chronicle-std=lib/chronicle-std/src"
+    ],
+    "solc_optimize": "10000",
+    "parametric_contracts": ["Scribe"],
+    "prover_args": [
+        "-depth 15",
+        "-mediumTimeout 1800"
+    ]
+}

specs/ScribeAuth.spec

@@ -0,0 +1,118 @@
+// SPDX-License-Identifier: BUSL-1.1
+// Certora Verification Language (CVL) specification for Scribe
+
+methods {
+    // Feed management
+    function lift(LibSecp256k1.Point, IScribe.ECDSAData) external returns (uint8);
+    function lift(LibSecp256k1.Point[], IScribe.ECDSAData[]) external returns (uint8[]);
+    function drop(uint8) external;
+    function drop(uint8[]) external;
+    function setBar(uint8) external;
+
+    // Auth management
+    function rely(address) external;
+    function deny(address) external;
+    function authed(address) external returns (bool) envfree;
+    function wards(address) external returns (uint256) envfree;
+
+    // Toll management
+    function kiss(address) external;
+    function diss(address) external;
+}
+
+// -----------------------------------------------------------------------------
+// Manual Storage Management
+//
+// When verifying the following rules, calling `authed(e.msg.sender)` returns a
+// symbolic boolean that Certora does not automatically link to the actual
+// `_wards` storage that the `auth` modifier checks.
+//
+// This is because the `auth` modifier uses inline assembly to read
+// `_wards[msg.sender]`:
+//   let slot := keccak256(0x00, 0x40)
+//   let isAuthed := sload(slot)
+//
+// This direct `sload` is not linked to the `authed()` view function's return
+// value in Certora's symbolic execution. As a result, rules using `authed()`
+// may fail because the prover treats them as independent symbolic values.
+//
+// Therefore, a `ghostWards` ghost mapping is introduced that manually tracks
+// the `_wards` via storage hooks. Note that rules should therefore use the
+// `isAuthed(address)` helper function instead calling `authed(address)`
+// directly on the contract.
+
+ghost mapping(address => uint256) ghostWards {
+    init_state axiom forall address a. ghostWards[a] == 0;
+}
+
+hook Sstore currentContract._wards[KEY address who] uint256 newVal (uint256 oldVal) {
+    ghostWards[who] = newVal;
+}
+
+hook Sload uint256 val currentContract._wards[KEY address who] {
+    require ghostWards[who] == val;
+}
+
+definition isAuthed(address who) returns bool =
+    ghostWards[who] != 0;
+
+// ----------------------------------------------------------------------------
+// Rules
+
+rule liftRevertsIfNotAuthed(env e, LibSecp256k1.Point pubKey, IScribe.ECDSAData ecdsaData) {
+    bool callerAuthed = isAuthed(e.msg.sender);
+
+    lift@withrevert(e, pubKey, ecdsaData);
+
+    assert !callerAuthed => lastReverted;
+}
+
+rule dropRevertsIfNotAuthed(env e, uint8 feedId) {
+    bool callerAuthed = isAuthed(e.msg.sender);
+
+    drop@withrevert(e, feedId);
+
+    assert !callerAuthed => lastReverted;
+}
+
+rule setBarRevertsIfNotAuthed(env e, uint8 newBar) {
+    require newBar != 0;
+
+    bool callerAuthed = isAuthed(e.msg.sender);
+
+    setBar@withrevert(e, newBar);
+
+    assert !callerAuthed => lastReverted;
+}
+
+rule relyRevertsIfNotAuthed(env e, address who) {
+    bool callerAuthed = isAuthed(e.msg.sender);
+
+    rely@withrevert(e, who);
+
+    assert !callerAuthed => lastReverted;
+}
+
+rule denyRevertsIfNotAuthed(env e, address who) {
+    bool callerAuthed = isAuthed(e.msg.sender);
+
+    deny@withrevert(e, who);
+
+    assert !callerAuthed => lastReverted;
+}
+
+rule kissRevertsIfNotAuthed(env e, address who) {
+    bool callerAuthed = isAuthed(e.msg.sender);
+
+    kiss@withrevert(e, who);
+
+    assert !callerAuthed => lastReverted;
+}
+
+rule dissRevertsIfNotAuthed(env e, address who) {
+    bool callerAuthed = isAuthed(e.msg.sender);
+
+    diss@withrevert(e, who);
+
+    assert !callerAuthed => lastReverted;
+}

specs/ScribeFeedManagement.conf

@@ -0,0 +1,19 @@
+{
+    "files": [
+        "src/Scribe.sol"
+    ],
+    "verify": "Scribe:specs/ScribeFeedManagement.spec",
+    "optimistic_loop": true,
+    "loop_iter": 3,
+    "rule_sanity": "basic",
+    "msg": "Scribe Feed Management Invariants",
+    "packages": [
+        "chronicle-std=lib/chronicle-std/src"
+    ],
+    "solc_optimize": "10000",
+    "parametric_contracts": ["Scribe"],
+    "prover_args": [
+        "-depth 15",
+        "-mediumTimeout 1800"
+    ]
+}

specs/ScribeFeedManagement.spec

@@ -0,0 +1,63 @@
+// SPDX-License-Identifier: BUSL-1.1
+// Certora Verification Language (CVL) specification for Scribe
+
+methods {
+    function lift(LibSecp256k1.Point, IScribe.ECDSAData) external returns (uint8);
+    function lift(LibSecp256k1.Point[], IScribe.ECDSAData[]) external returns (uint8[]);
+    function drop(uint8) external;
+    function drop(uint8[]) external;
+    function feeds(address) external returns (bool) envfree;
+    function feeds(uint8) external returns (bool, address) envfree;
+}
+
+// -----------------------------------------------------------------------------
+// Ghost Storage Management
+
+ghost mapping(uint256 => uint256) ghostPubKeysX {
+    init_state axiom forall uint256 id. ghostPubKeysX[id] == 0;
+}
+
+ghost mapping(uint256 => uint256) ghostPubKeysY {
+    init_state axiom forall uint256 id. ghostPubKeysY[id] == 0;
+}
+
+hook Sstore currentContract._pubKeys[INDEX uint256 id].x uint256 newX (uint256 oldX) {
+    ghostPubKeysX[id] = newX;
+}
+
+hook Sload uint256 x currentContract._pubKeys[INDEX uint256 id].x {
+    require ghostPubKeysX[id] == x;
+}
+
+hook Sstore currentContract._pubKeys[INDEX uint256 id].y uint256 newY (uint256 oldY) {
+    ghostPubKeysY[id] = newY;
+}
+
+hook Sload uint256 y currentContract._pubKeys[INDEX uint256 id].y {
+    require ghostPubKeysY[id] == y;
+}
+
+// -----------------------------------------------------------------------------
+// Helper Functions
+
+definition isNotLiftOrDrop(method f) returns bool =
+    f.selector != sig:lift(LibSecp256k1.Point, IScribe.ECDSAData).selector &&
+    f.selector != sig:lift(LibSecp256k1.Point[], IScribe.ECDSAData[]).selector &&
+    f.selector != sig:drop(uint8).selector &&
+    f.selector != sig:drop(uint8[]).selector;
+
+// -----------------------------------------------------------------------------
+// Rules
+
+/// @dev Verifies no non-lift/drop function updates feeds.
+rule onlyLiftAndDropCanMutatePubKeys(method f, env e, calldataarg args, uint8 feedId)
+    filtered { f -> !f.isView && !f.isFallback && isNotLiftOrDrop(f) }
+{
+    uint256 pubKeyXBefore = ghostPubKeysX[feedId];
+    uint256 pubKeyYBefore = ghostPubKeysY[feedId];
+
+    f(e, args);
+
+    assert ghostPubKeysX[feedId] == pubKeyXBefore;
+    assert ghostPubKeysY[feedId] == pubKeyYBefore;
+}

specs/ScribePoke.conf

@@ -0,0 +1,19 @@
+{
+    "files": [
+        "src/Scribe.sol"
+    ],
+    "verify": "Scribe:specs/ScribePoke.spec",
+    "optimistic_loop": true,
+    "loop_iter": 3,
+    "rule_sanity": "basic",
+    "msg": "Scribe Poke Invariants",
+    "packages": [
+        "chronicle-std=lib/chronicle-std/src"
+    ],
+    "solc_optimize": "10000",
+    "parametric_contracts": ["Scribe"],
+    "prover_args": [
+        "-depth 15",
+        "-mediumTimeout 1800"
+    ]
+}

specs/ScribePoke.spec

@@ -0,0 +1,71 @@
+// SPDX-License-Identifier: BUSL-1.1
+// Certora Verification Language (CVL) specification for Scribe
+
+methods {
+    function poke(IScribe.PokeData, IScribe.SchnorrData) external;
+    function poke_optimized_7136211(IScribe.PokeData, IScribe.SchnorrData) external;
+    function bar() external returns (uint8) envfree;
+}
+
+// -----------------------------------------------------------------------------
+// Ghost Storage Management
+
+ghost uint128 ghostPokeDataVal {
+    init_state axiom ghostPokeDataVal == 0;
+}
+
+ghost uint32 ghostPokeDataAge {
+    init_state axiom ghostPokeDataAge == 0;
+}
+
+hook Sstore currentContract._pokeData.val uint128 newVal (uint128 oldVal) {
+    ghostPokeDataVal = newVal;
+}
+
+hook Sload uint128 val currentContract._pokeData.val {
+    require ghostPokeDataVal == val;
+}
+
+hook Sstore currentContract._pokeData.age uint32 newAge (uint32 oldAge) {
+    ghostPokeDataAge = newAge;
+}
+
+hook Sload uint32 age currentContract._pokeData.age {
+    require ghostPokeDataAge == age;
+}
+
+// -----------------------------------------------------------------------------
+// Helper Functions
+
+definition isNotPoke(method f) returns bool =
+    f.selector != sig:poke(IScribe.PokeData, IScribe.SchnorrData).selector &&
+    f.selector != sig:poke_optimized_7136211(IScribe.PokeData, IScribe.SchnorrData).selector;
+
+// -----------------------------------------------------------------------------
+// Rules
+
+/// @dev Verifies every value has an age.
+invariant valueImpliesAge()
+    ghostPokeDataVal != 0 => ghostPokeDataAge != 0;
+
+/// @dev Verifies no non-poke function updates the poke data.
+rule onlyPokeCanMutatePokeData(method f, env e, calldataarg args)
+    filtered { f -> !f.isView && !f.isFallback && isNotPoke(f) }
+{
+    uint128 valBefore = ghostPokeDataVal;
+    uint32 ageBefore = ghostPokeDataAge;
+
+    f(e, args);
+
+    assert ghostPokeDataVal == valBefore;
+    assert ghostPokeDataAge == ageBefore;
+}
+
+/// @dev Verifies poke reverts if length of `feedIds` does not match bar.
+rule pokeRevertsIfBarNotReached(env e, IScribe.PokeData pokeData, IScribe.SchnorrData schnorrData) {
+    require schnorrData.feedIds.length != to_mathint(bar());
+
+    poke@withrevert(e, pokeData, schnorrData);
+
+    assert lastReverted;
+}

specs/ScribeToll.conf

@@ -0,0 +1,19 @@
+{
+    "files": [
+        "src/Scribe.sol"
+    ],
+    "verify": "Scribe:specs/ScribeToll.spec",
+    "optimistic_loop": true,
+    "loop_iter": 3,
+    "rule_sanity": "basic",
+    "msg": "Scribe Toll Invariants",
+    "packages": [
+        "chronicle-std=lib/chronicle-std/src"
+    ],
+    "solc_optimize": "10000",
+    "parametric_contracts": ["Scribe"],
+    "prover_args": [
+        "-depth 15",
+        "-mediumTimeout 1800"
+    ]
+}