From 3cbdffba664ef3105e6a3ceff4145df70b13cda1 Mon Sep 17 00:00:00 2001 From: merkleplant Date: Wed, 18 Feb 2026 15:33:09 +0100 Subject: [PATCH 1/3] specs: Adds certora specs for Scribe --- specs/ScribeAuth.conf | 19 +++++ specs/ScribeAuth.spec | 118 +++++++++++++++++++++++++++++++ specs/ScribeFeedManagement.conf | 19 +++++ specs/ScribeFeedManagement.spec | 64 +++++++++++++++++ specs/ScribePoke.conf | 19 +++++ specs/ScribePoke.spec | 71 +++++++++++++++++++ specs/ScribeToll.conf | 19 +++++ specs/ScribeToll.spec | 120 ++++++++++++++++++++++++++++++++ 8 files changed, 449 insertions(+) create mode 100644 specs/ScribeAuth.conf create mode 100644 specs/ScribeAuth.spec create mode 100644 specs/ScribeFeedManagement.conf create mode 100644 specs/ScribeFeedManagement.spec create mode 100644 specs/ScribePoke.conf create mode 100644 specs/ScribePoke.spec create mode 100644 specs/ScribeToll.conf create mode 100644 specs/ScribeToll.spec diff --git a/specs/ScribeAuth.conf b/specs/ScribeAuth.conf new file mode 100644 index 0000000..a21b98a --- /dev/null +++ b/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": "200", + "parametric_contracts": ["Scribe"], + "prover_args": [ + "-depth 15", + "-mediumTimeout 300" + ] +} diff --git a/specs/ScribeAuth.spec b/specs/ScribeAuth.spec new file mode 100644 index 0000000..3ba24d3 --- /dev/null +++ b/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; +} diff --git a/specs/ScribeFeedManagement.conf b/specs/ScribeFeedManagement.conf new file mode 100644 index 0000000..2cc279e --- /dev/null +++ b/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": "200", + "parametric_contracts": ["Scribe"], + "prover_args": [ + "-depth 15", + "-mediumTimeout 300" + ] +} diff --git a/specs/ScribeFeedManagement.spec b/specs/ScribeFeedManagement.spec new file mode 100644 index 0000000..d5039d7 --- /dev/null +++ b/specs/ScribeFeedManagement.spec @@ -0,0 +1,64 @@ +// 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; +} + diff --git a/specs/ScribePoke.conf b/specs/ScribePoke.conf new file mode 100644 index 0000000..0f1b8e2 --- /dev/null +++ b/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": "200", + "parametric_contracts": ["Scribe"], + "prover_args": [ + "-depth 15", + "-mediumTimeout 300" + ] +} diff --git a/specs/ScribePoke.spec b/specs/ScribePoke.spec new file mode 100644 index 0000000..a32205c --- /dev/null +++ b/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; +} diff --git a/specs/ScribeToll.conf b/specs/ScribeToll.conf new file mode 100644 index 0000000..d95c7a7 --- /dev/null +++ b/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": "200", + "parametric_contracts": ["Scribe"], + "prover_args": [ + "-depth 15", + "-mediumTimeout 300" + ] +} diff --git a/specs/ScribeToll.spec b/specs/ScribeToll.spec new file mode 100644 index 0000000..5475ced --- /dev/null +++ b/specs/ScribeToll.spec @@ -0,0 +1,120 @@ +// SPDX-License-Identifier: BUSL-1.1 +// Certora Verification Language (CVL) specification for Scribe + +methods { + // Read functions + function read() external returns (uint256); + function tryRead() external returns (bool, uint256); + function readWithAge() external returns (uint256, uint256); + function tryReadWithAge() external returns (bool, uint256, uint256); + function peek() external returns (uint256, bool); + function peep() external returns (uint256, bool); + function latestRoundData() external returns (uint80, int256, uint256, uint256, uint80); + function latestAnswer() external returns (int256); + + // Toll management + function tolled(address) external returns (bool) envfree; + function bud(address) external returns (uint256) envfree; +} + +// ----------------------------------------------------------------------------- +// Manual Storage Management +// +// When verifying the following rules, calling `tolled(e.msg.sender)` returns a +// symbolic boolean that Certora does not automatically link to the actual +// `_buds` storage that the `toll` modifier checks. +// +// This is because the `toll` modifier uses inline assembly to read +// `_buds[msg.sender]`: +// let slot := keccak256(0x00, 0x40) +// let isTolled := sload(slot) +// +// This direct `sload` is not linked to the `tolled()` view function's return +// value in Certora's symbolic execution. As a result, rules using `tolled()` +// may fail because the prover treats them as independent symbolic values. +// +// Therefore, a `ghostBuds` ghost mapping is introduced that manually tracks +// the `_buds` via storage hooks. Note that rules should therefore use the +// `isTolled(address)` helper function instead calling `tolled(address)` +// directly on the contract. + +ghost mapping(address => uint256) ghostBuds { + init_state axiom forall address a. ghostBuds[a] == 0; +} + +hook Sstore currentContract._buds[KEY address who] uint256 newVal (uint256 oldVal) { + ghostBuds[who] = newVal; +} + +hook Sload uint256 val currentContract._buds[KEY address who] { + require ghostBuds[who] == val; +} + +definition isTolled(address who) returns bool = + ghostBuds[who] != 0; + +// ---------------------------------------------------------------------------- + +rule readRevertsIfNotTolled(env e) { + bool callerTolled = isTolled(e.msg.sender); + + read@withrevert(e); + + assert !callerTolled => lastReverted; +} + +rule tryReadRevertsIfNotTolled(env e) { + bool callerTolled = isTolled(e.msg.sender); + + tryRead@withrevert(e); + + assert !callerTolled => lastReverted; +} + +rule readWithAgeRevertsIfNotTolled(env e) { + bool callerTolled = isTolled(e.msg.sender); + + readWithAge@withrevert(e); + + assert !callerTolled => lastReverted; +} + +rule tryReadWithAgeRevertsIfNotTolled(env e) { + bool callerTolled = isTolled(e.msg.sender); + + tryReadWithAge@withrevert(e); + + assert !callerTolled => lastReverted; +} + +rule peekRevertsIfNotTolled(env e) { + bool callerTolled = isTolled(e.msg.sender); + + peek@withrevert(e); + + assert !callerTolled => lastReverted; +} + +rule peepRevertsIfNotTolled(env e) { + bool callerTolled = isTolled(e.msg.sender); + + peep@withrevert(e); + + assert !callerTolled => lastReverted; +} + +rule latestRoundDataRevertsIfNotTolled(env e) { + bool callerTolled = isTolled(e.msg.sender); + + latestRoundData@withrevert(e); + + assert !callerTolled => lastReverted; +} + +rule latestAnswerRevertsIfNotTolled(env e) { + bool callerTolled = isTolled(e.msg.sender); + + latestAnswer@withrevert(e); + + assert !callerTolled => lastReverted; +} From 23181edb5bb74a1038d7983d7b4ef7789bc60807 Mon Sep 17 00:00:00 2001 From: merkleplant Date: Wed, 18 Feb 2026 15:34:29 +0100 Subject: [PATCH 2/3] lint --- specs/ScribeFeedManagement.spec | 1 - 1 file changed, 1 deletion(-) diff --git a/specs/ScribeFeedManagement.spec b/specs/ScribeFeedManagement.spec index d5039d7..78d434c 100644 --- a/specs/ScribeFeedManagement.spec +++ b/specs/ScribeFeedManagement.spec @@ -61,4 +61,3 @@ rule onlyLiftAndDropCanMutatePubKeys(method f, env e, calldataarg args, uint8 fe assert ghostPubKeysX[feedId] == pubKeyXBefore; assert ghostPubKeysY[feedId] == pubKeyYBefore; } - From 2aa3b730becb904b611fc2a03f10d7b24e8ffe1e Mon Sep 17 00:00:00 2001 From: merkleplant Date: Mon, 23 Feb 2026 13:50:37 +0100 Subject: [PATCH 3/3] ci: Remove lint and add specs/README --- .github/workflows/lint.yml | 23 -------------------- specs/README.md | 37 +++++++++++++++++++++++++++++++++ specs/ScribeAuth.conf | 4 ++-- specs/ScribeFeedManagement.conf | 4 ++-- specs/ScribePoke.conf | 4 ++-- specs/ScribeToll.conf | 4 ++-- 6 files changed, 45 insertions(+), 31 deletions(-) delete mode 100644 .github/workflows/lint.yml create mode 100644 specs/README.md diff --git a/.github/workflows/lint.yml b/.github/workflows/lint.yml deleted file mode 100644 index f2b986e..0000000 --- a/.github/workflows/lint.yml +++ /dev/null @@ -1,23 +0,0 @@ -name: Lint - -on: - push: - branches: - - main - pull_request: - -jobs: - tests: - runs-on: ubuntu-latest - steps: - - uses: actions/checkout@v3 - with: - submodules: recursive - - - name: Install Foundry - uses: foundry-rs/foundry-toolchain@v1 - with: - version: nightly - - - name: Check formatting - run: forge fmt --check diff --git a/specs/README.md b/specs/README.md new file mode 100644 index 0000000..e204d85 --- /dev/null +++ b/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= +``` + +### 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 +``` diff --git a/specs/ScribeAuth.conf b/specs/ScribeAuth.conf index a21b98a..860418f 100644 --- a/specs/ScribeAuth.conf +++ b/specs/ScribeAuth.conf @@ -10,10 +10,10 @@ "packages": [ "chronicle-std=lib/chronicle-std/src" ], - "solc_optimize": "200", + "solc_optimize": "10000", "parametric_contracts": ["Scribe"], "prover_args": [ "-depth 15", - "-mediumTimeout 300" + "-mediumTimeout 1800" ] } diff --git a/specs/ScribeFeedManagement.conf b/specs/ScribeFeedManagement.conf index 2cc279e..e10855d 100644 --- a/specs/ScribeFeedManagement.conf +++ b/specs/ScribeFeedManagement.conf @@ -10,10 +10,10 @@ "packages": [ "chronicle-std=lib/chronicle-std/src" ], - "solc_optimize": "200", + "solc_optimize": "10000", "parametric_contracts": ["Scribe"], "prover_args": [ "-depth 15", - "-mediumTimeout 300" + "-mediumTimeout 1800" ] } diff --git a/specs/ScribePoke.conf b/specs/ScribePoke.conf index 0f1b8e2..09c7a68 100644 --- a/specs/ScribePoke.conf +++ b/specs/ScribePoke.conf @@ -10,10 +10,10 @@ "packages": [ "chronicle-std=lib/chronicle-std/src" ], - "solc_optimize": "200", + "solc_optimize": "10000", "parametric_contracts": ["Scribe"], "prover_args": [ "-depth 15", - "-mediumTimeout 300" + "-mediumTimeout 1800" ] } diff --git a/specs/ScribeToll.conf b/specs/ScribeToll.conf index d95c7a7..bf224d3 100644 --- a/specs/ScribeToll.conf +++ b/specs/ScribeToll.conf @@ -10,10 +10,10 @@ "packages": [ "chronicle-std=lib/chronicle-std/src" ], - "solc_optimize": "200", + "solc_optimize": "10000", "parametric_contracts": ["Scribe"], "prover_args": [ "-depth 15", - "-mediumTimeout 300" + "-mediumTimeout 1800" ] }