Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Governor

Showcase port of OpenZeppelin-style governance (Governor, TimelockController, ERC20Votes) under examples/governor/ in cambrian-lang. Targets EVM with deterministic CREATE2; Lean project file is project.lean.yaml.

Do not expect a line-for-line OZ clone — see the repo README.md / PLAN.md for intentional simplifications (snapshot-free voting, single-target proposals, fixed quorum, …).

Layout

examples/governor/
  project.yaml              # target: evm
  project.lean.yaml
  ERC20Votes.cam            (+ .test / .fuzz / .invariant / .multi.invariant)
  TimelockController.cam    (+ .test / .invariant)
  Governor.cam              (+ .test / .fuzz / .invariant / .multi.invariant)
  ref/                      # vendored OZ reference
  build/                    # generated EVM project (gitignored)
  build-lean/               # generated Lean project (gitignored)

The *.multi.invariant.cam files hold multi-entity invariants and are listed only in project.lean.yaml.

Entities

EntityShapeRole
ERC20VotesToken + votesgetVotes / transfers; feed for castVote
TimelockControllerSingletonSchedule / execute / cancel with role from
GovernorSingletonPropose → vote → queue → execute

Cross-contract handles use typed addresses:

#[factory_only]
constructor(token:    Address<ERC20Votes>,
            timelock: Address<TimelockController>,
            admin:    address,
            voting_period: u64,
            quorum_votes:  U256) => []

Idioms exercised

Phased var capture — read voting power, then tally only if weight is positive (Phased Routes):

castVote(proposal_id: U256, support: u8) => [
    read: [
        var weight = getVotes(msg::sender) ~> m_token;
    ]
    tally where weight > 0 : throw 100 : [
    ]
]

Role from on members — Timelock gates schedule / execute / cancel:

schedule(target: address, value: U256, data: CamData,
         predecessor: U256, salt: U256, delay: u64)
    from m_proposer : throw 1
    where delay >= m_min_delay : throw 2
=> []

execute(target: address, value: U256, data: CamData,
        predecessor: U256, salt: U256)
    from m_executor : throw 3
=> [
    ~> target with { value: value, data: data }
]

Unphased execute relies on EVM SSTORE-before-CALL so reentry cannot re-run a finished op.

Enums — ProposalState / OpState drive member transforms. hashOf(...) — proposal / operation ids → keccak256(abi.encode(...)) on EVM.

Build and test

# From the cambrian-lang repo root:
cargo run -p cambrian-transpiler --release -- \
    --project examples/governor/project.yaml

cd examples/governor/build
bash setup.sh
forge build
forge test -vv

# Lean (separate project file, output in build-lean/):
cambrian-transpiler --project examples/governor/project.lean.yaml
cd examples/governor/build-lean
lake build

The transpiler prints warnings while generating (among them an F7 note that fuzz.shrink in project.yaml has no effect); they don’t stop the build. The Foundry run passes all unit, fuzz and invariant suites.

Full commands and status live in examples/governor/README.md.