What I was trying to model
In Midas, the contract reads block.timestamp directly in several places:
Relevant Solidity snippets:
require(block.timestamp - _lastUpdatedAt > 1 hours, "CAG: not enough time passed");
require(_dataTimestamp < block.timestamp, "CAG: timestamp >= now");
return applyGrowth(_answer, _growthApr, _timestampFrom, block.timestamp);
I wanted to model this directly in verity_contract, instead of threading the block timestamp in manually as an explicit function argument.
Why I could not do it
There is a real core accessor in Verity/Core.lean:
def blockTimestamp : Contract Uint256 :=
fun state => ContractResult.success state.blockTimestamp state
However, the verity_contract bind-source whitelist rejects it.
Source: https://github.com/lfglabs-dev/verity/blob/main/Verity/Macro/Translate.lean#L1476-L1478
The allowed bind sources include msgSender and msgValue, but not blockTimestamp.
There is also a placeholder in Contracts/Common.lean:
def blockTimestamp : Uint256 := 0
Minimal repro
verity_contract BlockTimeTest where
storage
x : Uint256 := slot 0
function nowish () : Uint256 := do
let t ← Verity.blockTimestamp
return tThis fails with:
unsupported bind source; expected getStorage/getStorageAddr/...
What is missing
Executable verity_contract support for binding blockTimestamp in the same style as msgSender / msgValue, so contracts can directly model block.timestamp reads from Solidity.
Why this matters
Without this, contracts that naturally depend on ambient block time have to add an extra explicit timestamp parameter just to be expressible/provable, which breaks source-level fidelity and changes the function shape relative to Solidity.
What I was trying to model
In Midas, the contract reads
block.timestampdirectly in several places:applyGrowth: https://github.com/midas-apps/contracts/blob/main/contracts/feeds/CustomAggregatorV3CompatibleFeedGrowth.sol#L404-L410Relevant Solidity snippets:
I wanted to model this directly in
verity_contract, instead of threading the block timestamp in manually as an explicit function argument.Why I could not do it
There is a real core accessor in
Verity/Core.lean:However, the
verity_contractbind-source whitelist rejects it.Source: https://github.com/lfglabs-dev/verity/blob/main/Verity/Macro/Translate.lean#L1476-L1478
The allowed bind sources include
msgSenderandmsgValue, but notblockTimestamp.There is also a placeholder in
Contracts/Common.lean:Minimal repro
verity_contract BlockTimeTest where storage x : Uint256 := slot 0 function nowish () : Uint256 := do let t ← Verity.blockTimestamp return tThis fails with:
What is missing
Executable
verity_contractsupport for bindingblockTimestampin the same style asmsgSender/msgValue, so contracts can directly modelblock.timestampreads from Solidity.Why this matters
Without this, contracts that naturally depend on ambient block time have to add an extra explicit timestamp parameter just to be expressible/provable, which breaks source-level fidelity and changes the function shape relative to Solidity.