From 4d263b5f54cc3815b603ccca7f7352f289b8e8ab Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jakub=20Kopa=C5=84ski?= Date: Thu, 22 Aug 2024 16:17:07 +0200 Subject: [PATCH] Explicitly match none case --- Clear/PrimOps.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Clear/PrimOps.lean b/Clear/PrimOps.lean index 319934a..12ff0d4 100644 --- a/Clear/PrimOps.lean +++ b/Clear/PrimOps.lean @@ -50,12 +50,12 @@ def primCall (s : State) : PrimOp → List Literal → State × List Literal | .Sar, [a,b] => (s, [UInt256.sar a b]) | .Keccak256, [a,b] => match s.evm.keccak256 a b with - | .some (val, evm') => (s.setEvm evm', [val]) + | .some a => (s.setEvm a.snd, [a.fst]) -- This is the hash collision case. It's essentially an unrecoverable -- error, and we model it similar to how we model infinite loops, except we -- put the error in the EVM instead, so we don't have to bother with it in -- the interpreter. - | _ => (s.setEvm s.evm.addHashCollision, [0]) + | .none => (s.setEvm s.evm.addHashCollision, [0]) | .Address, [] => (s, [s.evm.execution_env.code_owner]) | .Balance, [a] => (s, [s.evm.balanceOf a]) | .Origin, [] => (s, [s.evm.execution_env.sender]) @@ -129,7 +129,7 @@ lemma EVMByte' : primCall s .Byte [a,b] = (s, [UInt lemma EVMShl' : primCall s .Shl [a,b] = (s, [Fin.shiftLeft b a]) := rfl lemma EVMShr' : primCall s .Shr [a,b] = (s, [Fin.shiftRight b a]) := rfl lemma EVMSar' : primCall s .Sar [a,b] = (s, [UInt256.sar a b]) := rfl -lemma EVMKeccak256' : primCall s .Keccak256 [a,b] = match s.evm.keccak256 a b with | .some (val, evm') => (s.setEvm evm', [val]) | _ => (s.setEvm s.evm.addHashCollision, [0]) := rfl +lemma EVMKeccak256' : primCall s .Keccak256 [a,b] = match s.evm.keccak256 a b with | .some a => (s.setEvm a.snd, [a.fst]) | .none => (s.setEvm s.evm.addHashCollision, [0]) := rfl lemma EVMAddress' : primCall s .Address [] = (s, ([s.evm.execution_env.code_owner] : List Literal)) := rfl lemma EVMBalance' : primCall s .Balance [a] = (s, [s.evm.balanceOf a]) := rfl lemma EVMOrigin' : primCall s .Origin [] = (s, ([s.evm.execution_env.sender] : List Literal)) := rfl