Enhancing security, tests, gas optimisations, etc. - #114
Merged
Merged
Conversation
Neither coordinate of a point on the P256 curve can be zero, so a key with a zero component can never verify a signature. A wallet deployed with one is unusable for its whole life, and it still consumes its device identifier and its registeredP256Keys entry, neither of which can be released today. Both deploy paths accepted such a key: the admin batch through _createAccountForUser, and the permissionless createAccount. C-13
bytes32 is a fixed-size type, so bytes32(0).length is the constant 32 and both requires were unconditionally true. They never rejected anything. This function is the documented off-chain pre-check for the userop deploy path, so it has to reject exactly what the deploy path now rejects. C-13
Each test fails at e77b997 with "next call did not revert as expected", which is the defect: a zero key was accepted and a permanently unusable wallet was deployed against a consumed device identifier. Asserts registry state after the revert rather than the return value, so an identifier or key hash that leaked through would still be caught. C-13
None of the four had a constructor, so anyone could call initialize on the implementation address and own it, and on either factory also make it deploy an UpgradeableBeacon under their control. The proxies are unaffected, since they hold their own storage, and OZ v5 already blocks the implementation-bricking route by making upgradeToAndCall onlyProxy. This closes the invariant the upgrades tooling relies on and removes a trap for any later upgrade that adds an outward call not keyed on a proxy address. Written as _disableInitializers() rather than the OZ v4 constructor() initializer idiom that was commented out at these lines, matching Account4337. C-16
Each test deploys the implementation the way the deploy script does, with no proxy in front, and calls initialize as an unrelated account. All four fail at 2599a02 with "next call did not revert as expected", which is the defect. Asserts owner and beacon state after the revert, so an initialize that partly succeeded would still be caught. C-16
renounceOwnership was inherited unoverridden on all five Ownable-derived contracts, and on each one it is unrecoverable. On ESIMWallet it zeroes owner() while deviceWallet still points at the old device wallet. sendETHToDeviceWallet then fails its own zero-owner check and DeviceWallet._addESIMWallet can never accept the wallet again, so the ETH held there can only ever leave through buyDataBundle to the vault. On the four UUPS singletons the owner is the only caller _authorizeUpgrade accepts, and for both factories it is also the only route to beacon.upgradeTo. Renouncing freezes the contract, or every wallet under its beacon, on the current logic with no way back. Ownable2Step does not help here because it guards transfer, not renouncement, which stays a single call. C-09
One test per contract, each asserting the specific selector and then that the owner is still the address it was before the call. The eSIM wallet case goes through DeviceWallet.execute rather than pranking the device wallet directly, because that is the route that actually reaches renounceOwnership in production: the owner is a contract, not a key, and the only way it calls anything is through the EntryPoint. The two factory cases also assert the beacon is still owned by its factory, since that is what the renouncement would have stranded. C-09
_secureTransferOwnership emitted OwnershipTransferred itself right after _transferOwnership, which already emits it. previousOwner was captured before the call and owner() read after, so both logs carried identical arguments and were indistinguishable to any consumer. An indexer replaying them would count one transfer as two. Dropped previousOwner along with the emit, since that was its only use. C-19
Counts matching logs from vm.getRecordedLogs rather than using vm.expectEmit. expectEmit matches a single occurrence and passes unchanged against a duplicate emission, so it cannot detect the defect this covers. Fails at d3b0e1f with 2 != 1. C-19
switchESIMIdentifierToNewDeviceIdentifier was the only mutator in this contract without an isLazyWalletDeployed check. batchPopulateHistory and deployLazyWalletAndSetESIMIdentifier both carry one. Two separate divergences were reachable. Switching away from a deployed device left its eSIM wallet onchain, still owned by that device wallet, while the switch deleted the device's purchase history. Switching onto a deployed device orphaned the eSIM, because deploying that device a second time is already refused, so the eSIM would never receive a wallet under it. Nothing reads the lazy registry after deployment, so neither state can be repaired. No capability is lost. Moving an eSIM after deployment is what ESIMWallet.requestTransferOwnership and acceptOwnershipTransfer are for. The error carries the offending identifier so the caller can tell which of the two devices blocked the switch. C-11
One test per direction, each asserting the identifier binding and the purchase history are untouched after the revert rather than only that it reverted. Both fail at 43bdcd0 with the call not reverting. C-11
Registry.initialize checked eSIMWalletAdmin, vault, upgradeManager and entryPoint for zero but let both factory addresses through unchecked. Neither deviceWalletFactory nor eSIMWalletFactory has a setter anywhere in the protocol, so a zero written at deploy time is permanent: the lazy wallet deployment path calls into address(0), onlyDeviceWalletFactory can never match a sender, and the factory branch of the eSIM wallet factory's caller check is unreachable. The only recovery is an upgrade. The new ZeroAddress error carries the parameter name because the initializer checks several addresses and a bare error would not say which one failed. C-18, F-20
Each revert test names the ZeroAddress selector along with the parameter name, so a guard that fires for the wrong argument still fails. Both tests report "next call did not revert as expected" against the parent commit. The third test asserts the registry still records both factories on the intended deployment, so a guard that rejects valid input would show up too. C-18
Registry.initialize accepted a P256Verifier and never stored it, passing it only to the RegistryInitialized event. Callers could reasonably read the parameter as the registry adopting a verifier, when the canonical copy lives in DeviceWalletFactory.verifier, is written once by that contract's initializer and has no setter. Storing a second copy was the alternative and was rejected: both live proxies are already initialized, so a new slot would read zero on chain forever unless a reinitializer or an owner setter came with it, and the protocol would then hold two verifier addresses that can diverge. The event loses its last field with the parameter, so anything offchain decoding RegistryInitialized needs updating. Deployed proxies are unaffected, having already run initialize. C-18, F-20
deployESIMWallet takes the owner as a parameter unrelated to msg.sender, so any registered device wallet could name a different one. That creates an eSIM wallet owned by a device wallet that never asked for it, is not recorded by _addESIMWallet or by the registry, and sits at the CREATE2 address the named owner would have used for that salt, so its own deployment then fails with no reason attached. The registry and the device wallet factory legitimately deploy on behalf of a device wallet, so the restriction applies only to the branch of the caller check that admits a device wallet directly. DeviceWallet already passes address(this), so no existing caller changes. C-20, F-22
The revert test names the OnlyDeployForSelf selector and then has the named device wallet deploy at the same salt, so the test also shows the refused call left that address free. It reports "next call did not revert as expected" against the parent commit. The third test records that one salt with two different owners already resolves to two addresses, because the owner sits in the encoded initialize call, which is a constructor argument and therefore part of the CREATE2 init code. It passes against the parent commit too, which is the point: the backlog described this property as the fix, and it already held. C-20
verifySignature skipped 13 bytes from challengeIndex without checking that they were the challenge key, then read to the next quote. Since challengeIndex comes from the caller alongside the signature, an assertion made for a different challenge passed whenever the client data carried the expected base64url value in any other quoted field. The origin is the obvious carrier, and a relying party the user's key has ever signed for can put an arbitrary string there. Three malformed inputs also panicked instead of returning false: authenticatorData shorter than 33 bytes was indexed for its flags byte, and typeIndex or challengeIndex near the maximum overflowed the offset addition. This function sits inside ERC-4337 validation and behind isValidSignature, where a revert is not a rejection: the bundler drops the operation and an ERC-1271 caller sees a failure rather than an invalid signature. The typeIndex bound goes beyond the cited lines deliberately. It is the same defect as the authenticatorData one and runs before every guard added here, so without it the panic stays reachable through the other index. Solady's slice clamps both ends, so the slices themselves need no bounds check once the indices are inside the JSON. C-08, F-07, F-18
Against the parent commit all five fail, each for the reason its fix addresses: two array out-of-bounds panics, two arithmetic overflow panics, and the challenge replay reaching P256 verification at 229,972 gas against a 50,000 bound. The replay test needs that gas bound because both outcomes are false. It builds client data committing to one challenge while carrying the expected base64url value at the end of its origin, so before the fix the value matched and verification ran on to the signature. Where it stopped is the only observable difference, and gas is what shows it. A test that accepts a forged assertion outright would need a P256 signature over crafted client data, which needs an offchain signer. test_isValidSignature in DeviceWallet.t.sol is the positive control: it carries a real assertion from a device and still passes, so the new key check agrees with what authenticators actually emit. C-08
The factory only rejected a zero coordinate. A non-zero pair off the curve still deployed a wallet, and FCL_ecdsa.ecdsa_verify rejects such a key before it does anything else, so no signature could ever validate for that wallet. It would still hold its device identifier and key hash, neither of which the protocol can release, so the identifier is burned permanently. ecAff_isOnCurve is the same predicate verification applies, so the deploy paths and the signature path now agree exactly. It also covers coordinates at or above the field prime, which the zero check let through. Runtime size 16,469 to 16,702 bytes, margin 7,874.
Each of the four tests fails at the parent commit with "next call did not revert as expected": (1, 1) and a coordinate at the field prime both deployed a wallet before. The batch path also asserts that neither the identifier nor the key hash was recorded in the registry.
removeESIMWallet called the wallet it was removing before clearing isValidESIMWallet and canPullETH, so during that call the wallet still passed onlyAssociatedESIMWallets and could pull the device wallet's ETH through pullETH. All eSIM wallets share one upgradeable beacon with no per-wallet opt-out, so the logic reached by that callback is not fixed for the life of the protocol. The state and registry writes now happen first, and the function carries nonReentrant as a second layer. The two eSIM wallet paths could not both take the guard. requestTransferOwnership calls removeESIMWallet, which calls back into sendETHToDeviceWallet on the same contract, so guarding both makes the callback revert into removeESIMWallet's try/catch, which swallows it and strands the wallet's ETH with no error. The guard goes on requestTransferOwnership, which is the one with a state write after the call. sendETHToDeviceWallet writes no state of its own and only the owner can call it to move ETH to itself, so re-entering it gains nothing. requestTransferOwnership keeps its ordering. The registry refuses to clear the association of a wallet that already has a pending request, so writing newRequestedOwner first would make the removal revert. Slither drops five reentrancy findings, 154 to 149, with nothing new.
The suite had no reentrancy test at all. A handler etched over a valid eSIM wallet re-enters pullETH from inside its own removal. At the parent commit it drains 1 ETH from the device wallet; now it finds itself already unbound and already stripped of ETH access, and pullETH reverts with OnlyAssociatedESIMWallets into the caller's try/catch.
The caller check accepted any associated eSIM wallet regardless of which one was named, so one of them could unbind a sibling, clear its ETH access, put it on standby and force its whole balance back to the device wallet. All eSIM wallets share one upgradeable beacon, so a wallet's logic is not fixed for the life of the protocol. The association of the named wallet is still established by removeESIMWallet itself, which requires isValidESIMWallet before doing anything, so the check no longer needs to test the caller's own association.
Fails at the parent commit with "next call did not revert as expected". Also asserts the sibling keeps its binding and its ETH, and that a wallet removing itself still works.
The wallets are still built against the v0.7 EntryPoint, two releases behind. v0.8 is as far as we can go: gas sponsorship in the SDK runs through a paymaster that supports v0.6 through v0.8 and has no v0.9 implementation, so a v0.9 target would leave sponsored operations with nothing to pay them. The bundler side already handles v0.9, and that is what earlier notes wrongly recorded as the ceiling. Two source changes come with the bump. TokenCallbackHandler moved from samples/callback to accounts/callback, and IEntryPoint gained senderCreator(), which the EntryPoint mock has to implement now that it declares the full interface. The mock returns the zero address because nothing in the suite exercises sender creation. Nothing onchain changes yet. Each wallet reads its EntryPoint from an immutable set at deployment, so the live wallets keep talking to v0.7 until a new implementation is deployed and the beacon is pointed at it. Storage layouts are identical for all seven contracts, forge and hardhat still emit byte-identical bytecode, and the suite is unchanged at 139 passing.
The registry treats both the device identifier and the P256 key hash as one-to-one with a wallet, but nothing enforced it at the point of write. The two deploy paths check first, so they were fine. postCreateAccount does not: its only guard is that the wallet address has no record yet, which says nothing about the identifier or the key being free. An admin passing an identifier that already belongs to another wallet therefore repointed it silently. The original wallet kept its owner key but lost the identifier, and could never be redeployed against it again, because the deploy path compares the registered wallet with the address the identifier and key hash to. Reusing a key had the mirror effect: the key stopped resolving to the wallet that actually holds it. The check goes in the shared write rather than in postCreateAccount so that any future caller inherits it.
Both tests deploy two independent wallets, register the first, then have the admin try to register the second against the first's identifier and against its owner key. Each asserts the registry binding still points at the original wallet afterwards, not just that the call reverted. Both fail on the parent commit with the second registration succeeding.
validateUserOp returns packed validationData, not a bytes4, and the EntryPoint reads its low 160 bits as an authorizer. Returning 0xffffffff for a signature too short to hold a header and a challenge therefore named the aggregator 0x00000000000000000000000000000000ffffFFff, which does not exist. The EntryPoint would try to route the operation to it and revert the whole bundle rather than dropping the one bad operation. The two later returns in the same function already used SIG_VALIDATION_FAILED; only the length guard was inconsistent.
Asserts the returned validationData is exactly SIG_VALIDATION_FAILED and that its upper bits are clear, so the EntryPoint reads no validity window alongside the failure. Fails on the parent commit with 4294967295.
The only positive control for isValidSignature was an assertion captured from a real device. It cannot be moved to a different challenge: the challenge is base64url encoded inside the clientDataJSON that the P256 signature covers, and the private key that signed it is not in this repo. Anything that changes how the challenge is derived therefore had no way to be tested. A small node script signs an assertion for a challenge the test picks, using a fixed test key pair, and a library drives it through vm.ffi. It runs the full onchain path, so both the challenge comparison and the P256 verification are real. The captured assertion stays. It is the only evidence the onchain checks agree with what authenticators actually emit, which a self-signed fixture cannot show.
The admin could only ever nominate its own replacement, so a key in someone else's hands could not be removed by anybody. That key also holds pause, and the owner holds the release, which looked like a safe split until you notice the key can simply pause again. The two sides trade transactions and the attacker wins, because the one call that would end it needed the attacker to sign. requestAdminUpdate is the owner's now. A nomination also strips the incumbent at once, so the role goes dormant rather than being shared while a handover is outstanding, and naming the incumbent withdraws the nomination and hands its powers back for a call sent in error. disableAdmin and enableAdmin are the same lever without a replacement ready. Suspending leaves the address on the books and answers zero from the accessor every gate in the protocol already reads, so one write closes all of them and no reader needed editing. Restoring is deliberately owner only and has no fast route: a key that could be handed back as quickly as it was taken away would recreate the deadlock this exists to break. adminOfRecord keeps slot 60 and adminDisabled packs into the spare bytes beside paused, so nothing moves. Rotation and suspension move out of Registry.t.sol into their own file, and the campaign's rotation handler moves to the upgrade manager, which is the actor that now performs it. The config invariant is restated: the accessor may read zero, what must never happen is the address itself going missing, since both routes back go through it.
The guardian could release a pause but not stop the key that applies one, so its release only held until the next block. Suspending the admin is what makes unpauseInstantly stick, and it is the same shape as the other two powers: it takes something away and hands nothing out. Reinstating is not offered here. A guardian able to hand a suspended key its powers back would beat the owner's scheduled restore every time and rebuild the same unwinnable race one level up, and one able to appoint an admin would reach buyDataBundle and every wallet holding ETH access. Both stay with the owner, where they wait. disableAndNominate is the replacement path and is not a fast route. It carries no role and only the timelock can call it, so it is scheduled like any other change. It exists because the two effects belong in one operation and a reviewer should be able to read that off the name rather than infer it from a payload.
The admin address and the power attached to it are separate facts now, and the handover rule read the accessor, which also goes to zero on a suspension and on a nomination. It would have failed on disableAdmin for a reason that has nothing to do with the address moving. Two rules added for the half that was lost: the power never lands on an address that is not on the books, and a suspended or handed over admin cannot act. The second is what every gate in the protocol relies on. Both new views read storage only and never the environment, so they are envfree and pass the static check. Not re-run against the prover yet.
Every admin gated path costs a little more, because the accessor reads two slots where the gate used to read one. Two figures fall instead: pullETH and a buyDataBundle that needs no top up both check the pause after an admin check, and the accessor now warms the slot paused sits in, so they pay for it once rather than twice. Storage layout moves by one entry. adminOfRecord is the old admin slot under a new name and adminDisabled packs beside paused, so no variable shifts.
The ceiling limits what the admin may charge a wallet for one data bundle, and only the owning device wallet can set it. Every other authority marker is re-decided when a wallet changes hands: the incoming device wallet's addESIMWallet call sets isValidESIMWallet and canPullETH, and bindESIMWallet follows on the registry. The ceiling crossed unexamined, so a wallet handed over carrying a raised one left its new owner bound to a figure the last owner chose, with nothing saying so. It now goes back to zero with the owner, which hands the wallet to the registry default until the new owner sets one of its own. Written only on a change, so an ordinary handover of a wallet that never set a ceiling emits nothing. The Certora rule that said the ceiling moves only through its setter is restated: the setter is still the only writer of a value, and a handover may only clear it.
bindESIMWallet decided whether an address belonged to the protocol by asking that address. Both checks read owner() and newRequestedOwner() off the target, and any contract can answer those however its author likes, so a device wallet owner could write an address of their choosing into isESIMWalletValid and have the protocol treat it as one of its own. The factory is the one party that can state this, and its isESIMWalletDeployed mapping had no onchain consumer until now. The second half is what made it worth closing. DeviceWallet's identifier setter checks that the registry knows the target rather than that this device wallet holds it, so a non-zero entry left by an unrelated device wallet let the admin make any device wallet in the protocol call into the attacker's contract. Only real eSIM wallets reach the mapping now, so that path lands on a wallet whose own guard refuses the caller. The cross-contract spec gains a NONDET summary for the new call. It leaves the three contracts in the scene, and an unsummarised one would havoc the storage the rules read.
Binding an eSIM wallet costs 1,553 more, measured as an exact per-wallet figure on the batch of 5 and the batch of 18. Accepting an eSIM wallet handover costs 2,116 more for the cold read of the ceiling slot.
isLazyWalletDeployed asked the registry whether a device identifier had a wallet, so it was already true for a device deployed through the ordinary route. The name said lazy and misled every reader of the three call sites. It moves onto the registry, which owns the fact, as isDeviceIdentifierAlreadyUsed. The two history helpers were also hard to tell apart. One moves the purchase entries, the other moves the membership record saying the eSIM exists, and a switch needs both, so they are now named for that.
The lazy registry checked the registry before it accepted work, but the ordinary route never checked back. Deploying a device wallet under an identifier that already had lazy records left that user with no way out: their eSIM wallets cannot be deployed, their purchases cannot be copied, and the eSIMs cannot be moved to a clean device either, because all three paths refuse an identifier that has a wallet. Every eSIM bound to it was stranded protocol-wide, recoverable only by an upgrade. Both admin-facing entry points on the factory now ask the registry, which forwards to the lazy registry. The lazy route reaches the same code through the registry and is deploying against its own reservation, so it is told apart by the sender rather than by a new argument. createAccount is left alone: it runs inside ERC-4337 validation, where reading another contract's storage is barred, and postCreateAccount is where that route gets checked. The continuation test asserted a state this closes. It kept the part that still holds, that the deploy cursor rather than the registry record is what says a lazy device was started.
An eSIM wallet's own identifier slot was set once, but nothing compared it against any other wallet. Two live wallets could carry the same eSIM identifier, one per deployment route, and nothing onchain could say which one held the eSIM. A lazy record could also form under an identifier a wallet already held, leaving purchases nobody could ever reach. The registry now keeps the identifier to wallet record and refuses a second claim. It sits there rather than on the device wallet because a device wallet can reach the registry directly through execute, so a guard on the wallet side would be skipped by doing exactly that. For the same reason the claiming device's own identifier is read from it rather than taken as an argument. A reserved identifier is refused for every device but the one that reserved it, which is what lets the lazy route claim what it set aside without a separate route flag. The lazy side refuses a new binding under an identifier already held onchain. The new mapping sits with the other registration records, so Registry's own state moves down one slot. The gap stays at 50: the protocol is being redeployed rather than upgraded.
Nine cases in one file, beside the salt collision tests, since this is the same kind of cross-route problem. Six of them fail on the code as it stood before the guards, checked by stripping the guard call sites and leaving the errors in place so the file still compiled. The regression cases carry as much weight as the refusals. A guard that also refuses the lazy route deploying against its own reservation would be worse than no guard, and that is the most likely way to break either of these.
The campaign drew device identifiers for the two deployment routes from namespaces that never overlap, so a cross-route invariant would have held over a state no sequence reaches. Both routes can now draw from a pool of eight, chosen per call, and the campaign gained the missing action: the ordinary route writing an eSIM identifier onto a wallet, which until now only the lazy deployment ever did. Two invariants on top of that, one per collision, plus a fuzz case sweeping both route orders and asserting exactly one of them takes the identifier. Exactly one matters in both directions: two would mean the collision is back, none would mean a guard refusing the legitimate first claim. Both invariants were checked against the guards removed and both go red, so neither is passing by never reaching the state it describes.
Two rules on the registry: the claim is write-once, and only a device wallet makes one, through the one entry point. The second is parametric for the same reason the device wallet validity rule is. The claim is reachable directly rather than only through DeviceWallet, so its own gate is the whole of the access control and a second writer added later fails here without anyone remembering to extend a test. The cross-contract spec gains three summaries. Two are the reservation reads the registry makes on the lazy wallet registry, whose address comes from a storage field, which is the shape the unresolved external line never reaches: the selector is known and only the callee is not, so the prover would pick a havoc scoped to everything but the caller and rewrite the contracts a rule reads. The third is the device identifier the registry reads off its caller, which is the scene's device wallet whenever that wallet is the one claiming. Unrun. The prover jobs for the registry, the eSIM wallet and the cross contract spec were already owed from the previous fixes, and the device wallet and factory specs join them.
An eSIM wallet deployment went from about 460,000 gas to about 500,000, so a full batch of twenty is 10,025,567 rather than 9,278,724. Both figures are quoted as the justification for the batch cap, so both were wrong the moment the identifier claim landed. The cap and the bound are unchanged: the point of the bound is retry cost, and instrumented coverage runs still fit inside it.
Registry's own state starts one slot later, both baselines move with the new checks, and the docs pick up the new views and errors.
Revoking an eSIM wallet's right to pull ETH is onlySelf, so it costs a signature from the user's P256 key. Granting cost nothing: deployESIMWallet is onlyESIMWalletAdmin and took the flag as a caller argument, and addESIMWallet accepted it from the registry and the factory too. A user who signed a revocation had it undone by the admin deploying a second wallet with the flag set, and the whole device wallet balance was reachable again through a wallet the user never asked for. _addESIMWallet now refuses the flag outright. It is the single funnel both public binders reach, so there is no second place to forget. Passing true reverts ETHAccessNotGrantableAtBind rather than being quietly downgraded, from every caller including the device wallet itself, so a caller that believes it granted access finds out at the call. Both bool parameters stay on the ABI with false as their only valid value, and toggleAccessToETH is the only way access is ever granted. The write below the guard is false rather than left alone. The slot is already provably false on arrival, since removeESIMWallet is the only unbind and it zeroes both flags, but writing it makes the property readable in one function instead of resting on another staying correct. The lazy route and the ordinary batch both passed true on every onboarding and now pass false. The first data bundle paid out of the device wallet's balance waits on the user signing a grant; until then the admin covers the price with msg.value or sends ETH straight to the eSIM wallet.
Five cases in the device wallet ETH file, which already owns every path ETH takes into and out of a device wallet, so nothing new was needed. Four of them go red against the code as it stood: the admin granting at deploy time, the device wallet granting at bind time, the revocation the admin could undo, and a fresh wallet arriving with access down both deploy routes. The fifth is the other side of the change, the owner granting after the bind and the purchase then going through, and stays green either way. One fuzz case draws the caller across the four the bind paths admit and a fifth they do not. Access control runs first, so an unauthorised caller is turned away before the flag is looked at and the authorised ones are refused on the flag itself; the wallet ends up without the access either way. Five fixtures grant explicitly now. Granting there keeps the ripple inside the fixture instead of spreading through every test that pulls ETH. The rest of the changes are assertions following the deploy paths, which no longer hand out access. The gas file loses its third-wallet-with-ETH-access row. It measured the difference between a true and a false deploy and that difference is gone; the grant already has a row of its own.
The new invariant says a pair holding the right to pull ETH has a recorded grant behind it. The ghost is keyed by the device wallet and the eSIM wallet together, so a wallet that moves does not read as carrying the first device wallet's grant, and both the current holder and the last one are checked since the two differ while a transfer is outstanding. Two handler actions needed fixing first. addESIMWallet passed true and asserted the access afterwards, so it would have reverted on every draw, and the distribution check requires each action to reach its share of successes. deployESIMWalletForDevice drew the flag and would have reverted on half. The grant is recorded in ghost state rather than asserted in the handler body. With fail_on_revert off, an assertion that trips inside a handler reverts the call and the campaign reads it as a skipped action rather than a failure.
One rule saying canPullETH moves from false to true only under toggleAccessToETH. Stated over the whole method set rather than over the two bind paths, so a later function that writes the flag has to answer it too. The caller check is not restated in the rule. It belongs to onlySelf and is what the rule leans on rather than what it proves. Single contract, so no out-of-scene summaries are needed. Not run yet. This spec already owed the prover a run for a changed contract and now owes one for a new rule as well.
Every bind is 19,913 gas cheaper, because it now writes false to a slot that is already zero instead of paying a cold SSTORE. toggleAccessToETH grant picks up the same amount, so the cost has moved to the call that actually asks for the access rather than disappearing. A batch of five is exactly five times 19,913 cheaper, and the lazy batches scale the same way.
Several dev blocks restated the same point across two or three sentences, or explained the consequence twice. Cut to what a reader needs, keeping the reasoning that is not visible in the code.
Registry.initialize gained a data bundle price cap parameter, so the six argument selector in the filter matched nothing and the spec failed to typecheck.
newRequestedAdmin, paused and adminDisabled share slot 64, so accepting a handover compiles to a masked read-modify-write. Integer arithmetic cannot evaluate the mask and reports a nomination surviving that never did. This conf runs that one rule with bit vectors, where it verifies.
…evice wallet The transfer request rule failed on requestTransferOwnership for two reasons that hid each other, so fixing either one alone left it failing. The dispatch list was empty, and the default case runs no code. removeESIMWallet resolved to a no-op that reported success, so the removal branch ran and wrote nothing, which read as a device wallet still holding a wallet it had just let go. The list now names the five calls on that path. It deliberately stops there: a complete list of every call between the three contracts turned each call inside execute, whose target and calldata are both arbitrary, into a case split over all twenty-five signatures, and that run segfaulted after a hundred and three minutes with no report. requireLinkedScene never tied the eSIM wallet's own deviceWallet field to the device wallet in the scene. The getter was declared and used nowhere. A conf link binds the address but does not stop the prover summarising a call made through it, so the removal could land on a contract no rule reads while the scene's device wallet kept holding the wallet. Four rules over 94 methods, zero assert failures.
The full cross contract spec is four rules over 94 methods and takes about twenty minutes, which is too slow to iterate on a summarisation problem. This narrows the scene to one rule against one method and returns in about ninety seconds, on the same links and packages so the result carries over. Note that method must be contract qualified when the scene holds more than one contract, or the local typechecker rejects it and certoraRun still exits zero.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.