diff --git a/Benchmarks/Dss/Clipper/Common.lean b/Benchmarks/Dss/Clipper/Common.lean index c724380..f311dd1 100644 --- a/Benchmarks/Dss/Clipper/Common.lean +++ b/Benchmarks/Dss/Clipper/Common.lean @@ -479,6 +479,21 @@ theorem uInt256OfByteArray_word_toBytesBE (w : UInt256) : · rw [byteArray_toList_eq] · simpa using word_toBytesBE_toByteArray_size w +-- LIBRARY CANDIDATE: decode a `PUSH32` from local opcode/payload facts without reducing the +-- surrounding generated bytecode by definitional equality. +theorem decode_push32_of_get?_extract' {code : ByteArray} {pc w : UInt256} + (hget : code.get? pc.toNat = some 0x7f) + (hpayload : code.extract' (pc.toNat + 1) (pc.toNat + 33) + = ({ data := (EVM.Word.toBytesBE w).toArray } : ByteArray)) : + decode code pc = some (.Push .PUSH32, some (w, 32)) := by + unfold decode + rw [hget] + have hparse : parseInstr 0x7f = some (.Push .PUSH32) := by native_decide + simp [hparse, argOnNBytesOfInstr] + rw [show pc.toNat + 1 + 32 = pc.toNat + 33 by omega] + rw [hpayload] + rw [uInt256OfByteArray_word_toBytesBE] + theorem clipperPatchesStartAt (v : ClipperImmutables) : PatchesStartAt 1463 (patches v) := by unfold PatchesStartAt patches patchesFrom offsets immValues diff --git a/Benchmarks/Dss/Clipper/Ilk.lean b/Benchmarks/Dss/Clipper/Ilk.lean index 7089878..5449e5a 100644 --- a/Benchmarks/Dss/Clipper/Ilk.lean +++ b/Benchmarks/Dss/Clipper/Ilk.lean @@ -264,15 +264,16 @@ theorem clipperIlkPush32Decode (v : ClipperImmutables) {code : ByteArray} (hlen : bs.length = 32) : decode code (⟨6799⟩ : UInt256) = some (.Push .PUSH32, some (EVM.Word.ofNat (fromBytesBigEndian bs), 32)) := by - unfold decode - rw [patchRuntime_get?_disjoint hpatch - (by apply clipperIlkPatchesWindowDisjoint32 v; native_decide)] - change some (Operation.Push Operation.POp.PUSH32, - some (uInt256OfByteArray (code.extract' 6800 6832), 32)) = - some (Operation.Push Operation.POp.PUSH32, - some (EVM.Word.ofNat (fromBytesBigEndian bs), 32)) - rw [clipperIlkPatchPayload v hpatch hilk hlen] - rw [uInt256OfByteArray_word_toBytesBE] + exact decode_push32_of_get?_extract' + (pc := (⟨6799⟩ : UInt256)) (w := EVM.Word.ofNat (fromBytesBigEndian bs)) + (by + rw [patchRuntime_get?_disjoint hpatch + (by apply clipperIlkPatchesWindowDisjoint32 v; native_decide)] + native_decide) + (by + rw [show (⟨6799⟩ : UInt256).toNat + 1 = 6800 by native_decide] + rw [show (⟨6799⟩ : UInt256).toNat + 33 = 6832 by native_decide] + exact clipperIlkPatchPayload v hpatch hilk hlen) set_option maxHeartbeats 1000000 in theorem clipperIlkConstGetterWf (v : ClipperImmutables) {code : ByteArray} diff --git a/Benchmarks/Dss/Clipper/Vat.lean b/Benchmarks/Dss/Clipper/Vat.lean index 8387bd1..3e6cedb 100644 --- a/Benchmarks/Dss/Clipper/Vat.lean +++ b/Benchmarks/Dss/Clipper/Vat.lean @@ -348,14 +348,16 @@ theorem clipperVatPush32Decode (v : ClipperImmutables) {code : ByteArray} (hpatch : patchRuntime clipperBytecode (patches v) = some code) : decode code (⟨3144⟩ : UInt256) = some (.Push .PUSH32, some (EVM.Word.ofNat (↑v.vat : Nat), 32)) := by - unfold decode - rw [patchRuntime_get?_disjoint hpatch - (by apply clipperVatPatchesWindowDisjoint32 v; native_decide)] - change some (Operation.Push Operation.POp.PUSH32, - some (uInt256OfByteArray (code.extract' 3145 3177), 32)) = - some (Operation.Push Operation.POp.PUSH32, some (EVM.Word.ofNat (↑v.vat : Nat), 32)) - rw [clipperVatPatchPayload v hpatch] - rw [uInt256OfByteArray_word_toBytesBE] + exact decode_push32_of_get?_extract' + (pc := (⟨3144⟩ : UInt256)) (w := EVM.Word.ofNat (↑v.vat : Nat)) + (by + rw [patchRuntime_get?_disjoint hpatch + (by apply clipperVatPatchesWindowDisjoint32 v; native_decide)] + native_decide) + (by + rw [show (⟨3144⟩ : UInt256).toNat + 1 = 3145 by native_decide] + rw [show (⟨3144⟩ : UInt256).toNat + 33 = 3177 by native_decide] + exact clipperVatPatchPayload v hpatch) set_option maxHeartbeats 1000000 in theorem clipperVatConstGetterWf (v : ClipperImmutables) {code : ByteArray} diff --git a/Benchmarks/Dss/End/Dispatch.lean b/Benchmarks/Dss/End/Dispatch.lean index d88e9d1..0d704ea 100644 --- a/Benchmarks/Dss/End/Dispatch.lean +++ b/Benchmarks/Dss/End/Dispatch.lean @@ -759,6 +759,191 @@ theorem endLow2SplitWellFormed : dsimp [selectorSplitWellFormed] repeat' first | apply And.intro | native_decide +theorem endRootSplitTaken {ee : ExecutionEnv} {g : Sat256} {s0 : State} + {selWord : UInt256} {mem : ByteArray} {aw : UInt256} {rdata : ByteArray} + {acc : Batteries.RBSet AccountAddress compare × AccountMap} {k C : ℕ} + {rest : List UInt256} + (h : RD endBytecode ee g s0 endRootSplitPc (selWord :: rest) mem aw rdata acc k C) + (hb : UInt256.gt (armSelNat endBytecode endRootSplitPc) selWord ≠ ⟨0⟩) + (hov : rest.length + 3 ≤ 1024) : + RD endBytecode ee g s0 endLow1JumpdestPc (selWord :: rest) mem aw rdata acc + (k + 5) (C + 22) := by + exact RD.selectorSplitTakenResolved (tgt := endLow1JumpdestPc) (width := 2) + (op := .PUSH2) h endRootSplitWellFormed (by native_decide) (by native_decide) + (by native_decide) hb (by jump_dest) hov + +theorem endRootSplitNotTaken {ee : ExecutionEnv} {g : Sat256} {s0 : State} + {selWord : UInt256} {mem : ByteArray} {aw : UInt256} {rdata : ByteArray} + {acc : Batteries.RBSet AccountAddress compare × AccountMap} {k C : ℕ} + {rest : List UInt256} + (h : RD endBytecode ee g s0 endRootSplitPc (selWord :: rest) mem aw rdata acc k C) + (hb : UInt256.gt (armSelNat endBytecode endRootSplitPc) selWord = ⟨0⟩) + (hov : rest.length + 3 ≤ 1024) : + RD endBytecode ee g s0 endHighSplitPc (selWord :: rest) mem aw rdata acc + (k + 5) (C + 22) := by + exact RD.selectorSplitNotTakenResolved (tgt := endLow1JumpdestPc) (nextPc := endHighSplitPc) + (width := 2) (op := .PUSH2) h endRootSplitWellFormed (by native_decide) + (by native_decide) (by native_decide) (by native_decide) hb hov + +theorem endHighSplitTaken {ee : ExecutionEnv} {g : Sat256} {s0 : State} + {selWord : UInt256} {mem : ByteArray} {aw : UInt256} {rdata : ByteArray} + {acc : Batteries.RBSet AccountAddress compare × AccountMap} {k C : ℕ} + {rest : List UInt256} + (h : RD endBytecode ee g s0 endHighSplitPc (selWord :: rest) mem aw rdata acc k C) + (hb : UInt256.gt (armSelNat endBytecode endHighSplitPc) selWord ≠ ⟨0⟩) + (hov : rest.length + 3 ≤ 1024) : + RD endBytecode ee g s0 endHighJumpdestPc (selWord :: rest) mem aw rdata acc + (k + 5) (C + 22) := by + exact RD.selectorSplitTakenResolved (tgt := endHighJumpdestPc) (width := 2) + (op := .PUSH2) h endHighSplitWellFormed (by native_decide) (by native_decide) + (by native_decide) hb (by jump_dest) hov + +theorem endHighSplitNotTaken {ee : ExecutionEnv} {g : Sat256} {s0 : State} + {selWord : UInt256} {mem : ByteArray} {aw : UInt256} {rdata : ByteArray} + {acc : Batteries.RBSet AccountAddress compare × AccountMap} {k C : ℕ} + {rest : List UInt256} + (h : RD endBytecode ee g s0 endHighSplitPc (selWord :: rest) mem aw rdata acc k C) + (hb : UInt256.gt (armSelNat endBytecode endHighSplitPc) selWord = ⟨0⟩) + (hov : rest.length + 3 ≤ 1024) : + RD endBytecode ee g s0 endHigh2SplitPc (selWord :: rest) mem aw rdata acc + (k + 5) (C + 22) := by + exact RD.selectorSplitNotTakenResolved (tgt := endHighJumpdestPc) (nextPc := endHigh2SplitPc) + (width := 2) (op := .PUSH2) h endHighSplitWellFormed (by native_decide) + (by native_decide) (by native_decide) (by native_decide) hb hov + +theorem endHigh2SplitTaken {ee : ExecutionEnv} {g : Sat256} {s0 : State} + {selWord : UInt256} {mem : ByteArray} {aw : UInt256} {rdata : ByteArray} + {acc : Batteries.RBSet AccountAddress compare × AccountMap} {k C : ℕ} + {rest : List UInt256} + (h : RD endBytecode ee g s0 endHigh2SplitPc (selWord :: rest) mem aw rdata acc k C) + (hb : UInt256.gt (armSelNat endBytecode endHigh2SplitPc) selWord ≠ ⟨0⟩) + (hov : rest.length + 3 ≤ 1024) : + RD endBytecode ee g s0 endGroup114JumpdestPc (selWord :: rest) mem aw rdata acc + (k + 5) (C + 22) := by + exact RD.selectorSplitTakenResolved (tgt := endGroup114JumpdestPc) (width := 2) + (op := .PUSH2) h endHigh2SplitWellFormed (by native_decide) (by native_decide) + (by native_decide) hb (by jump_dest) hov + +theorem endHigh2SplitNotTaken {ee : ExecutionEnv} {g : Sat256} {s0 : State} + {selWord : UInt256} {mem : ByteArray} {aw : UInt256} {rdata : ByteArray} + {acc : Batteries.RBSet AccountAddress compare × AccountMap} {k C : ℕ} + {rest : List UInt256} + (h : RD endBytecode ee g s0 endHigh2SplitPc (selWord :: rest) mem aw rdata acc k C) + (hb : UInt256.gt (armSelNat endBytecode endHigh2SplitPc) selWord = ⟨0⟩) + (hov : rest.length + 3 ≤ 1024) : + RD endBytecode ee g s0 endGroup65FirstArmPc (selWord :: rest) mem aw rdata acc + (k + 5) (C + 22) := by + exact RD.selectorSplitNotTakenResolved (tgt := endGroup114JumpdestPc) + (nextPc := endGroup65FirstArmPc) (width := 2) (op := .PUSH2) h + endHigh2SplitWellFormed (by native_decide) (by native_decide) (by native_decide) + (by native_decide) hb hov + +theorem endHighMidSplitTaken {ee : ExecutionEnv} {g : Sat256} {s0 : State} + {selWord : UInt256} {mem : ByteArray} {aw : UInt256} {rdata : ByteArray} + {acc : Batteries.RBSet AccountAddress compare × AccountMap} {k C : ℕ} + {rest : List UInt256} + (h : RD endBytecode ee g s0 endHighMidSplitPc (selWord :: rest) mem aw rdata acc k C) + (hb : UInt256.gt (armSelNat endBytecode endHighMidSplitPc) selWord ≠ ⟨0⟩) + (hov : rest.length + 3 ≤ 1024) : + RD endBytecode ee g s0 endGroup223JumpdestPc (selWord :: rest) mem aw rdata acc + (k + 5) (C + 22) := by + exact RD.selectorSplitTakenResolved (tgt := endGroup223JumpdestPc) (width := 2) + (op := .PUSH2) h endHighMidSplitWellFormed (by native_decide) (by native_decide) + (by native_decide) hb (by jump_dest) hov + +theorem endHighMidSplitNotTaken {ee : ExecutionEnv} {g : Sat256} {s0 : State} + {selWord : UInt256} {mem : ByteArray} {aw : UInt256} {rdata : ByteArray} + {acc : Batteries.RBSet AccountAddress compare × AccountMap} {k C : ℕ} + {rest : List UInt256} + (h : RD endBytecode ee g s0 endHighMidSplitPc (selWord :: rest) mem aw rdata acc k C) + (hb : UInt256.gt (armSelNat endBytecode endHighMidSplitPc) selWord = ⟨0⟩) + (hov : rest.length + 3 ≤ 1024) : + RD endBytecode ee g s0 endGroup174FirstArmPc (selWord :: rest) mem aw rdata acc + (k + 5) (C + 22) := by + exact RD.selectorSplitNotTakenResolved (tgt := endGroup223JumpdestPc) + (nextPc := endGroup174FirstArmPc) (width := 2) (op := .PUSH2) h + endHighMidSplitWellFormed (by native_decide) (by native_decide) (by native_decide) + (by native_decide) hb hov + +theorem endLow1SplitTaken {ee : ExecutionEnv} {g : Sat256} {s0 : State} + {selWord : UInt256} {mem : ByteArray} {aw : UInt256} {rdata : ByteArray} + {acc : Batteries.RBSet AccountAddress compare × AccountMap} {k C : ℕ} + {rest : List UInt256} + (h : RD endBytecode ee g s0 endLow1SplitPc (selWord :: rest) mem aw rdata acc k C) + (hb : UInt256.gt (armSelNat endBytecode endLow1SplitPc) selWord ≠ ⟨0⟩) + (hov : rest.length + 3 ≤ 1024) : + RD endBytecode ee g s0 endLow2JumpdestPc (selWord :: rest) mem aw rdata acc + (k + 5) (C + 22) := by + exact RD.selectorSplitTakenResolved (tgt := endLow2JumpdestPc) (width := 2) + (op := .PUSH2) h endLow1SplitWellFormed (by native_decide) (by native_decide) + (by native_decide) hb (by jump_dest) hov + +theorem endLow1SplitNotTaken {ee : ExecutionEnv} {g : Sat256} {s0 : State} + {selWord : UInt256} {mem : ByteArray} {aw : UInt256} {rdata : ByteArray} + {acc : Batteries.RBSet AccountAddress compare × AccountMap} {k C : ℕ} + {rest : List UInt256} + (h : RD endBytecode ee g s0 endLow1SplitPc (selWord :: rest) mem aw rdata acc k C) + (hb : UInt256.gt (armSelNat endBytecode endLow1SplitPc) selWord = ⟨0⟩) + (hov : rest.length + 3 ≤ 1024) : + RD endBytecode ee g s0 endLowHighSplitPc (selWord :: rest) mem aw rdata acc + (k + 5) (C + 22) := by + exact RD.selectorSplitNotTakenResolved (tgt := endLow2JumpdestPc) + (nextPc := endLowHighSplitPc) (width := 2) (op := .PUSH2) h endLow1SplitWellFormed + (by native_decide) (by native_decide) (by native_decide) (by native_decide) hb hov + +theorem endLowHighSplitTaken {ee : ExecutionEnv} {g : Sat256} {s0 : State} + {selWord : UInt256} {mem : ByteArray} {aw : UInt256} {rdata : ByteArray} + {acc : Batteries.RBSet AccountAddress compare × AccountMap} {k C : ℕ} + {rest : List UInt256} + (h : RD endBytecode ee g s0 endLowHighSplitPc (selWord :: rest) mem aw rdata acc k C) + (hb : UInt256.gt (armSelNat endBytecode endLowHighSplitPc) selWord ≠ ⟨0⟩) + (hov : rest.length + 3 ≤ 1024) : + RD endBytecode ee g s0 endGroup343JumpdestPc (selWord :: rest) mem aw rdata acc + (k + 5) (C + 22) := by + exact RD.selectorSplitTakenResolved (tgt := endGroup343JumpdestPc) (width := 2) + (op := .PUSH2) h endLowHighSplitWellFormed (by native_decide) (by native_decide) + (by native_decide) hb (by jump_dest) hov + +theorem endLowHighSplitNotTaken {ee : ExecutionEnv} {g : Sat256} {s0 : State} + {selWord : UInt256} {mem : ByteArray} {aw : UInt256} {rdata : ByteArray} + {acc : Batteries.RBSet AccountAddress compare × AccountMap} {k C : ℕ} + {rest : List UInt256} + (h : RD endBytecode ee g s0 endLowHighSplitPc (selWord :: rest) mem aw rdata acc k C) + (hb : UInt256.gt (armSelNat endBytecode endLowHighSplitPc) selWord = ⟨0⟩) + (hov : rest.length + 3 ≤ 1024) : + RD endBytecode ee g s0 endGroup294FirstArmPc (selWord :: rest) mem aw rdata acc + (k + 5) (C + 22) := by + exact RD.selectorSplitNotTakenResolved (tgt := endGroup343JumpdestPc) + (nextPc := endGroup294FirstArmPc) (width := 2) (op := .PUSH2) h + endLowHighSplitWellFormed (by native_decide) (by native_decide) (by native_decide) + (by native_decide) hb hov + +theorem endLow2SplitTaken {ee : ExecutionEnv} {g : Sat256} {s0 : State} + {selWord : UInt256} {mem : ByteArray} {aw : UInt256} {rdata : ByteArray} + {acc : Batteries.RBSet AccountAddress compare × AccountMap} {k C : ℕ} + {rest : List UInt256} + (h : RD endBytecode ee g s0 endLow2SplitPc (selWord :: rest) mem aw rdata acc k C) + (hb : UInt256.gt (armSelNat endBytecode endLow2SplitPc) selWord ≠ ⟨0⟩) + (hov : rest.length + 3 ≤ 1024) : + RD endBytecode ee g s0 endVeryLowJumpdestPc (selWord :: rest) mem aw rdata acc + (k + 5) (C + 22) := by + exact RD.selectorSplitTakenResolved (tgt := endVeryLowJumpdestPc) (width := 2) + (op := .PUSH2) h endLow2SplitWellFormed (by native_decide) (by native_decide) + (by native_decide) hb (by jump_dest) hov + +theorem endLow2SplitNotTaken {ee : ExecutionEnv} {g : Sat256} {s0 : State} + {selWord : UInt256} {mem : ByteArray} {aw : UInt256} {rdata : ByteArray} + {acc : Batteries.RBSet AccountAddress compare × AccountMap} {k C : ℕ} + {rest : List UInt256} + (h : RD endBytecode ee g s0 endLow2SplitPc (selWord :: rest) mem aw rdata acc k C) + (hb : UInt256.gt (armSelNat endBytecode endLow2SplitPc) selWord = ⟨0⟩) + (hov : rest.length + 3 ≤ 1024) : + RD endBytecode ee g s0 endGroup403FirstArmPc (selWord :: rest) mem aw rdata acc + (k + 5) (C + 22) := by + exact RD.selectorSplitNotTakenResolved (tgt := endVeryLowJumpdestPc) + (nextPc := endGroup403FirstArmPc) (width := 2) (op := .PUSH2) h endLow2SplitWellFormed + (by native_decide) (by native_decide) (by native_decide) (by native_decide) hb hov + set_option maxHeartbeats 1000000 in theorem endGroup65ArmsWellFormed : ∀ j, j ≤ 3 → armWellFormed endBytecode (nthArmPc endBytecode endGroup65FirstArmPc j) := by @@ -980,8 +1165,7 @@ theorem endReachDebtFirstArm {cA gh bl σ σ₀ A I} {g : Sat256} have h271 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endLow1JumpdestPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5) (C32 + 22) := by - simpa [endRootSplitPc, endLow1JumpdestPc] using - RD.selectorSplitTakenAuto h32 endRootSplitWellFormed hroot (by jump_dest) (by simp) + exact endRootSplitTaken h32 hroot (by simp) have h272 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endLow1SplitPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 1) (C32 + 22 + 1) := by @@ -989,8 +1173,7 @@ theorem endReachDebtFirstArm {cA gh bl σ σ₀ A I} {g : Sat256} have h391 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endLow2JumpdestPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 1 + 5) (C32 + 22 + 1 + 22) := by - simpa [endLow1SplitPc, endLow2JumpdestPc] using - RD.selectorSplitTakenAuto h272 endLow1SplitWellFormed hlow1 (by jump_dest) (by simp) + exact endLow1SplitTaken h272 hlow1 (by simp) have h392 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endLow2SplitPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 1 + 5 + 1) (C32 + 22 + 1 + 22 + 1) := by @@ -999,8 +1182,7 @@ theorem endReachDebtFirstArm {cA gh bl σ σ₀ A I} {g : Sat256} endVeryLowJumpdestPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 1 + 5 + 1 + 5) (C32 + 22 + 1 + 22 + 1 + 22) := by - simpa [endLow2SplitPc, endVeryLowJumpdestPc] using - RD.selectorSplitTakenAuto h392 endLow2SplitWellFormed hlow2 (by jump_dest) (by simp) + exact endLow2SplitTaken h392 hlow2 (by simp) have h452 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endDebtFirstArmPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 1 + 5 + 1 + 5 + 1) @@ -1047,21 +1229,15 @@ theorem endReachGroup65FirstArm {cA gh bl σ σ₀ A I} {g : Sat256} have h43 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endHighSplitPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5) (C32 + 22) := by - simpa [endRootSplitPc, endHighSplitPc, selArmNextPc, armTgtWidth, - selArmJumpiPc, selArmPushTgtPc, selArmEqPc, selArmPush4Pc] using - RD.selectorSplitNotTakenAuto h32 endRootSplitWellFormed hroot (by simp) + exact endRootSplitNotTaken h32 hroot (by simp) have h54 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endHigh2SplitPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 5) (C32 + 22 + 22) := by - simpa [endHighSplitPc, endHigh2SplitPc, selArmNextPc, armTgtWidth, - selArmJumpiPc, selArmPushTgtPc, selArmEqPc, selArmPush4Pc] using - RD.selectorSplitNotTakenAuto h43 endHighSplitWellFormed hhigh (by simp) + exact endHighSplitNotTaken h43 hhigh (by simp) have h65 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endGroup65FirstArmPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 5 + 5) (C32 + 22 + 22 + 22) := by - simpa [endHigh2SplitPc, endGroup65FirstArmPc, selArmNextPc, armTgtWidth, - selArmJumpiPc, selArmPushTgtPc, selArmEqPc, selArmPush4Pc] using - RD.selectorSplitNotTakenAuto h54 endHigh2SplitWellFormed hhigh2 (by simp) + exact endHigh2SplitNotTaken h54 hhigh2 (by simp) exact ⟨_, _, h65⟩ theorem endReachGroup114FirstArm {cA gh bl σ σ₀ A I} {g : Sat256} @@ -1079,20 +1255,15 @@ theorem endReachGroup114FirstArm {cA gh bl σ σ₀ A I} {g : Sat256} have h43 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endHighSplitPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5) (C32 + 22) := by - simpa [endRootSplitPc, endHighSplitPc, selArmNextPc, armTgtWidth, - selArmJumpiPc, selArmPushTgtPc, selArmEqPc, selArmPush4Pc] using - RD.selectorSplitNotTakenAuto h32 endRootSplitWellFormed hroot (by simp) + exact endRootSplitNotTaken h32 hroot (by simp) have h54 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endHigh2SplitPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 5) (C32 + 22 + 22) := by - simpa [endHighSplitPc, endHigh2SplitPc, selArmNextPc, armTgtWidth, - selArmJumpiPc, selArmPushTgtPc, selArmEqPc, selArmPush4Pc] using - RD.selectorSplitNotTakenAuto h43 endHighSplitWellFormed hhigh (by simp) + exact endHighSplitNotTaken h43 hhigh (by simp) have h113 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endGroup114JumpdestPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 5 + 5) (C32 + 22 + 22 + 22) := by - simpa [endHigh2SplitPc, endGroup114JumpdestPc] using - RD.selectorSplitTakenAuto h54 endHigh2SplitWellFormed hhigh2 (by jump_dest) (by simp) + exact endHigh2SplitTaken h54 hhigh2 (by simp) have h114 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endGroup114FirstArmPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 5 + 5 + 1) (C32 + 22 + 22 + 22 + 1) := by @@ -1114,14 +1285,11 @@ theorem endReachGroup174FirstArm {cA gh bl σ σ₀ A I} {g : Sat256} have h43 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endHighSplitPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5) (C32 + 22) := by - simpa [endRootSplitPc, endHighSplitPc, selArmNextPc, armTgtWidth, - selArmJumpiPc, selArmPushTgtPc, selArmEqPc, selArmPush4Pc] using - RD.selectorSplitNotTakenAuto h32 endRootSplitWellFormed hroot (by simp) + exact endRootSplitNotTaken h32 hroot (by simp) have h162 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endHighJumpdestPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 5) (C32 + 22 + 22) := by - simpa [endHighSplitPc, endHighJumpdestPc] using - RD.selectorSplitTakenAuto h43 endHighSplitWellFormed hhigh (by jump_dest) (by simp) + exact endHighSplitTaken h43 hhigh (by simp) have h163 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endHighMidSplitPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 5 + 1) (C32 + 22 + 22 + 1) := by @@ -1129,9 +1297,7 @@ theorem endReachGroup174FirstArm {cA gh bl σ σ₀ A I} {g : Sat256} have h174 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endGroup174FirstArmPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 5 + 1 + 5) (C32 + 22 + 22 + 1 + 22) := by - simpa [endHighMidSplitPc, endGroup174FirstArmPc, selArmNextPc, armTgtWidth, - selArmJumpiPc, selArmPushTgtPc, selArmEqPc, selArmPush4Pc] using - RD.selectorSplitNotTakenAuto h163 endHighMidSplitWellFormed hmid (by simp) + exact endHighMidSplitNotTaken h163 hmid (by simp) exact ⟨_, _, h174⟩ theorem endReachGroup223FirstArm {cA gh bl σ σ₀ A I} {g : Sat256} @@ -1149,14 +1315,11 @@ theorem endReachGroup223FirstArm {cA gh bl σ σ₀ A I} {g : Sat256} have h43 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endHighSplitPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5) (C32 + 22) := by - simpa [endRootSplitPc, endHighSplitPc, selArmNextPc, armTgtWidth, - selArmJumpiPc, selArmPushTgtPc, selArmEqPc, selArmPush4Pc] using - RD.selectorSplitNotTakenAuto h32 endRootSplitWellFormed hroot (by simp) + exact endRootSplitNotTaken h32 hroot (by simp) have h162 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endHighJumpdestPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 5) (C32 + 22 + 22) := by - simpa [endHighSplitPc, endHighJumpdestPc] using - RD.selectorSplitTakenAuto h43 endHighSplitWellFormed hhigh (by jump_dest) (by simp) + exact endHighSplitTaken h43 hhigh (by simp) have h163 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endHighMidSplitPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 5 + 1) (C32 + 22 + 22 + 1) := by @@ -1164,8 +1327,7 @@ theorem endReachGroup223FirstArm {cA gh bl σ σ₀ A I} {g : Sat256} have h222 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endGroup223JumpdestPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 5 + 1 + 5) (C32 + 22 + 22 + 1 + 22) := by - simpa [endHighMidSplitPc, endGroup223JumpdestPc] using - RD.selectorSplitTakenAuto h163 endHighMidSplitWellFormed hmid (by jump_dest) (by simp) + exact endHighMidSplitTaken h163 hmid (by simp) have h223 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endGroup223FirstArmPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 5 + 1 + 5 + 1) @@ -1188,8 +1350,7 @@ theorem endReachGroup294FirstArm {cA gh bl σ σ₀ A I} {g : Sat256} have h271 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endLow1JumpdestPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5) (C32 + 22) := by - simpa [endRootSplitPc, endLow1JumpdestPc] using - RD.selectorSplitTakenAuto h32 endRootSplitWellFormed hroot (by jump_dest) (by simp) + exact endRootSplitTaken h32 hroot (by simp) have h272 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endLow1SplitPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 1) (C32 + 22 + 1) := by @@ -1197,15 +1358,11 @@ theorem endReachGroup294FirstArm {cA gh bl σ σ₀ A I} {g : Sat256} have h283 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endLowHighSplitPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 1 + 5) (C32 + 22 + 1 + 22) := by - simpa [endLow1SplitPc, endLowHighSplitPc, selArmNextPc, armTgtWidth, - selArmJumpiPc, selArmPushTgtPc, selArmEqPc, selArmPush4Pc] using - RD.selectorSplitNotTakenAuto h272 endLow1SplitWellFormed hlow1 (by simp) + exact endLow1SplitNotTaken h272 hlow1 (by simp) have h294 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endGroup294FirstArmPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 1 + 5 + 5) (C32 + 22 + 1 + 22 + 22) := by - simpa [endLowHighSplitPc, endGroup294FirstArmPc, selArmNextPc, armTgtWidth, - selArmJumpiPc, selArmPushTgtPc, selArmEqPc, selArmPush4Pc] using - RD.selectorSplitNotTakenAuto h283 endLowHighSplitWellFormed hlowHigh (by simp) + exact endLowHighSplitNotTaken h283 hlowHigh (by simp) exact ⟨_, _, h294⟩ theorem endReachGroup343FirstArm {cA gh bl σ σ₀ A I} {g : Sat256} @@ -1223,8 +1380,7 @@ theorem endReachGroup343FirstArm {cA gh bl σ σ₀ A I} {g : Sat256} have h271 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endLow1JumpdestPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5) (C32 + 22) := by - simpa [endRootSplitPc, endLow1JumpdestPc] using - RD.selectorSplitTakenAuto h32 endRootSplitWellFormed hroot (by jump_dest) (by simp) + exact endRootSplitTaken h32 hroot (by simp) have h272 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endLow1SplitPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 1) (C32 + 22 + 1) := by @@ -1232,15 +1388,11 @@ theorem endReachGroup343FirstArm {cA gh bl σ σ₀ A I} {g : Sat256} have h283 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endLowHighSplitPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 1 + 5) (C32 + 22 + 1 + 22) := by - simpa [endLow1SplitPc, endLowHighSplitPc, selArmNextPc, armTgtWidth, - selArmJumpiPc, selArmPushTgtPc, selArmEqPc, selArmPush4Pc] using - RD.selectorSplitNotTakenAuto h272 endLow1SplitWellFormed hlow1 (by simp) + exact endLow1SplitNotTaken h272 hlow1 (by simp) have h342 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endGroup343JumpdestPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 1 + 5 + 5) (C32 + 22 + 1 + 22 + 22) := by - simpa [endLowHighSplitPc, endGroup343JumpdestPc] using - RD.selectorSplitTakenAuto h283 endLowHighSplitWellFormed hlowHigh - (by jump_dest) (by simp) + exact endLowHighSplitTaken h283 hlowHigh (by simp) have h343 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endGroup343FirstArmPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 1 + 5 + 5 + 1) @@ -1263,8 +1415,7 @@ theorem endReachGroup403FirstArm {cA gh bl σ σ₀ A I} {g : Sat256} have h271 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endLow1JumpdestPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5) (C32 + 22) := by - simpa [endRootSplitPc, endLow1JumpdestPc] using - RD.selectorSplitTakenAuto h32 endRootSplitWellFormed hroot (by jump_dest) (by simp) + exact endRootSplitTaken h32 hroot (by simp) have h272 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endLow1SplitPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 1) (C32 + 22 + 1) := by @@ -1272,8 +1423,7 @@ theorem endReachGroup403FirstArm {cA gh bl σ σ₀ A I} {g : Sat256} have h391 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endLow2JumpdestPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 1 + 5) (C32 + 22 + 1 + 22) := by - simpa [endLow1SplitPc, endLow2JumpdestPc] using - RD.selectorSplitTakenAuto h272 endLow1SplitWellFormed hlow1 (by jump_dest) (by simp) + exact endLow1SplitTaken h272 hlow1 (by simp) have h392 : RD endBytecode I g (initState cA gh bl σ σ₀ g A I) endLow2SplitPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 1 + 5 + 1) (C32 + 22 + 1 + 22 + 1) := by @@ -1282,9 +1432,7 @@ theorem endReachGroup403FirstArm {cA gh bl σ σ₀ A I} {g : Sat256} endGroup403FirstArmPc [endSelWord I] solcFreePtrMem (UInt256.ofNat 3) ByteArray.empty (cA, σ) (k32 + 5 + 1 + 5 + 1 + 5) (C32 + 22 + 1 + 22 + 1 + 22) := by - simpa [endLow2SplitPc, endGroup403FirstArmPc, selArmNextPc, armTgtWidth, - selArmJumpiPc, selArmPushTgtPc, selArmEqPc, selArmPush4Pc] using - RD.selectorSplitNotTakenAuto h392 endLow2SplitWellFormed hlow2 (by simp) + exact endLow2SplitNotTaken h392 hlow2 (by simp) exact ⟨_, _, h403⟩ theorem endJumpToNoMatchRevert {cA gh bl σ σ₀ A I} {g : Sat256} {pc : UInt256} diff --git a/Reasoning/Reach.lean b/Reasoning/Reach.lean index 146546d..e203988 100644 --- a/Reasoning/Reach.lean +++ b/Reasoning/Reach.lean @@ -2288,6 +2288,54 @@ theorem RD.selectorSplitNotTakenAuto {code : ByteArray} {ee : ExecutionEnv} {g : obtain ⟨hdup, hpush4, hgt, hopT, hpushT, hjumpi⟩ := hwf exact h.selectorSplitNotTaken hdup hpush4 hgt hopT hpushT hjumpi hb hov +/-- Selector split **taken**, with the bytecode-derived target/op/width resolved explicitly. + +Use this variant when the caller already has concrete generated-code facts. It keeps the result +from containing reducible `armTgt` projections, so later `simpa` steps do not unfold large bytecode +constants while trying to identify the jump target. -/ +theorem RD.selectorSplitTakenResolved {code : ByteArray} {ee : ExecutionEnv} {g : Sat256} + {s0 : State} {splitPc selWord tgt : UInt256} {mem : ByteArray} {aw : UInt256} + {rdata : ByteArray} {acc : Batteries.RBSet AccountAddress compare × AccountMap} + {k C width : ℕ} {op : Operation.POp} {rest : List UInt256} + (h : RD code ee g s0 splitPc (selWord :: rest) mem aw rdata acc k C) + (hwf : selectorSplitWellFormed code splitPc) + (hopEq : armTgtOp code splitPc = op) + (htgtEq : armTgt code splitPc = tgt) + (hwidthEq : armTgtWidth code splitPc = width) + (hb : UInt256.gt (armSelNat code splitPc) selWord ≠ ⟨0⟩) + (hjd : (D_J code 0).contains tgt = true) + (hov : rest.length + 3 ≤ 1024) : + RD code ee g s0 tgt (selWord :: rest) mem aw rdata acc (k + 5) (C + 22) := by + obtain ⟨hdup, hpush4, hgt, hopT, hpushT, hjumpi⟩ := hwf + exact h.selectorSplitTaken (pivot := armSelNat code splitPc) (tgt := tgt) (width := width) + (op := op) hdup hpush4 hgt (by simpa [hopEq] using hopT) + (by simpa [hopEq, htgtEq, hwidthEq] using hpushT) + (by simpa [hwidthEq] using hjumpi) hb hjd hov + +/-- Selector split **not taken**, with the bytecode-derived target/op/width and next pc resolved. + +This is the fall-through counterpart to `RD.selectorSplitTakenResolved`; the named `nextPc` +prevents callers from reducing `armTgtWidth` through generated bytecode during defeq. -/ +theorem RD.selectorSplitNotTakenResolved {code : ByteArray} {ee : ExecutionEnv} {g : Sat256} + {s0 : State} {splitPc selWord tgt nextPc : UInt256} {mem : ByteArray} {aw : UInt256} + {rdata : ByteArray} {acc : Batteries.RBSet AccountAddress compare × AccountMap} + {k C width : ℕ} {op : Operation.POp} {rest : List UInt256} + (h : RD code ee g s0 splitPc (selWord :: rest) mem aw rdata acc k C) + (hwf : selectorSplitWellFormed code splitPc) + (hopEq : armTgtOp code splitPc = op) + (htgtEq : armTgt code splitPc = tgt) + (hwidthEq : armTgtWidth code splitPc = width) + (hnextEq : selArmNextPc splitPc width = nextPc) + (hb : UInt256.gt (armSelNat code splitPc) selWord = ⟨0⟩) + (hov : rest.length + 3 ≤ 1024) : + RD code ee g s0 nextPc (selWord :: rest) mem aw rdata acc (k + 5) (C + 22) := by + rw [← hnextEq] + obtain ⟨hdup, hpush4, hgt, hopT, hpushT, hjumpi⟩ := hwf + exact h.selectorSplitNotTaken (pivot := armSelNat code splitPc) (tgt := tgt) (width := width) + (op := op) hdup hpush4 hgt (by simpa [hopEq] using hopT) + (by simpa [hopEq, htgtEq, hwidthEq] using hpushT) + (by simpa [hwidthEq] using hjumpi) hb hov + /-- The pc of the `n`-th arm from `start`, each arm's width read from the bytecode (so it threads `PUSH1` and `PUSH2` target arms alike). -/ def nthArmPc (code : ByteArray) (start : UInt256) : ℕ → UInt256 diff --git a/Solm/Syntax/DecEq.lean b/Solm/Syntax/DecEq.lean index 683f59d..181f621 100644 --- a/Solm/Syntax/DecEq.lean +++ b/Solm/Syntax/DecEq.lean @@ -3,12 +3,10 @@ import Solm.Syntax.Basic /-! `DecidableEq` instances for the `Solm` syntax types. -`Expr`, `StorageType`, and `Stmt` each carry nested `List` payloads (e.g. -`arrayLit : List Expr`), a shape Lean's `deriving DecidableEq` handler cannot -process, so their instances are hand-written structural `decEq`s. Every other -type derives normally. Instances appear in dependency order: each is in scope -before the types that use it. Kept out of `Solm.Syntax.Basic` so that file reads -as plain type definitions. +The recursive syntax types contain nested lists, a shape Lean's `DecidableEq` +deriver does not support. The hand-written deciders below keep those instances +computable while avoiding the large constructor cross-product that previously +made this module expensive to compile. -/ namespace Solm @@ -16,11 +14,10 @@ namespace Solm open ABI deriving instance DecidableEq for KeyValue - deriving instance DecidableEq for EvaledStorageRefStep - deriving instance DecidableEq for EvaledStorageRef +set_option maxHeartbeats 2000000 in mutual private def StorageType.decEq : (a b : StorageType) -> Decidable (a = b) | .elem p, .elem q => @@ -155,1777 +152,355 @@ instance : DecidableEq StorageType := StorageType.decEq deriving instance DecidableEq for EnvVar - deriving instance DecidableEq for UnaryOp - deriving instance DecidableEq for BinaryOp - deriving instance DecidableEq for VarOrigin --- The hand-written structural `DecidableEq` is an O(n²) match over `Expr`'s constructors; with the --- `keccak256`/`abiEncodePacked` additions it exceeds the default heartbeat budget during the equation --- compiler's `simp` pass, so the limit is raised for this block. -set_option maxHeartbeats 5000000 in +private def decEqOfIff {α : Type} {a b : α} (p : Prop) [Decidable p] + (hp : p → a = b) (hn : a = b → p) : Decidable (a = b) := + match (inferInstance : Decidable p) with + | isTrue h => isTrue (hp h) + | isFalse h => isFalse (fun hab => h (hn hab)) + +set_option maxHeartbeats 2000000 in mutual - private def Expr.decEq : (a b : Expr) -> Decidable (a = b) - | .intLit x, .intLit y => - match (inferInstance : Decidable (x = y)) with - | isTrue h => isTrue (by subst y; rfl) - | isFalse h => isFalse (by intro h'; cases h'; exact h rfl) - | .boolLit x, .boolLit y => - match (inferInstance : Decidable (x = y)) with - | isTrue h => isTrue (by subst y; rfl) - | isFalse h => isFalse (by intro h'; cases h'; exact h rfl) - | .bytesLit x, .bytesLit y => - match (inferInstance : Decidable (x = y)) with - | isTrue h => isTrue (by subst y; rfl) - | isFalse h => isFalse (by intro h'; cases h'; exact h rfl) - | .newBytes x, .newBytes y => - match Expr.decEq x y with - | isTrue h => isTrue (by cases h; rfl) - | isFalse h => isFalse (by intro h'; cases h'; exact h rfl) - | .newArray tx x, .newArray ty y => - match (inferInstance : Decidable (tx = ty)), Expr.decEq x y with - | isTrue ht, isTrue hx => isTrue (by cases ht; cases hx; rfl) - | isFalse ht, _ => isFalse (by intro h'; cases h'; exact ht rfl) - | _, isFalse hx => isFalse (by intro h'; cases h'; exact hx rfl) - | .bytesSlice b1 s1 e1, .bytesSlice b2 s2 e2 => - match Expr.decEq b1 b2, Expr.decEq s1 s2, Expr.decEq e1 e2 with - | isTrue hb, isTrue hs, isTrue he => isTrue (by cases hb; cases hs; cases he; rfl) - | isFalse hb, _, _ => isFalse (by intro h'; cases h'; exact hb rfl) - | _, isFalse hs, _ => isFalse (by intro h'; cases h'; exact hs rfl) - | _, _, isFalse he => isFalse (by intro h'; cases h'; exact he rfl) - | .var x, .var y => - match (inferInstance : Decidable (x = y)) with - | isTrue h => isTrue (by subst y; rfl) - | isFalse h => isFalse (by intro h'; cases h'; exact h rfl) - | .env x, .env y => - match (inferInstance : Decidable (x = y)) with - | isTrue h => isTrue (by subst y; rfl) - | isFalse h => isFalse (by intro h'; cases h'; exact h rfl) - | .field x fx, .field y fy => - match Expr.decEq x y, (inferInstance : Decidable (fx = fy)) with - | isTrue hx, isTrue hf => isTrue (by subst y; subst fy; rfl) - | isFalse hx, _ => isFalse (by intro h'; cases h'; exact hx rfl) - | _, isFalse hf => isFalse (by intro h'; cases h'; exact hf rfl) - | .storage x, .storage y => - match StorageRef.decEq x y with - | isTrue h => isTrue (by cases h; rfl) - | isFalse h => isFalse (by intro h'; cases h'; exact h rfl) - | .inRange tx x, .inRange ty y => - match (inferInstance : Decidable (tx = ty)), Expr.decEq x y with - | isTrue ht, isTrue hx => isTrue (by cases ht; cases hx; rfl) - | isFalse ht, _ => isFalse (by intro h'; cases h'; exact ht rfl) - | _, isFalse hx => isFalse (by intro h'; cases h'; exact hx rfl) - | .cast x tx, .cast y ty => - match Expr.decEq x y, (inferInstance : Decidable (tx = ty)) with - | isTrue hx, isTrue ht => isTrue (by cases hx; cases ht; rfl) - | isFalse hx, _ => isFalse (by intro h'; cases h'; exact hx rfl) - | _, isFalse ht => isFalse (by intro h'; cases h'; exact ht rfl) - | .addrOf x, .addrOf y => - match Expr.decEq x y with - | isTrue h => isTrue (by cases h; rfl) - | isFalse h => isFalse (by intro h'; cases h'; exact h rfl) - | .unary ox x, .unary oy y => - match (inferInstance : Decidable (ox = oy)), Expr.decEq x y with - | isTrue ho, isTrue hx => isTrue (by cases ho; cases hx; rfl) - | isFalse ho, _ => isFalse (by intro h'; cases h'; exact ho rfl) - | _, isFalse hx => isFalse (by intro h'; cases h'; exact hx rfl) - | .binary ox lx rx, .binary oy ly ry => - match (inferInstance : Decidable (ox = oy)), Expr.decEq lx ly, Expr.decEq rx ry with - | isTrue ho, isTrue hl, isTrue hr => isTrue (by cases ho; cases hl; cases hr; rfl) - | isFalse ho, _, _ => isFalse (by intro h'; cases h'; exact ho rfl) - | _, isFalse hl, _ => isFalse (by intro h'; cases h'; exact hl rfl) - | _, _, isFalse hr => isFalse (by intro h'; cases h'; exact hr rfl) - | .index bx ix, .index byx iy => - match Expr.decEq bx byx, Expr.decEq ix iy with - | isTrue hb, isTrue hi => isTrue (by cases hb; cases hi; rfl) - | isFalse hb, _ => isFalse (by intro h'; cases h'; exact hb rfl) - | _, isFalse hi => isFalse (by intro h'; cases h'; exact hi rfl) - | .ite cx tx fx, .ite cy ty fy => - match Expr.decEq cx cy, Expr.decEq tx ty, Expr.decEq fx fy with - | isTrue hc, isTrue ht, isTrue hf => isTrue (by cases hc; cases ht; cases hf; rfl) - | isFalse hc, _, _ => isFalse (by intro h'; cases h'; exact hc rfl) - | _, isFalse ht, _ => isFalse (by intro h'; cases h'; exact ht rfl) - | _, _, isFalse hf => isFalse (by intro h'; cases h'; exact hf rfl) - | .arrayLength ox x, .arrayLength oy y => - match (inferInstance : Decidable (ox = oy)), StorageRef.decEq x y with - | isTrue ho, isTrue hx => isTrue (by cases ho; cases hx; rfl) - | isFalse ho, _ => isFalse (by intro h'; cases h'; exact ho rfl) - | _, isFalse hx => isFalse (by intro h'; cases h'; exact hx rfl) - | .newArray _ _, .intLit _ => isFalse (by intro h; cases h) - | .newArray _ _, .boolLit _ => isFalse (by intro h; cases h) - | .newArray _ _, .bytesLit _ => isFalse (by intro h; cases h) - | .newArray _ _, .newBytes _ => isFalse (by intro h; cases h) - | .newArray _ _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .newArray _ _, .var _ => isFalse (by intro h; cases h) - | .newArray _ _, .env _ => isFalse (by intro h; cases h) - | .newArray _ _, .field _ _ => isFalse (by intro h; cases h) - | .newArray _ _, .storage _ => isFalse (by intro h; cases h) - | .newArray _ _, .inRange _ _ => isFalse (by intro h; cases h) - | .newArray _ _, .cast _ _ => isFalse (by intro h; cases h) - | .newArray _ _, .addrOf _ => isFalse (by intro h; cases h) - | .newArray _ _, .unary _ _ => isFalse (by intro h; cases h) - | .newArray _ _, .binary _ _ _ => isFalse (by intro h; cases h) - | .newArray _ _, .index _ _ => isFalse (by intro h; cases h) - | .newArray _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .newArray _ _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .intLit _, .newArray _ _ => isFalse (by intro h; cases h) - | .boolLit _, .newArray _ _ => isFalse (by intro h; cases h) - | .bytesLit _, .newArray _ _ => isFalse (by intro h; cases h) - | .newBytes _, .newArray _ _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .newArray _ _ => isFalse (by intro h; cases h) - | .var _, .newArray _ _ => isFalse (by intro h; cases h) - | .env _, .newArray _ _ => isFalse (by intro h; cases h) - | .field _ _, .newArray _ _ => isFalse (by intro h; cases h) - | .storage _, .newArray _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .newArray _ _ => isFalse (by intro h; cases h) - | .cast _ _, .newArray _ _ => isFalse (by intro h; cases h) - | .addrOf _, .newArray _ _ => isFalse (by intro h; cases h) - | .unary _ _, .newArray _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .newArray _ _ => isFalse (by intro h; cases h) - | .index _ _, .newArray _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .newArray _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .newArray _ _ => isFalse (by intro h; cases h) - | .intLit _, .boolLit _ => isFalse (by intro h; cases h) - | .intLit _, .var _ => isFalse (by intro h; cases h) - | .intLit _, .env _ => isFalse (by intro h; cases h) - | .intLit _, .field _ _ => isFalse (by intro h; cases h) - | .intLit _, .storage _ => isFalse (by intro h; cases h) - | .intLit _, .inRange _ _ => isFalse (by intro h; cases h) - | .intLit _, .cast _ _ => isFalse (by intro h; cases h) - | .intLit _, .addrOf _ => isFalse (by intro h; cases h) - | .intLit _, .unary _ _ => isFalse (by intro h; cases h) - | .intLit _, .binary _ _ _ => isFalse (by intro h; cases h) - | .intLit _, .index _ _ => isFalse (by intro h; cases h) - | .intLit _, .ite _ _ _ => isFalse (by intro h; cases h) - | .boolLit _, .intLit _ => isFalse (by intro h; cases h) - | .boolLit _, .var _ => isFalse (by intro h; cases h) - | .boolLit _, .env _ => isFalse (by intro h; cases h) - | .boolLit _, .field _ _ => isFalse (by intro h; cases h) - | .boolLit _, .storage _ => isFalse (by intro h; cases h) - | .boolLit _, .inRange _ _ => isFalse (by intro h; cases h) - | .boolLit _, .cast _ _ => isFalse (by intro h; cases h) - | .boolLit _, .addrOf _ => isFalse (by intro h; cases h) - | .boolLit _, .unary _ _ => isFalse (by intro h; cases h) - | .boolLit _, .binary _ _ _ => isFalse (by intro h; cases h) - | .boolLit _, .index _ _ => isFalse (by intro h; cases h) - | .boolLit _, .ite _ _ _ => isFalse (by intro h; cases h) - | .var _, .intLit _ => isFalse (by intro h; cases h) - | .var _, .boolLit _ => isFalse (by intro h; cases h) - | .var _, .env _ => isFalse (by intro h; cases h) - | .var _, .field _ _ => isFalse (by intro h; cases h) - | .var _, .storage _ => isFalse (by intro h; cases h) - | .var _, .inRange _ _ => isFalse (by intro h; cases h) - | .var _, .cast _ _ => isFalse (by intro h; cases h) - | .var _, .addrOf _ => isFalse (by intro h; cases h) - | .var _, .unary _ _ => isFalse (by intro h; cases h) - | .var _, .binary _ _ _ => isFalse (by intro h; cases h) - | .var _, .index _ _ => isFalse (by intro h; cases h) - | .var _, .ite _ _ _ => isFalse (by intro h; cases h) - | .env _, .intLit _ => isFalse (by intro h; cases h) - | .env _, .boolLit _ => isFalse (by intro h; cases h) - | .env _, .var _ => isFalse (by intro h; cases h) - | .env _, .field _ _ => isFalse (by intro h; cases h) - | .env _, .storage _ => isFalse (by intro h; cases h) - | .env _, .inRange _ _ => isFalse (by intro h; cases h) - | .env _, .cast _ _ => isFalse (by intro h; cases h) - | .env _, .addrOf _ => isFalse (by intro h; cases h) - | .env _, .unary _ _ => isFalse (by intro h; cases h) - | .env _, .binary _ _ _ => isFalse (by intro h; cases h) - | .env _, .index _ _ => isFalse (by intro h; cases h) - | .env _, .ite _ _ _ => isFalse (by intro h; cases h) - | .field _ _, .intLit _ => isFalse (by intro h; cases h) - | .field _ _, .boolLit _ => isFalse (by intro h; cases h) - | .field _ _, .var _ => isFalse (by intro h; cases h) - | .field _ _, .env _ => isFalse (by intro h; cases h) - | .field _ _, .storage _ => isFalse (by intro h; cases h) - | .field _ _, .inRange _ _ => isFalse (by intro h; cases h) - | .field _ _, .cast _ _ => isFalse (by intro h; cases h) - | .field _ _, .addrOf _ => isFalse (by intro h; cases h) - | .field _ _, .unary _ _ => isFalse (by intro h; cases h) - | .field _ _, .binary _ _ _ => isFalse (by intro h; cases h) - | .field _ _, .index _ _ => isFalse (by intro h; cases h) - | .field _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .storage _, .intLit _ => isFalse (by intro h; cases h) - | .storage _, .boolLit _ => isFalse (by intro h; cases h) - | .storage _, .var _ => isFalse (by intro h; cases h) - | .storage _, .env _ => isFalse (by intro h; cases h) - | .storage _, .field _ _ => isFalse (by intro h; cases h) - | .storage _, .inRange _ _ => isFalse (by intro h; cases h) - | .storage _, .cast _ _ => isFalse (by intro h; cases h) - | .storage _, .addrOf _ => isFalse (by intro h; cases h) - | .storage _, .unary _ _ => isFalse (by intro h; cases h) - | .storage _, .binary _ _ _ => isFalse (by intro h; cases h) - | .storage _, .index _ _ => isFalse (by intro h; cases h) - | .storage _, .ite _ _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .intLit _ => isFalse (by intro h; cases h) - | .inRange _ _, .boolLit _ => isFalse (by intro h; cases h) - | .inRange _ _, .var _ => isFalse (by intro h; cases h) - | .inRange _ _, .env _ => isFalse (by intro h; cases h) - | .inRange _ _, .field _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .storage _ => isFalse (by intro h; cases h) - | .inRange _ _, .cast _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .addrOf _ => isFalse (by intro h; cases h) - | .inRange _ _, .unary _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .binary _ _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .index _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .cast _ _, .intLit _ => isFalse (by intro h; cases h) - | .cast _ _, .boolLit _ => isFalse (by intro h; cases h) - | .cast _ _, .var _ => isFalse (by intro h; cases h) - | .cast _ _, .env _ => isFalse (by intro h; cases h) - | .cast _ _, .field _ _ => isFalse (by intro h; cases h) - | .cast _ _, .storage _ => isFalse (by intro h; cases h) - | .cast _ _, .inRange _ _ => isFalse (by intro h; cases h) - | .cast _ _, .addrOf _ => isFalse (by intro h; cases h) - | .cast _ _, .unary _ _ => isFalse (by intro h; cases h) - | .cast _ _, .binary _ _ _ => isFalse (by intro h; cases h) - | .cast _ _, .index _ _ => isFalse (by intro h; cases h) - | .cast _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .addrOf _, .intLit _ => isFalse (by intro h; cases h) - | .addrOf _, .boolLit _ => isFalse (by intro h; cases h) - | .addrOf _, .var _ => isFalse (by intro h; cases h) - | .addrOf _, .env _ => isFalse (by intro h; cases h) - | .addrOf _, .field _ _ => isFalse (by intro h; cases h) - | .addrOf _, .storage _ => isFalse (by intro h; cases h) - | .addrOf _, .inRange _ _ => isFalse (by intro h; cases h) - | .addrOf _, .cast _ _ => isFalse (by intro h; cases h) - | .addrOf _, .unary _ _ => isFalse (by intro h; cases h) - | .addrOf _, .binary _ _ _ => isFalse (by intro h; cases h) - | .addrOf _, .index _ _ => isFalse (by intro h; cases h) - | .addrOf _, .ite _ _ _ => isFalse (by intro h; cases h) - | .unary _ _, .intLit _ => isFalse (by intro h; cases h) - | .unary _ _, .boolLit _ => isFalse (by intro h; cases h) - | .unary _ _, .var _ => isFalse (by intro h; cases h) - | .unary _ _, .env _ => isFalse (by intro h; cases h) - | .unary _ _, .field _ _ => isFalse (by intro h; cases h) - | .unary _ _, .storage _ => isFalse (by intro h; cases h) - | .unary _ _, .inRange _ _ => isFalse (by intro h; cases h) - | .unary _ _, .cast _ _ => isFalse (by intro h; cases h) - | .unary _ _, .addrOf _ => isFalse (by intro h; cases h) - | .unary _ _, .binary _ _ _ => isFalse (by intro h; cases h) - | .unary _ _, .index _ _ => isFalse (by intro h; cases h) - | .unary _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .intLit _ => isFalse (by intro h; cases h) - | .binary _ _ _, .boolLit _ => isFalse (by intro h; cases h) - | .binary _ _ _, .var _ => isFalse (by intro h; cases h) - | .binary _ _ _, .env _ => isFalse (by intro h; cases h) - | .binary _ _ _, .field _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .storage _ => isFalse (by intro h; cases h) - | .binary _ _ _, .inRange _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .cast _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .addrOf _ => isFalse (by intro h; cases h) - | .binary _ _ _, .unary _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .index _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .index _ _, .intLit _ => isFalse (by intro h; cases h) - | .index _ _, .boolLit _ => isFalse (by intro h; cases h) - | .index _ _, .var _ => isFalse (by intro h; cases h) - | .index _ _, .env _ => isFalse (by intro h; cases h) - | .index _ _, .field _ _ => isFalse (by intro h; cases h) - | .index _ _, .storage _ => isFalse (by intro h; cases h) - | .index _ _, .inRange _ _ => isFalse (by intro h; cases h) - | .index _ _, .cast _ _ => isFalse (by intro h; cases h) - | .index _ _, .addrOf _ => isFalse (by intro h; cases h) - | .index _ _, .unary _ _ => isFalse (by intro h; cases h) - | .index _ _, .binary _ _ _ => isFalse (by intro h; cases h) - | .index _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .intLit _ => isFalse (by intro h; cases h) - | .ite _ _ _, .boolLit _ => isFalse (by intro h; cases h) - | .ite _ _ _, .var _ => isFalse (by intro h; cases h) - | .ite _ _ _, .env _ => isFalse (by intro h; cases h) - | .ite _ _ _, .field _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .storage _ => isFalse (by intro h; cases h) - | .ite _ _ _, .inRange _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .cast _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .addrOf _ => isFalse (by intro h; cases h) - | .ite _ _ _, .unary _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .binary _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .index _ _ => isFalse (by intro h; cases h) - | .bytesLit _, .intLit _ => isFalse (by intro h; cases h) - | .bytesLit _, .boolLit _ => isFalse (by intro h; cases h) - | .bytesLit _, .var _ => isFalse (by intro h; cases h) - | .bytesLit _, .env _ => isFalse (by intro h; cases h) - | .bytesLit _, .field _ _ => isFalse (by intro h; cases h) - | .bytesLit _, .storage _ => isFalse (by intro h; cases h) - | .bytesLit _, .inRange _ _ => isFalse (by intro h; cases h) - | .bytesLit _, .cast _ _ => isFalse (by intro h; cases h) - | .bytesLit _, .addrOf _ => isFalse (by intro h; cases h) - | .bytesLit _, .unary _ _ => isFalse (by intro h; cases h) - | .bytesLit _, .binary _ _ _ => isFalse (by intro h; cases h) - | .bytesLit _, .index _ _ => isFalse (by intro h; cases h) - | .bytesLit _, .ite _ _ _ => isFalse (by intro h; cases h) - | .bytesLit _, .newBytes _ => isFalse (by intro h; cases h) - | .intLit _, .bytesLit _ => isFalse (by intro h; cases h) - | .boolLit _, .bytesLit _ => isFalse (by intro h; cases h) - | .var _, .bytesLit _ => isFalse (by intro h; cases h) - | .env _, .bytesLit _ => isFalse (by intro h; cases h) - | .field _ _, .bytesLit _ => isFalse (by intro h; cases h) - | .storage _, .bytesLit _ => isFalse (by intro h; cases h) - | .inRange _ _, .bytesLit _ => isFalse (by intro h; cases h) - | .cast _ _, .bytesLit _ => isFalse (by intro h; cases h) - | .addrOf _, .bytesLit _ => isFalse (by intro h; cases h) - | .unary _ _, .bytesLit _ => isFalse (by intro h; cases h) - | .binary _ _ _, .bytesLit _ => isFalse (by intro h; cases h) - | .index _ _, .bytesLit _ => isFalse (by intro h; cases h) - | .ite _ _ _, .bytesLit _ => isFalse (by intro h; cases h) - | .newBytes _, .intLit _ => isFalse (by intro h; cases h) - | .newBytes _, .boolLit _ => isFalse (by intro h; cases h) - | .newBytes _, .var _ => isFalse (by intro h; cases h) - | .newBytes _, .env _ => isFalse (by intro h; cases h) - | .newBytes _, .field _ _ => isFalse (by intro h; cases h) - | .newBytes _, .storage _ => isFalse (by intro h; cases h) - | .newBytes _, .inRange _ _ => isFalse (by intro h; cases h) - | .newBytes _, .cast _ _ => isFalse (by intro h; cases h) - | .newBytes _, .addrOf _ => isFalse (by intro h; cases h) - | .newBytes _, .unary _ _ => isFalse (by intro h; cases h) - | .newBytes _, .binary _ _ _ => isFalse (by intro h; cases h) - | .newBytes _, .index _ _ => isFalse (by intro h; cases h) - | .newBytes _, .ite _ _ _ => isFalse (by intro h; cases h) - | .newBytes _, .bytesLit _ => isFalse (by intro h; cases h) - | .intLit _, .newBytes _ => isFalse (by intro h; cases h) - | .boolLit _, .newBytes _ => isFalse (by intro h; cases h) - | .var _, .newBytes _ => isFalse (by intro h; cases h) - | .env _, .newBytes _ => isFalse (by intro h; cases h) - | .field _ _, .newBytes _ => isFalse (by intro h; cases h) - | .storage _, .newBytes _ => isFalse (by intro h; cases h) - | .inRange _ _, .newBytes _ => isFalse (by intro h; cases h) - | .cast _ _, .newBytes _ => isFalse (by intro h; cases h) - | .addrOf _, .newBytes _ => isFalse (by intro h; cases h) - | .unary _ _, .newBytes _ => isFalse (by intro h; cases h) - | .binary _ _ _, .newBytes _ => isFalse (by intro h; cases h) - | .index _ _, .newBytes _ => isFalse (by intro h; cases h) - | .ite _ _ _, .newBytes _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .intLit _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .boolLit _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .bytesLit _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .newBytes _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .var _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .env _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .field _ _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .storage _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .inRange _ _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .cast _ _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .addrOf _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .unary _ _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .binary _ _ _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .index _ _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .intLit _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .boolLit _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .bytesLit _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .newBytes _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .var _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .env _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .field _ _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .storage _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .cast _ _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .addrOf _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .unary _ _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .index _ _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .intLit _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .boolLit _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .bytesLit _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .newBytes _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .var _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .env _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .field _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .storage _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .inRange _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .cast _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .addrOf _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .unary _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .binary _ _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .index _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .intLit _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .boolLit _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .bytesLit _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .newBytes _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .var _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .env _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .field _ _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .storage _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .cast _ _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .addrOf _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .unary _ _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .index _ _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .structLit nx fx, .structLit ny fy => - match (inferInstance : Decidable (nx = ny)), Expr.decEqNamedList fx fy with - | isTrue hn, isTrue hf => isTrue (by cases hn; cases hf; rfl) - | isFalse hn, _ => isFalse (by intro h; cases h; exact hn rfl) - | _, isFalse hf => isFalse (by intro h; cases h; exact hf rfl) - | .arrayLit xs, .arrayLit ys => - match Expr.decEqList xs ys with - | isTrue h => isTrue (by cases h; rfl) - | isFalse h => isFalse (by intro h'; cases h'; exact h rfl) - | .structLit _ _, .intLit _ => isFalse (by intro h; cases h) - | .intLit _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .boolLit _ => isFalse (by intro h; cases h) - | .boolLit _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .bytesLit _ => isFalse (by intro h; cases h) - | .bytesLit _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .newBytes _ => isFalse (by intro h; cases h) - | .newBytes _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .newArray _ _ => isFalse (by intro h; cases h) - | .newArray _ _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .var _ => isFalse (by intro h; cases h) - | .var _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .env _ => isFalse (by intro h; cases h) - | .env _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .field _ _ => isFalse (by intro h; cases h) - | .field _ _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .storage _ => isFalse (by intro h; cases h) - | .storage _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .inRange _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .cast _ _ => isFalse (by intro h; cases h) - | .cast _ _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .addrOf _ => isFalse (by intro h; cases h) - | .addrOf _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .unary _ _ => isFalse (by intro h; cases h) - | .unary _ _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .binary _ _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .index _ _ => isFalse (by intro h; cases h) - | .index _ _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .structLit _ _ => isFalse (by intro h; cases h) - | .arrayLit _, .intLit _ => isFalse (by intro h; cases h) - | .intLit _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .boolLit _ => isFalse (by intro h; cases h) - | .boolLit _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .bytesLit _ => isFalse (by intro h; cases h) - | .bytesLit _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .newBytes _ => isFalse (by intro h; cases h) - | .newBytes _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .newArray _ _ => isFalse (by intro h; cases h) - | .newArray _ _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .var _ => isFalse (by intro h; cases h) - | .var _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .env _ => isFalse (by intro h; cases h) - | .env _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .field _ _ => isFalse (by intro h; cases h) - | .field _ _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .storage _ => isFalse (by intro h; cases h) - | .storage _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .inRange _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .cast _ _ => isFalse (by intro h; cases h) - | .cast _ _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .addrOf _ => isFalse (by intro h; cases h) - | .addrOf _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .unary _ _ => isFalse (by intro h; cases h) - | .unary _ _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .binary _ _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .index _ _ => isFalse (by intro h; cases h) - | .index _ _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .arrayLit _ => isFalse (by intro h; cases h) - | .structLit _ _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .structLit _ _ => isFalse (by intro h; cases h) - | .tupleLit xs, .tupleLit ys => - match Expr.decEqList xs ys with - | isTrue h => isTrue (by cases h; rfl) - | isFalse h => isFalse (by intro h'; cases h'; exact h rfl) - | .tupleLit _, .intLit _ => isFalse (by intro h; cases h) - | .intLit _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .boolLit _ => isFalse (by intro h; cases h) - | .boolLit _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .bytesLit _ => isFalse (by intro h; cases h) - | .bytesLit _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .newBytes _ => isFalse (by intro h; cases h) - | .newBytes _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .newArray _ _ => isFalse (by intro h; cases h) - | .newArray _ _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .var _ => isFalse (by intro h; cases h) - | .var _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .env _ => isFalse (by intro h; cases h) - | .env _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .field _ _ => isFalse (by intro h; cases h) - | .field _ _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .storage _ => isFalse (by intro h; cases h) - | .storage _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .inRange _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .cast _ _ => isFalse (by intro h; cases h) - | .cast _ _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .addrOf _ => isFalse (by intro h; cases h) - | .addrOf _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .unary _ _ => isFalse (by intro h; cases h) - | .unary _ _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .binary _ _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .index _ _ => isFalse (by intro h; cases h) - | .index _ _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .tupleLit _ => isFalse (by intro h; cases h) - | .keccak256 x, .keccak256 y => - match Expr.decEq x y with - | isTrue h => isTrue (by cases h; rfl) - | isFalse h => isFalse (by intro h'; cases h'; exact h rfl) - | .keccak256 _, .intLit _ => isFalse (by intro h; cases h) - | .intLit _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .boolLit _ => isFalse (by intro h; cases h) - | .boolLit _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .bytesLit _ => isFalse (by intro h; cases h) - | .bytesLit _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .newBytes _ => isFalse (by intro h; cases h) - | .newBytes _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .newArray _ _ => isFalse (by intro h; cases h) - | .newArray _ _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .var _ => isFalse (by intro h; cases h) - | .var _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .env _ => isFalse (by intro h; cases h) - | .env _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .field _ _ => isFalse (by intro h; cases h) - | .field _ _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .storage _ => isFalse (by intro h; cases h) - | .storage _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .inRange _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .cast _ _ => isFalse (by intro h; cases h) - | .cast _ _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .addrOf _ => isFalse (by intro h; cases h) - | .addrOf _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .unary _ _ => isFalse (by intro h; cases h) - | .unary _ _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .binary _ _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .index _ _ => isFalse (by intro h; cases h) - | .index _ _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .keccak256 _ => isFalse (by intro h; cases h) - | .abiEncodePacked xs, .abiEncodePacked ys => - match Expr.decEqTypedList xs ys with - | isTrue h => isTrue (by cases h; rfl) - | isFalse h => isFalse (by intro h'; cases h'; exact h rfl) - | .abiEncodeCall nx xs, .abiEncodeCall ny ys => - match (inferInstance : Decidable (nx = ny)), Expr.decEqList xs ys with - | isTrue hn, isTrue hs => isTrue (by cases hn; cases hs; rfl) - | isFalse hn, _ => isFalse (by intro h; cases h; exact hn rfl) - | _, isFalse hs => isFalse (by intro h; cases h; exact hs rfl) - | .abiDecode tx x, .abiDecode ty y => - match (inferInstance : Decidable (tx = ty)), Expr.decEq x y with - | isTrue ht, isTrue hx => isTrue (by cases ht; cases hx; rfl) - | isFalse ht, _ => isFalse (by intro h; cases h; exact ht rfl) - | _, isFalse hx => isFalse (by intro h; cases h; exact hx rfl) - | .abiEncodeCall _ _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .intLit _ => isFalse (by intro h; cases h) - | .intLit _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .boolLit _ => isFalse (by intro h; cases h) - | .boolLit _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .bytesLit _ => isFalse (by intro h; cases h) - | .bytesLit _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .newBytes _ => isFalse (by intro h; cases h) - | .newBytes _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .newArray _ _ => isFalse (by intro h; cases h) - | .newArray _ _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .var _ => isFalse (by intro h; cases h) - | .var _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .env _ => isFalse (by intro h; cases h) - | .env _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .field _ _ => isFalse (by intro h; cases h) - | .field _ _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .storage _ => isFalse (by intro h; cases h) - | .storage _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .inRange _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .cast _ _ => isFalse (by intro h; cases h) - | .cast _ _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .addrOf _ => isFalse (by intro h; cases h) - | .addrOf _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .unary _ _ => isFalse (by intro h; cases h) - | .unary _ _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .binary _ _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .index _ _ => isFalse (by intro h; cases h) - | .index _ _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .intLit _ => isFalse (by intro h; cases h) - | .intLit _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .boolLit _ => isFalse (by intro h; cases h) - | .boolLit _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .bytesLit _ => isFalse (by intro h; cases h) - | .bytesLit _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .newBytes _ => isFalse (by intro h; cases h) - | .newBytes _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .newArray _ _ => isFalse (by intro h; cases h) - | .newArray _ _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .var _ => isFalse (by intro h; cases h) - | .var _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .env _ => isFalse (by intro h; cases h) - | .env _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .field _ _ => isFalse (by intro h; cases h) - | .field _ _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .storage _ => isFalse (by intro h; cases h) - | .storage _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .inRange _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .cast _ _ => isFalse (by intro h; cases h) - | .cast _ _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .addrOf _ => isFalse (by intro h; cases h) - | .addrOf _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .unary _ _ => isFalse (by intro h; cases h) - | .unary _ _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .binary _ _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .index _ _ => isFalse (by intro h; cases h) - | .index _ _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .intLit _ => isFalse (by intro h; cases h) - | .intLit _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .boolLit _ => isFalse (by intro h; cases h) - | .boolLit _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .bytesLit _ => isFalse (by intro h; cases h) - | .bytesLit _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .newBytes _ => isFalse (by intro h; cases h) - | .newBytes _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .newArray _ _ => isFalse (by intro h; cases h) - | .newArray _ _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .var _ => isFalse (by intro h; cases h) - | .var _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .env _ => isFalse (by intro h; cases h) - | .env _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .field _ _ => isFalse (by intro h; cases h) - | .field _ _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .storage _ => isFalse (by intro h; cases h) - | .storage _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .inRange _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .cast _ _ => isFalse (by intro h; cases h) - | .cast _ _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .addrOf _ => isFalse (by intro h; cases h) - | .addrOf _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .unary _ _ => isFalse (by intro h; cases h) - | .unary _ _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .binary _ _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .index _ _ => isFalse (by intro h; cases h) - | .index _ _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .extCodeSize x, .extCodeSize y => - match Expr.decEq x y with - | isTrue h => isTrue (by cases h; rfl) - | isFalse h => isFalse (by intro h'; cases h'; exact h rfl) - | .fixedBytesLit nx bx, .fixedBytesLit ny byy => - match (inferInstance : Decidable (nx = ny)), (inferInstance : Decidable (bx = byy)) with - | isTrue hn, isTrue hb => isTrue (by cases hn; cases hb; rfl) - | isFalse hn, _ => isFalse (by intro h; cases h; exact hn rfl) - | _, isFalse hb => isFalse (by intro h; cases h; exact hb rfl) - | .extCodeSize _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .intLit _ => isFalse (by intro h; cases h) - | .intLit _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .boolLit _ => isFalse (by intro h; cases h) - | .boolLit _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .bytesLit _ => isFalse (by intro h; cases h) - | .bytesLit _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .newBytes _ => isFalse (by intro h; cases h) - | .newBytes _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .newArray _ _ => isFalse (by intro h; cases h) - | .newArray _ _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .var _ => isFalse (by intro h; cases h) - | .var _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .env _ => isFalse (by intro h; cases h) - | .env _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .field _ _ => isFalse (by intro h; cases h) - | .field _ _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .storage _ => isFalse (by intro h; cases h) - | .storage _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .inRange _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .cast _ _ => isFalse (by intro h; cases h) - | .cast _ _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .addrOf _ => isFalse (by intro h; cases h) - | .addrOf _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .unary _ _ => isFalse (by intro h; cases h) - | .unary _ _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .binary _ _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .index _ _ => isFalse (by intro h; cases h) - | .index _ _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodePrefix ax lx, .extCodePrefix ay ly => - match Expr.decEq ax ay, Expr.decEq lx ly with - | isTrue ha, isTrue hl => isTrue (by cases ha; cases hl; rfl) - | isFalse ha, _ => isFalse (by intro h'; cases h'; exact ha rfl) - | _, isFalse hl => isFalse (by intro h'; cases h'; exact hl rfl) - | .tupleGet ex nx, .tupleGet ey ny => - match Expr.decEq ex ey, (inferInstance : Decidable (nx = ny)) with - | isTrue he, isTrue hn => isTrue (by cases he; cases hn; rfl) - | isFalse he, _ => isFalse (by intro h'; cases h'; exact he rfl) - | _, isFalse hn => isFalse (by intro h'; cases h'; exact hn rfl) - | .blockhash x, .blockhash y => - match Expr.decEq x y with - | isTrue h => isTrue (by cases h; rfl) - | isFalse h => isFalse (by intro h'; cases h'; exact h rfl) - | .balanceOf x, .balanceOf y => - match Expr.decEq x y with + private def Expr.decEq (a b : Expr) : Decidable (a = b) := by + cases a <;> cases b + all_goals first + | exact isFalse (by intro h; contradiction) + | skip + next x y => + exact decEqOfIff (x = y) (by intro h; cases h; rfl) (by intro h; cases h; rfl) + next x y => + exact decEqOfIff (x = y) (by intro h; cases h; rfl) (by intro h; cases h; rfl) + next x y => + exact decEqOfIff (x = y) (by intro h; cases h; rfl) (by intro h; cases h; rfl) + next x y => + letI : Decidable (x = y) := Expr.decEq x y + exact decEqOfIff (x = y) (by intro h; cases h; rfl) (by intro h; cases h; rfl) + next tx x ty y => + letI : Decidable (x = y) := Expr.decEq x y + exact decEqOfIff (tx = ty ∧ x = y) + (by rintro ⟨rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl⟩) + next nx fx ny fy => + letI : Decidable (fx = fy) := Expr.decEqNamedList fx fy + exact decEqOfIff (nx = ny ∧ fx = fy) + (by rintro ⟨rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl⟩) + next xs ys => + exact match Expr.decEqList xs ys with | isTrue h => isTrue (by cases h; rfl) | isFalse h => isFalse (by intro h'; cases h'; exact h rfl) - | .extCodeHash x, .extCodeHash y => - match Expr.decEq x y with + next xs ys => + exact match Expr.decEqList xs ys with | isTrue h => isTrue (by cases h; rfl) | isFalse h => isFalse (by intro h'; cases h'; exact h rfl) - | .tupleGet _ _, .intLit _ => isFalse (by intro h; cases h) - | .intLit _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .boolLit _ => isFalse (by intro h; cases h) - | .boolLit _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .bytesLit _ => isFalse (by intro h; cases h) - | .bytesLit _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .newBytes _ => isFalse (by intro h; cases h) - | .newBytes _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .newArray _ _ => isFalse (by intro h; cases h) - | .newArray _ _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .var _ => isFalse (by intro h; cases h) - | .var _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .env _ => isFalse (by intro h; cases h) - | .env _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .field _ _ => isFalse (by intro h; cases h) - | .field _ _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .storage _ => isFalse (by intro h; cases h) - | .storage _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .inRange _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .cast _ _ => isFalse (by intro h; cases h) - | .cast _ _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .addrOf _ => isFalse (by intro h; cases h) - | .addrOf _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .unary _ _ => isFalse (by intro h; cases h) - | .unary _ _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .binary _ _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .index _ _ => isFalse (by intro h; cases h) - | .index _ _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .blockhash _, .intLit _ => isFalse (by intro h; cases h) - | .intLit _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .boolLit _ => isFalse (by intro h; cases h) - | .boolLit _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .bytesLit _ => isFalse (by intro h; cases h) - | .bytesLit _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .newBytes _ => isFalse (by intro h; cases h) - | .newBytes _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .newArray _ _ => isFalse (by intro h; cases h) - | .newArray _ _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .var _ => isFalse (by intro h; cases h) - | .var _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .env _ => isFalse (by intro h; cases h) - | .env _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .field _ _ => isFalse (by intro h; cases h) - | .field _ _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .storage _ => isFalse (by intro h; cases h) - | .storage _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .inRange _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .cast _ _ => isFalse (by intro h; cases h) - | .cast _ _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .addrOf _ => isFalse (by intro h; cases h) - | .addrOf _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .unary _ _ => isFalse (by intro h; cases h) - | .unary _ _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .binary _ _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .index _ _ => isFalse (by intro h; cases h) - | .index _ _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .blockhash _ => isFalse (by intro h; cases h) - | .balanceOf _, .intLit _ => isFalse (by intro h; cases h) - | .intLit _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .boolLit _ => isFalse (by intro h; cases h) - | .boolLit _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .bytesLit _ => isFalse (by intro h; cases h) - | .bytesLit _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .newBytes _ => isFalse (by intro h; cases h) - | .newBytes _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .newArray _ _ => isFalse (by intro h; cases h) - | .newArray _ _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .var _ => isFalse (by intro h; cases h) - | .var _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .env _ => isFalse (by intro h; cases h) - | .env _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .field _ _ => isFalse (by intro h; cases h) - | .field _ _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .storage _ => isFalse (by intro h; cases h) - | .storage _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .inRange _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .cast _ _ => isFalse (by intro h; cases h) - | .cast _ _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .addrOf _ => isFalse (by intro h; cases h) - | .addrOf _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .unary _ _ => isFalse (by intro h; cases h) - | .unary _ _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .binary _ _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .index _ _ => isFalse (by intro h; cases h) - | .index _ _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .balanceOf _ => isFalse (by intro h; cases h) - | .extCodeHash _, .intLit _ => isFalse (by intro h; cases h) - | .intLit _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .boolLit _ => isFalse (by intro h; cases h) - | .boolLit _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .bytesLit _ => isFalse (by intro h; cases h) - | .bytesLit _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .newBytes _ => isFalse (by intro h; cases h) - | .newBytes _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .newArray _ _ => isFalse (by intro h; cases h) - | .newArray _ _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .var _ => isFalse (by intro h; cases h) - | .var _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .env _ => isFalse (by intro h; cases h) - | .env _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .field _ _ => isFalse (by intro h; cases h) - | .field _ _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .storage _ => isFalse (by intro h; cases h) - | .storage _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .inRange _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .cast _ _ => isFalse (by intro h; cases h) - | .cast _ _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .addrOf _ => isFalse (by intro h; cases h) - | .addrOf _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .unary _ _ => isFalse (by intro h; cases h) - | .unary _ _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .binary _ _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .index _ _ => isFalse (by intro h; cases h) - | .index _ _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .extCodeHash _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .tupleGet _ _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .tupleGet _ _ => isFalse (by intro h; cases h) - | .blockhash _, .balanceOf _ => isFalse (by intro h; cases h) - | .balanceOf _, .blockhash _ => isFalse (by intro h; cases h) - | .blockhash _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .blockhash _ => isFalse (by intro h; cases h) - | .balanceOf _, .extCodeHash _ => isFalse (by intro h; cases h) - | .extCodeHash _, .balanceOf _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .intLit _ => isFalse (by intro h; cases h) - | .intLit _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .boolLit _ => isFalse (by intro h; cases h) - | .boolLit _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .bytesLit _ => isFalse (by intro h; cases h) - | .bytesLit _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .newBytes _ => isFalse (by intro h; cases h) - | .newBytes _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .newArray _ _ => isFalse (by intro h; cases h) - | .newArray _ _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .var _ => isFalse (by intro h; cases h) - | .var _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .env _ => isFalse (by intro h; cases h) - | .env _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .field _ _ => isFalse (by intro h; cases h) - | .field _ _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .storage _ => isFalse (by intro h; cases h) - | .storage _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .inRange _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .cast _ _ => isFalse (by intro h; cases h) - | .cast _ _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .addrOf _ => isFalse (by intro h; cases h) - | .addrOf _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .unary _ _ => isFalse (by intro h; cases h) - | .unary _ _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .binary _ _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .index _ _ => isFalse (by intro h; cases h) - | .index _ _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .abiEncodeCall _ _ => isFalse (by intro h; cases h) - | .abiEncodeCall _ _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .abiDecode _ _ => isFalse (by intro h; cases h) - | .abiDecode _ _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .extCodeSize _ => isFalse (by intro h; cases h) - | .extCodeSize _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .extCodePrefix _ _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .extCodePrefix _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .intLit _ => isFalse (by intro h; cases h) - | .intLit _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .boolLit _ => isFalse (by intro h; cases h) - | .boolLit _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .bytesLit _ => isFalse (by intro h; cases h) - | .bytesLit _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .newBytes _ => isFalse (by intro h; cases h) - | .newBytes _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .newArray _ _ => isFalse (by intro h; cases h) - | .newArray _ _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .structLit _ _ => isFalse (by intro h; cases h) - | .structLit _ _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .arrayLit _ => isFalse (by intro h; cases h) - | .arrayLit _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .tupleLit _ => isFalse (by intro h; cases h) - | .tupleLit _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .bytesSlice _ _ _ => isFalse (by intro h; cases h) - | .bytesSlice _ _ _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .var _ => isFalse (by intro h; cases h) - | .var _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .env _ => isFalse (by intro h; cases h) - | .env _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .field _ _ => isFalse (by intro h; cases h) - | .field _ _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .storage _ => isFalse (by intro h; cases h) - | .storage _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .inRange _ _ => isFalse (by intro h; cases h) - | .inRange _ _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .cast _ _ => isFalse (by intro h; cases h) - | .cast _ _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .addrOf _ => isFalse (by intro h; cases h) - | .addrOf _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .unary _ _ => isFalse (by intro h; cases h) - | .unary _ _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .binary _ _ _ => isFalse (by intro h; cases h) - | .binary _ _ _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .index _ _ => isFalse (by intro h; cases h) - | .index _ _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .arrayLength _ _ => isFalse (by intro h; cases h) - | .arrayLength _ _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .keccak256 _ => isFalse (by intro h; cases h) - | .keccak256 _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - | .fixedBytesLit _ _, .abiEncodePacked _ => isFalse (by intro h; cases h) - | .abiEncodePacked _, .fixedBytesLit _ _ => isFalse (by intro h; cases h) - - private def Expr.decEqList : (as bs : List Expr) -> Decidable (as = bs) + next x ix y iy => + letI : Decidable (x = y) := Expr.decEq x y + exact decEqOfIff (x = y ∧ ix = iy) + (by rintro ⟨rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl⟩) + next bx sx ex byx sy ey => + letI : Decidable (bx = byx) := Expr.decEq bx byx + letI : Decidable (sx = sy) := Expr.decEq sx sy + letI : Decidable (ex = ey) := Expr.decEq ex ey + exact decEqOfIff (bx = byx ∧ sx = sy ∧ ex = ey) + (by rintro ⟨rfl, rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl, rfl⟩) + next x y => + exact decEqOfIff (x = y) (by intro h; cases h; rfl) (by intro h; cases h; rfl) + next x y => + exact decEqOfIff (x = y) (by intro h; cases h; rfl) (by intro h; cases h; rfl) + next x fx y fy => + letI : Decidable (x = y) := Expr.decEq x y + exact decEqOfIff (x = y ∧ fx = fy) + (by rintro ⟨rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl⟩) + next x y => + letI : Decidable (x = y) := StorageRef.decEq x y + exact decEqOfIff (x = y) (by intro h; cases h; rfl) (by intro h; cases h; rfl) + next tx x ty y => + letI : Decidable (x = y) := Expr.decEq x y + exact decEqOfIff (tx = ty ∧ x = y) + (by rintro ⟨rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl⟩) + next x tx y ty => + letI : Decidable (x = y) := Expr.decEq x y + exact decEqOfIff (x = y ∧ tx = ty) + (by rintro ⟨rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl⟩) + next x y => + letI : Decidable (x = y) := Expr.decEq x y + exact decEqOfIff (x = y) (by intro h; cases h; rfl) (by intro h; cases h; rfl) + next ox x oy y => + letI : Decidable (x = y) := Expr.decEq x y + exact decEqOfIff (ox = oy ∧ x = y) + (by rintro ⟨rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl⟩) + next ox lx rx oy ly ry => + letI : Decidable (lx = ly) := Expr.decEq lx ly + letI : Decidable (rx = ry) := Expr.decEq rx ry + exact decEqOfIff (ox = oy ∧ lx = ly ∧ rx = ry) + (by rintro ⟨rfl, rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl, rfl⟩) + next bx ix byx iy => + letI : Decidable (bx = byx) := Expr.decEq bx byx + letI : Decidable (ix = iy) := Expr.decEq ix iy + exact decEqOfIff (bx = byx ∧ ix = iy) + (by rintro ⟨rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl⟩) + next cx tx fx cy ty fy => + letI : Decidable (cx = cy) := Expr.decEq cx cy + letI : Decidable (tx = ty) := Expr.decEq tx ty + letI : Decidable (fx = fy) := Expr.decEq fx fy + exact decEqOfIff (cx = cy ∧ tx = ty ∧ fx = fy) + (by rintro ⟨rfl, rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl, rfl⟩) + next ox x oy y => + letI : Decidable (x = y) := StorageRef.decEq x y + exact decEqOfIff (ox = oy ∧ x = y) + (by rintro ⟨rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl⟩) + next x y => + letI : Decidable (x = y) := Expr.decEq x y + exact decEqOfIff (x = y) (by intro h; cases h; rfl) (by intro h; cases h; rfl) + next xs ys => + letI : Decidable (xs = ys) := Expr.decEqTypedList xs ys + exact decEqOfIff (xs = ys) (by intro h; cases h; rfl) (by intro h; cases h; rfl) + next nx xs ny ys => + letI : Decidable (xs = ys) := Expr.decEqList xs ys + exact decEqOfIff (nx = ny ∧ xs = ys) + (by rintro ⟨rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl⟩) + next tx x ty y => + letI : Decidable (x = y) := Expr.decEq x y + exact decEqOfIff (tx = ty ∧ x = y) + (by rintro ⟨rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl⟩) + next x y => + letI : Decidable (x = y) := Expr.decEq x y + exact decEqOfIff (x = y) (by intro h; cases h; rfl) (by intro h; cases h; rfl) + next ax lx ay ly => + letI : Decidable (ax = ay) := Expr.decEq ax ay + letI : Decidable (lx = ly) := Expr.decEq lx ly + exact decEqOfIff (ax = ay ∧ lx = ly) + (by rintro ⟨rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl⟩) + next x y => + letI : Decidable (x = y) := Expr.decEq x y + exact decEqOfIff (x = y) (by intro h; cases h; rfl) (by intro h; cases h; rfl) + next x y => + letI : Decidable (x = y) := Expr.decEq x y + exact decEqOfIff (x = y) (by intro h; cases h; rfl) (by intro h; cases h; rfl) + next x y => + letI : Decidable (x = y) := Expr.decEq x y + exact decEqOfIff (x = y) (by intro h; cases h; rfl) (by intro h; cases h; rfl) + next nx bx ny bys => + exact decEqOfIff (nx = ny ∧ bx = bys) + (by rintro ⟨rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl⟩) + + private def Expr.decEqList : (as bs : List Expr) → Decidable (as = bs) | [], [] => isTrue rfl | a :: as, b :: bs => - match Expr.decEq a b, Expr.decEqList as bs with - | isTrue ha, isTrue hs => isTrue (by cases ha; cases hs; rfl) - | isFalse ha, _ => isFalse (by intro h; cases h; exact ha rfl) - | _, isFalse hs => isFalse (by intro h; cases h; exact hs rfl) + letI : Decidable (a = b) := Expr.decEq a b + letI : Decidable (as = bs) := Expr.decEqList as bs + decEqOfIff (a = b ∧ as = bs) + (by rintro ⟨rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl⟩) | [], _ :: _ => isFalse (by intro h; cases h) | _ :: _, [] => isFalse (by intro h; cases h) - private def Expr.decEqNamedList : (as bs : List (Ident × Expr)) -> Decidable (as = bs) + private def Expr.decEqNamedList : (as bs : List (Ident × Expr)) → Decidable (as = bs) | [], [] => isTrue rfl - | (nx, ex) :: as, (ny, ey) :: bs => - match (inferInstance : Decidable (nx = ny)), Expr.decEq ex ey, Expr.decEqNamedList as bs with - | isTrue hn, isTrue he, isTrue hs => isTrue (by cases hn; cases he; cases hs; rfl) - | isFalse hn, _, _ => isFalse (by intro h; cases h; exact hn rfl) - | _, isFalse he, _ => isFalse (by intro h; cases h; exact he rfl) - | _, _, isFalse hs => isFalse (by intro h; cases h; exact hs rfl) + | (an, ax) :: as, (bn, bx) :: bs => + letI : Decidable (an = bn) := String.decEq an bn + letI : Decidable (ax = bx) := Expr.decEq ax bx + letI : Decidable (as = bs) := Expr.decEqNamedList as bs + decEqOfIff (an = bn ∧ ax = bx ∧ as = bs) + (by rintro ⟨rfl, rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl, rfl⟩) | [], _ :: _ => isFalse (by intro h; cases h) | _ :: _, [] => isFalse (by intro h; cases h) - private def Expr.decEqTypedList : (as bs : List (ABIType × Expr)) -> Decidable (as = bs) + private def Expr.decEqTypedList : (as bs : List (ABIType × Expr)) → Decidable (as = bs) | [], [] => isTrue rfl - | (tx, ex) :: as, (ty, ey) :: bs => - match (inferInstance : Decidable (tx = ty)), Expr.decEq ex ey, Expr.decEqTypedList as bs with - | isTrue ht, isTrue he, isTrue hs => isTrue (by cases ht; cases he; cases hs; rfl) - | isFalse ht, _, _ => isFalse (by intro h; cases h; exact ht rfl) - | _, isFalse he, _ => isFalse (by intro h; cases h; exact he rfl) - | _, _, isFalse hs => isFalse (by intro h; cases h; exact hs rfl) + | (aty, ax) :: as, (bty, bx) :: bs => + letI : Decidable (ax = bx) := Expr.decEq ax bx + letI : Decidable (as = bs) := Expr.decEqTypedList as bs + decEqOfIff (aty = bty ∧ ax = bx ∧ as = bs) + (by rintro ⟨rfl, rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl, rfl⟩) | [], _ :: _ => isFalse (by intro h; cases h) | _ :: _, [] => isFalse (by intro h; cases h) - private def StorageRefStep.decEq : (a b : StorageRefStep) -> Decidable (a = b) - | .field x, .field y => - match (inferInstance : Decidable (x = y)) with - | isTrue h => isTrue (by subst y; rfl) - | isFalse h => isFalse (by intro h'; cases h'; exact h rfl) - | .mindex x, .mindex y => - match Expr.decEq x y with - | isTrue h => isTrue (by cases h; rfl) - | isFalse h => isFalse (by intro h'; cases h'; exact h rfl) - | .aindex x, .aindex y => - match Expr.decEq x y with - | isTrue h => isTrue (by cases h; rfl) - | isFalse h => isFalse (by intro h'; cases h'; exact h rfl) - | .field _, .mindex _ => isFalse (by intro h; cases h) - | .field _, .aindex _ => isFalse (by intro h; cases h) - | .mindex _, .field _ => isFalse (by intro h; cases h) - | .mindex _, .aindex _ => isFalse (by intro h; cases h) - | .aindex _, .field _ => isFalse (by intro h; cases h) - | .aindex _, .mindex _ => isFalse (by intro h; cases h) - - private def StorageRef.decEq : (a b : StorageRef) -> Decidable (a = b) - | ⟨base, steps⟩, ⟨base', steps'⟩ => - match (inferInstance : Decidable (base = base')), StorageRefStep.decEqList steps steps' with - | isTrue hb, isTrue hs => isTrue (by cases hb; cases hs; rfl) - | isFalse hb, _ => isFalse (by intro h; cases h; exact hb rfl) - | _, isFalse hs => isFalse (by intro h; cases h; exact hs rfl) - - private def StorageRefStep.decEqList : (as bs : List StorageRefStep) -> Decidable (as = bs) + private def StorageRefStep.decEq (a b : StorageRefStep) : Decidable (a = b) := by + cases a <;> cases b + all_goals first + | exact isFalse (by intro h; contradiction) + | skip + next x y => + exact decEqOfIff (x = y) (by intro h; cases h; rfl) (by intro h; cases h; rfl) + next x y => + letI : Decidable (x = y) := Expr.decEq x y + exact decEqOfIff (x = y) (by intro h; cases h; rfl) (by intro h; cases h; rfl) + next x y => + letI : Decidable (x = y) := Expr.decEq x y + exact decEqOfIff (x = y) (by intro h; cases h; rfl) (by intro h; cases h; rfl) + private def StorageRef.decEq : (a b : StorageRef) → Decidable (a = b) + | ⟨baseA, stepsA⟩, ⟨baseB, stepsB⟩ => + letI : Decidable (baseA = baseB) := String.decEq baseA baseB + letI : Decidable (stepsA = stepsB) := StorageRefStep.decEqList stepsA stepsB + decEqOfIff (baseA = baseB ∧ stepsA = stepsB) + (by rintro ⟨rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl⟩) + + private def StorageRefStep.decEqList : + (as bs : List StorageRefStep) → Decidable (as = bs) | [], [] => isTrue rfl | a :: as, b :: bs => - match StorageRefStep.decEq a b, StorageRefStep.decEqList as bs with - | isTrue ha, isTrue hs => isTrue (by cases ha; cases hs; rfl) - | isFalse ha, _ => isFalse (by intro h; cases h; exact ha rfl) - | _, isFalse hs => isFalse (by intro h; cases h; exact hs rfl) + letI : Decidable (a = b) := StorageRefStep.decEq a b + letI : Decidable (as = bs) := StorageRefStep.decEqList as bs + decEqOfIff (a = b ∧ as = bs) + (by rintro ⟨rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl⟩) | [], _ :: _ => isFalse (by intro h; cases h) | _ :: _, [] => isFalse (by intro h; cases h) end -instance : DecidableEq Expr := - Expr.decEq - -instance : DecidableEq StorageRefStep := - StorageRefStep.decEq - -instance : DecidableEq StorageRef := - StorageRef.decEq +instance : DecidableEq Expr := Expr.decEq +instance : DecidableEq StorageRefStep := StorageRefStep.decEq +instance : DecidableEq StorageRef := StorageRef.decEq deriving instance DecidableEq for AssignRhs mutual - private def Stmt.decEq : (a b : Stmt) -> Decidable (a = b) - | .letDecl nx tx ex, .letDecl ny ty ey => - match (inferInstance : Decidable (nx = ny)), (inferInstance : Decidable (tx = ty)), Expr.decEq ex ey with - | isTrue hn, isTrue ht, isTrue he => isTrue (by cases hn; cases ht; cases he; rfl) - | isFalse hn, _, _ => isFalse (by intro h; cases h; exact hn rfl) - | _, isFalse ht, _ => isFalse (by intro h; cases h; exact ht rfl) - | _, _, isFalse he => isFalse (by intro h; cases h; exact he rfl) - | .letStorage nx rx, .letStorage ny ry => - match (inferInstance : Decidable (nx = ny)), StorageRef.decEq rx ry with - | isTrue hn, isTrue hr => isTrue (by cases hn; cases hr; rfl) - | isFalse hn, _ => isFalse (by intro h; cases h; exact hn rfl) - | _, isFalse hr => isFalse (by intro h; cases h; exact hr rfl) - | .letGas nx, .letGas ny => - match (inferInstance : Decidable (nx = ny)) with - | isTrue h => isTrue (by cases h; rfl) - | isFalse h => isFalse (by intro h'; cases h'; exact h rfl) - | .letGas _, .letDecl _ _ _ => isFalse (by intro h; cases h) - | .letDecl _ _ _, .letGas _ => isFalse (by intro h; cases h) - | .letGas _, .letStorage _ _ => isFalse (by intro h; cases h) - | .letStorage _ _, .letGas _ => isFalse (by intro h; cases h) - | .letGas _, .assign _ _ _ => isFalse (by intro h; cases h) - | .assign _ _ _, .letGas _ => isFalse (by intro h; cases h) - | .letGas _, .require _ => isFalse (by intro h; cases h) - | .require _, .letGas _ => isFalse (by intro h; cases h) - | .letGas _, .while _ _ => isFalse (by intro h; cases h) - | .while _ _, .letGas _ => isFalse (by intro h; cases h) - | .letGas _, .for _ _ _ _ => isFalse (by intro h; cases h) - | .for _ _ _ _, .letGas _ => isFalse (by intro h; cases h) - | .letGas _, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .letGas _ => isFalse (by intro h; cases h) - | .letGas _, .new _ _ _ _ _ => isFalse (by intro h; cases h) - | .new _ _ _ _ _, .letGas _ => isFalse (by intro h; cases h) - | .letGas _, .internalCall _ _ _ => isFalse (by intro h; cases h) - | .internalCall _ _ _, .letGas _ => isFalse (by intro h; cases h) - | .letGas _, .externalCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .externalCall _ _ _ _ _ _, .letGas _ => isFalse (by intro h; cases h) - | .letGas _, .lowLevelCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .lowLevelCall _ _ _ _ _ _, .letGas _ => isFalse (by intro h; cases h) - | .letGas _, .delegateCall _ _ _ _ => isFalse (by intro h; cases h) - | .delegateCall _ _ _ _, .letGas _ => isFalse (by intro h; cases h) - | .letGas _, .checkedCall _ _ _ _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .checkedCall _ _ _ _ _ _ _ _ _, .letGas _ => isFalse (by intro h; cases h) - | .letGas _, .return _ => isFalse (by intro h; cases h) - | .return _, .letGas _ => isFalse (by intro h; cases h) - | .letGas _, .break => isFalse (by intro h; cases h) - | .break, .letGas _ => isFalse (by intro h; cases h) - | .letGas _, .continue => isFalse (by intro h; cases h) - | .continue, .letGas _ => isFalse (by intro h; cases h) - | .letGas _, .push _ _ => isFalse (by intro h; cases h) - | .push _ _, .letGas _ => isFalse (by intro h; cases h) - | .letGas _, .pop _ => isFalse (by intro h; cases h) - | .pop _, .letGas _ => isFalse (by intro h; cases h) - | .letGas _, .delete _ => isFalse (by intro h; cases h) - | .delete _, .letGas _ => isFalse (by intro h; cases h) - | .assign ox sx ex, .assign oy sy ey => - match (inferInstance : Decidable (ox = oy)), StorageRef.decEq sx sy, Expr.decEq ex ey with - | isTrue ho, isTrue hs, isTrue he => isTrue (by cases ho; cases hs; cases he; rfl) - | isFalse ho, _, _ => isFalse (by intro h; cases h; exact ho rfl) - | _, isFalse hs, _ => isFalse (by intro h; cases h; exact hs rfl) - | _, _, isFalse he => isFalse (by intro h; cases h; exact he rfl) - | .require ex, .require ey => - match Expr.decEq ex ey with - | isTrue h => isTrue (by cases h; rfl) - | isFalse h => isFalse (by intro h'; cases h'; exact h rfl) - | .while cx bx, .while cy bodyY => - match Expr.decEq cx cy, Stmt.decEqList bx bodyY with - | isTrue hc, isTrue hb => isTrue (by cases hc; cases hb; rfl) - | isFalse hc, _ => isFalse (by intro h; cases h; exact hc rfl) - | _, isFalse hb => isFalse (by intro h; cases h; exact hb rfl) - | .ite cx tx ex, .ite cy ty ey => - match Expr.decEq cx cy, Stmt.decEqList tx ty, Stmt.decEqList ex ey with - | isTrue hc, isTrue ht, isTrue he => isTrue (by cases hc; cases ht; cases he; rfl) - | isFalse hc, _, _ => isFalse (by intro h; cases h; exact hc rfl) - | _, isFalse ht, _ => isFalse (by intro h; cases h; exact ht rfl) - | _, _, isFalse he => isFalse (by intro h; cases h; exact he rfl) - | .new nx vx ax rx sx, .new ny vy ay ry sy => - match (inferInstance : Decidable (nx = ny)), Expr.decEq vx vy, (inferInstance : Decidable (ax = ay)), (inferInstance : Decidable (rx = ry)), (inferInstance : Decidable (sx = sy)) with - | isTrue hn, isTrue hv, isTrue ha, isTrue hr, isTrue hs => isTrue (by cases hn; cases hv; cases ha; cases hr; cases hs; rfl) - | isFalse hn, _, _, _, _ => isFalse (by intro h; cases h; exact hn rfl) - | _, isFalse hv, _, _, _ => isFalse (by intro h; cases h; exact hv rfl) - | _, _, isFalse ha, _, _ => isFalse (by intro h; cases h; exact ha rfl) - | _, _, _, isFalse hr, _ => isFalse (by intro h; cases h; exact hr rfl) - | _, _, _, _, isFalse hs => isFalse (by intro h; cases h; exact hs rfl) - | .internalCall nx ax rx, .internalCall ny ay ry => - match (inferInstance : Decidable (nx = ny)), (inferInstance : Decidable (ax = ay)), (inferInstance : Decidable (rx = ry)) with - | isTrue hn, isTrue ha, isTrue hr => isTrue (by cases hn; cases ha; cases hr; rfl) - | isFalse hn, _, _ => isFalse (by intro h; cases h; exact hn rfl) - | _, isFalse ha, _ => isFalse (by intro h; cases h; exact ha rfl) - | _, _, isFalse hr => isFalse (by intro h; cases h; exact hr rfl) - | .externalCall tx nx vx ax rx px, .externalCall ty ny vy ay ry py => - match Expr.decEq tx ty, (inferInstance : Decidable (nx = ny)), Expr.decEq vx vy, - (inferInstance : Decidable (ax = ay)), (inferInstance : Decidable (rx = ry)), - (inferInstance : Decidable (px = py)) with - | isTrue ht, isTrue hn, isTrue hv, isTrue ha, isTrue hr, isTrue hp => - isTrue (by cases ht; cases hn; cases hv; cases ha; cases hr; cases hp; rfl) - | isFalse ht, _, _, _, _, _ => isFalse (by intro h; cases h; exact ht rfl) - | _, isFalse hn, _, _, _, _ => isFalse (by intro h; cases h; exact hn rfl) - | _, _, isFalse hv, _, _, _ => isFalse (by intro h; cases h; exact hv rfl) - | _, _, _, isFalse ha, _, _ => isFalse (by intro h; cases h; exact ha rfl) - | _, _, _, _, isFalse hr, _ => isFalse (by intro h; cases h; exact hr rfl) - | _, _, _, _, _, isFalse hp => isFalse (by intro h; cases h; exact hp rfl) - | .lowLevelCall tx vx cx ox dx px, .lowLevelCall ty vy cy oy dy py => - match Expr.decEq tx ty, Expr.decEq vx vy, Expr.decEq cx cy, (inferInstance : Decidable (ox = oy)), (inferInstance : Decidable (dx = dy)), (inferInstance : Decidable (px = py)) with - | isTrue ht, isTrue hv, isTrue hc, isTrue ho, isTrue hd, isTrue hp => isTrue (by cases ht; cases hv; cases hc; cases ho; cases hd; cases hp; rfl) - | isFalse ht, _, _, _, _, _ => isFalse (by intro h; cases h; exact ht rfl) - | _, isFalse hv, _, _, _, _ => isFalse (by intro h; cases h; exact hv rfl) - | _, _, isFalse hc, _, _, _ => isFalse (by intro h; cases h; exact hc rfl) - | _, _, _, isFalse ho, _, _ => isFalse (by intro h; cases h; exact ho rfl) - | _, _, _, _, isFalse hd, _ => isFalse (by intro h; cases h; exact hd rfl) - | _, _, _, _, _, isFalse hp => isFalse (by intro h; cases h; exact hp rfl) - | .delegateCall tx cx ox dx, .delegateCall ty cy oy dy => - match Expr.decEq tx ty, Expr.decEq cx cy, (inferInstance : Decidable (ox = oy)), - (inferInstance : Decidable (dx = dy)) with - | isTrue ht, isTrue hc, isTrue ho, isTrue hd => - isTrue (by cases ht; cases hc; cases ho; cases hd; rfl) - | isFalse ht, _, _, _ => isFalse (by intro h; cases h; exact ht rfl) - | _, isFalse hc, _, _ => isFalse (by intro h; cases h; exact hc rfl) - | _, _, isFalse ho, _ => isFalse (by intro h; cases h; exact ho rfl) - | _, _, _, isFalse hd => isFalse (by intro h; cases h; exact hd rfl) - | .checkedCall rx nx vx ax retx sx ex cx px, - .checkedCall ry ny vy ay rety sy ey cy py => - match Expr.decEq rx ry, (inferInstance : Decidable (nx = ny)), Expr.decEq vx vy, - (inferInstance : Decidable (ax = ay)), (inferInstance : Decidable (retx = rety)), - Stmt.decEqList sx sy, (inferInstance : Decidable (ex = ey)), Stmt.decEqList cx cy, - (inferInstance : Decidable (px = py)) with - | isTrue hr, isTrue hn, isTrue hv, isTrue ha, isTrue hret, isTrue hs, isTrue he, - isTrue hc, isTrue hp => - isTrue (by - cases hr; cases hn; cases hv; cases ha; cases hret; cases hs; cases he - cases hc; cases hp; rfl) - | isFalse hr, _, _, _, _, _, _, _, _ => isFalse (by intro h; cases h; exact hr rfl) - | _, isFalse hn, _, _, _, _, _, _, _ => isFalse (by intro h; cases h; exact hn rfl) - | _, _, isFalse hv, _, _, _, _, _, _ => isFalse (by intro h; cases h; exact hv rfl) - | _, _, _, isFalse ha, _, _, _, _, _ => isFalse (by intro h; cases h; exact ha rfl) - | _, _, _, _, isFalse hret, _, _, _, _ => isFalse (by intro h; cases h; exact hret rfl) - | _, _, _, _, _, isFalse hs, _, _, _ => isFalse (by intro h; cases h; exact hs rfl) - | _, _, _, _, _, _, isFalse he, _, _ => isFalse (by intro h; cases h; exact he rfl) - | _, _, _, _, _, _, _, isFalse hc, _ => isFalse (by intro h; cases h; exact hc rfl) - | _, _, _, _, _, _, _, _, isFalse hp => isFalse (by intro h; cases h; exact hp rfl) - | .return ex, .return ey => - match Expr.decEqList ex ey with - | isTrue h => isTrue (by cases h; rfl) - | isFalse h => isFalse (by intro h'; cases h'; exact h rfl) - | .break, .break => isTrue rfl - | .continue, .continue => isTrue rfl - | .letStorage _ _, .letDecl _ _ _ => isFalse (by intro h; cases h) - | .letDecl _ _ _, .letStorage _ _ => isFalse (by intro h; cases h) - | .letStorage _ _, .assign _ _ _ => isFalse (by intro h; cases h) - | .assign _ _ _, .letStorage _ _ => isFalse (by intro h; cases h) - | .letStorage _ _, .require _ => isFalse (by intro h; cases h) - | .require _, .letStorage _ _ => isFalse (by intro h; cases h) - | .letStorage _ _, .while _ _ => isFalse (by intro h; cases h) - | .while _ _, .letStorage _ _ => isFalse (by intro h; cases h) - | .letStorage _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .letStorage _ _ => isFalse (by intro h; cases h) - | .letStorage _ _, .new _ _ _ _ _ => isFalse (by intro h; cases h) - | .new _ _ _ _ _, .letStorage _ _ => isFalse (by intro h; cases h) - | .letStorage _ _, .internalCall _ _ _ => isFalse (by intro h; cases h) - | .internalCall _ _ _, .letStorage _ _ => isFalse (by intro h; cases h) - | .letStorage _ _, .externalCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .externalCall _ _ _ _ _ _, .letStorage _ _ => isFalse (by intro h; cases h) - | .letStorage _ _, .lowLevelCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .lowLevelCall _ _ _ _ _ _, .letStorage _ _ => isFalse (by intro h; cases h) - | .letStorage _ _, .checkedCall _ _ _ _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .checkedCall _ _ _ _ _ _ _ _ _, .letStorage _ _ => isFalse (by intro h; cases h) - | .letStorage _ _, .return _ => isFalse (by intro h; cases h) - | .return _, .letStorage _ _ => isFalse (by intro h; cases h) - | .letStorage _ _, .break => isFalse (by intro h; cases h) - | .break, .letStorage _ _ => isFalse (by intro h; cases h) - | .letStorage _ _, .continue => isFalse (by intro h; cases h) - | .continue, .letStorage _ _ => isFalse (by intro h; cases h) - | .letStorage _ _, .push _ _ => isFalse (by intro h; cases h) - | .push _ _, .letStorage _ _ => isFalse (by intro h; cases h) - | .letStorage _ _, .pop _ => isFalse (by intro h; cases h) - | .pop _, .letStorage _ _ => isFalse (by intro h; cases h) - | .letStorage _ _, .delete _ => isFalse (by intro h; cases h) - | .delete _, .letStorage _ _ => isFalse (by intro h; cases h) - | .letDecl _ _ _, .assign _ _ _ => isFalse (by intro h; cases h) - | .letDecl _ _ _, .require _ => isFalse (by intro h; cases h) - | .letDecl _ _ _, .while _ _ => isFalse (by intro h; cases h) - | .letDecl _ _ _, .new _ _ _ _ _ => isFalse (by intro h; cases h) - | .letDecl _ _ _, .internalCall _ _ _ => isFalse (by intro h; cases h) - | .letDecl _ _ _, .externalCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .letDecl _ _ _, .return _ => isFalse (by intro h; cases h) - | .letDecl _ _ _, .break => isFalse (by intro h; cases h) - | .letDecl _ _ _, .continue => isFalse (by intro h; cases h) - | .assign _ _ _, .letDecl _ _ _ => isFalse (by intro h; cases h) - | .assign _ _ _, .require _ => isFalse (by intro h; cases h) - | .assign _ _ _, .while _ _ => isFalse (by intro h; cases h) - | .assign _ _ _, .new _ _ _ _ _ => isFalse (by intro h; cases h) - | .assign _ _ _, .internalCall _ _ _ => isFalse (by intro h; cases h) - | .assign _ _ _, .externalCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .assign _ _ _, .return _ => isFalse (by intro h; cases h) - | .assign _ _ _, .break => isFalse (by intro h; cases h) - | .assign _ _ _, .continue => isFalse (by intro h; cases h) - | .require _, .letDecl _ _ _ => isFalse (by intro h; cases h) - | .require _, .assign _ _ _ => isFalse (by intro h; cases h) - | .require _, .while _ _ => isFalse (by intro h; cases h) - | .require _, .new _ _ _ _ _ => isFalse (by intro h; cases h) - | .require _, .internalCall _ _ _ => isFalse (by intro h; cases h) - | .require _, .externalCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .require _, .return _ => isFalse (by intro h; cases h) - | .require _, .break => isFalse (by intro h; cases h) - | .require _, .continue => isFalse (by intro h; cases h) - | .while _ _, .letDecl _ _ _ => isFalse (by intro h; cases h) - | .while _ _, .assign _ _ _ => isFalse (by intro h; cases h) - | .while _ _, .require _ => isFalse (by intro h; cases h) - | .while _ _, .new _ _ _ _ _ => isFalse (by intro h; cases h) - | .while _ _, .internalCall _ _ _ => isFalse (by intro h; cases h) - | .while _ _, .externalCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .while _ _, .return _ => isFalse (by intro h; cases h) - | .while _ _, .break => isFalse (by intro h; cases h) - | .while _ _, .continue => isFalse (by intro h; cases h) - | .new _ _ _ _ _, .letDecl _ _ _ => isFalse (by intro h; cases h) - | .new _ _ _ _ _, .assign _ _ _ => isFalse (by intro h; cases h) - | .new _ _ _ _ _, .require _ => isFalse (by intro h; cases h) - | .new _ _ _ _ _, .while _ _ => isFalse (by intro h; cases h) - | .new _ _ _ _ _, .internalCall _ _ _ => isFalse (by intro h; cases h) - | .new _ _ _ _ _, .externalCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .new _ _ _ _ _, .return _ => isFalse (by intro h; cases h) - | .new _ _ _ _ _, .break => isFalse (by intro h; cases h) - | .new _ _ _ _ _, .continue => isFalse (by intro h; cases h) - | .internalCall _ _ _, .letDecl _ _ _ => isFalse (by intro h; cases h) - | .internalCall _ _ _, .assign _ _ _ => isFalse (by intro h; cases h) - | .internalCall _ _ _, .require _ => isFalse (by intro h; cases h) - | .internalCall _ _ _, .while _ _ => isFalse (by intro h; cases h) - | .internalCall _ _ _, .new _ _ _ _ _ => isFalse (by intro h; cases h) - | .internalCall _ _ _, .externalCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .internalCall _ _ _, .return _ => isFalse (by intro h; cases h) - | .internalCall _ _ _, .break => isFalse (by intro h; cases h) - | .internalCall _ _ _, .continue => isFalse (by intro h; cases h) - | .externalCall _ _ _ _ _ _, .letDecl _ _ _ => isFalse (by intro h; cases h) - | .externalCall _ _ _ _ _ _, .assign _ _ _ => isFalse (by intro h; cases h) - | .externalCall _ _ _ _ _ _, .require _ => isFalse (by intro h; cases h) - | .externalCall _ _ _ _ _ _, .while _ _ => isFalse (by intro h; cases h) - | .externalCall _ _ _ _ _ _, .new _ _ _ _ _ => isFalse (by intro h; cases h) - | .externalCall _ _ _ _ _ _, .internalCall _ _ _ => isFalse (by intro h; cases h) - | .externalCall _ _ _ _ _ _, .return _ => isFalse (by intro h; cases h) - | .externalCall _ _ _ _ _ _, .break => isFalse (by intro h; cases h) - | .externalCall _ _ _ _ _ _, .continue => isFalse (by intro h; cases h) - | .return _, .letDecl _ _ _ => isFalse (by intro h; cases h) - | .return _, .assign _ _ _ => isFalse (by intro h; cases h) - | .return _, .require _ => isFalse (by intro h; cases h) - | .return _, .while _ _ => isFalse (by intro h; cases h) - | .return _, .new _ _ _ _ _ => isFalse (by intro h; cases h) - | .return _, .internalCall _ _ _ => isFalse (by intro h; cases h) - | .return _, .externalCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .return _, .break => isFalse (by intro h; cases h) - | .return _, .continue => isFalse (by intro h; cases h) - | .break, .letDecl _ _ _ => isFalse (by intro h; cases h) - | .break, .assign _ _ _ => isFalse (by intro h; cases h) - | .break, .require _ => isFalse (by intro h; cases h) - | .break, .while _ _ => isFalse (by intro h; cases h) - | .break, .new _ _ _ _ _ => isFalse (by intro h; cases h) - | .break, .internalCall _ _ _ => isFalse (by intro h; cases h) - | .break, .externalCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .break, .return _ => isFalse (by intro h; cases h) - | .break, .continue => isFalse (by intro h; cases h) - | .continue, .letDecl _ _ _ => isFalse (by intro h; cases h) - | .continue, .assign _ _ _ => isFalse (by intro h; cases h) - | .continue, .require _ => isFalse (by intro h; cases h) - | .continue, .while _ _ => isFalse (by intro h; cases h) - | .continue, .new _ _ _ _ _ => isFalse (by intro h; cases h) - | .continue, .internalCall _ _ _ => isFalse (by intro h; cases h) - | .continue, .externalCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .continue, .return _ => isFalse (by intro h; cases h) - | .continue, .break => isFalse (by intro h; cases h) - | .letDecl _ _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .assign _ _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .require _, .ite _ _ _ => isFalse (by intro h; cases h) - | .while _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .new _ _ _ _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .internalCall _ _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .externalCall _ _ _ _ _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .return _, .ite _ _ _ => isFalse (by intro h; cases h) - | .break, .ite _ _ _ => isFalse (by intro h; cases h) - | .continue, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .letDecl _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .assign _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .require _ => isFalse (by intro h; cases h) - | .ite _ _ _, .while _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .new _ _ _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .internalCall _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .externalCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .return _ => isFalse (by intro h; cases h) - | .ite _ _ _, .break => isFalse (by intro h; cases h) - | .ite _ _ _, .continue => isFalse (by intro h; cases h) - | .lowLevelCall _ _ _ _ _ _, .letDecl _ _ _ => isFalse (by intro h; cases h) - | .lowLevelCall _ _ _ _ _ _, .assign _ _ _ => isFalse (by intro h; cases h) - | .lowLevelCall _ _ _ _ _ _, .require _ => isFalse (by intro h; cases h) - | .lowLevelCall _ _ _ _ _ _, .while _ _ => isFalse (by intro h; cases h) - | .lowLevelCall _ _ _ _ _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .lowLevelCall _ _ _ _ _ _, .new _ _ _ _ _ => isFalse (by intro h; cases h) - | .lowLevelCall _ _ _ _ _ _, .internalCall _ _ _ => isFalse (by intro h; cases h) - | .lowLevelCall _ _ _ _ _ _, .externalCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .lowLevelCall _ _ _ _ _ _, .return _ => isFalse (by intro h; cases h) - | .lowLevelCall _ _ _ _ _ _, .break => isFalse (by intro h; cases h) - | .lowLevelCall _ _ _ _ _ _, .continue => isFalse (by intro h; cases h) - | .letDecl _ _ _, .lowLevelCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .assign _ _ _, .lowLevelCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .require _, .lowLevelCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .while _ _, .lowLevelCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .lowLevelCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .new _ _ _ _ _, .lowLevelCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .internalCall _ _ _, .lowLevelCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .externalCall _ _ _ _ _ _, .lowLevelCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .return _, .lowLevelCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .break, .lowLevelCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .continue, .lowLevelCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .checkedCall _ _ _ _ _ _ _ _ _, .letDecl _ _ _ => isFalse (by intro h; cases h) - | .checkedCall _ _ _ _ _ _ _ _ _, .assign _ _ _ => isFalse (by intro h; cases h) - | .checkedCall _ _ _ _ _ _ _ _ _, .require _ => isFalse (by intro h; cases h) - | .checkedCall _ _ _ _ _ _ _ _ _, .while _ _ => isFalse (by intro h; cases h) - | .checkedCall _ _ _ _ _ _ _ _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .checkedCall _ _ _ _ _ _ _ _ _, .new _ _ _ _ _ => isFalse (by intro h; cases h) - | .checkedCall _ _ _ _ _ _ _ _ _, .internalCall _ _ _ => isFalse (by intro h; cases h) - | .checkedCall _ _ _ _ _ _ _ _ _, .externalCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .checkedCall _ _ _ _ _ _ _ _ _, .lowLevelCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .checkedCall _ _ _ _ _ _ _ _ _, .return _ => isFalse (by intro h; cases h) - | .checkedCall _ _ _ _ _ _ _ _ _, .break => isFalse (by intro h; cases h) - | .checkedCall _ _ _ _ _ _ _ _ _, .continue => isFalse (by intro h; cases h) - | .letDecl _ _ _, .checkedCall _ _ _ _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .assign _ _ _, .checkedCall _ _ _ _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .require _, .checkedCall _ _ _ _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .while _ _, .checkedCall _ _ _ _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .checkedCall _ _ _ _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .new _ _ _ _ _, .checkedCall _ _ _ _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .internalCall _ _ _, .checkedCall _ _ _ _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .externalCall _ _ _ _ _ _, .checkedCall _ _ _ _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .lowLevelCall _ _ _ _ _ _, .checkedCall _ _ _ _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .return _, .checkedCall _ _ _ _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .break, .checkedCall _ _ _ _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .continue, .checkedCall _ _ _ _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .push rx vx, .push ry vy => - match StorageRef.decEq rx ry, (inferInstance : Decidable (vx = vy)) with - | isTrue hr, isTrue hv => isTrue (by cases hr; cases hv; rfl) - | isFalse hr, _ => isFalse (by intro h; cases h; exact hr rfl) - | _, isFalse hv => isFalse (by intro h; cases h; exact hv rfl) - | .pop rx, .pop ry => - match StorageRef.decEq rx ry with - | isTrue hr => isTrue (by cases hr; rfl) - | isFalse hr => isFalse (by intro h; cases h; exact hr rfl) - | .delete rx, .delete ry => - match StorageRef.decEq rx ry with - | isTrue hr => isTrue (by cases hr; rfl) - | isFalse hr => isFalse (by intro h; cases h; exact hr rfl) - | .delete _, .letDecl _ _ _ => isFalse (by intro h; cases h) - | .letDecl _ _ _, .delete _ => isFalse (by intro h; cases h) - | .delete _, .assign _ _ _ => isFalse (by intro h; cases h) - | .assign _ _ _, .delete _ => isFalse (by intro h; cases h) - | .delete _, .require _ => isFalse (by intro h; cases h) - | .require _, .delete _ => isFalse (by intro h; cases h) - | .delete _, .while _ _ => isFalse (by intro h; cases h) - | .while _ _, .delete _ => isFalse (by intro h; cases h) - | .delete _, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .delete _ => isFalse (by intro h; cases h) - | .delete _, .new _ _ _ _ _ => isFalse (by intro h; cases h) - | .new _ _ _ _ _, .delete _ => isFalse (by intro h; cases h) - | .delete _, .internalCall _ _ _ => isFalse (by intro h; cases h) - | .internalCall _ _ _, .delete _ => isFalse (by intro h; cases h) - | .delete _, .externalCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .externalCall _ _ _ _ _ _, .delete _ => isFalse (by intro h; cases h) - | .delete _, .lowLevelCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .lowLevelCall _ _ _ _ _ _, .delete _ => isFalse (by intro h; cases h) - | .delete _, .checkedCall _ _ _ _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .checkedCall _ _ _ _ _ _ _ _ _, .delete _ => isFalse (by intro h; cases h) - | .delete _, .return _ => isFalse (by intro h; cases h) - | .return _, .delete _ => isFalse (by intro h; cases h) - | .delete _, .break => isFalse (by intro h; cases h) - | .break, .delete _ => isFalse (by intro h; cases h) - | .delete _, .continue => isFalse (by intro h; cases h) - | .continue, .delete _ => isFalse (by intro h; cases h) - | .delete _, .push _ _ => isFalse (by intro h; cases h) - | .push _ _, .delete _ => isFalse (by intro h; cases h) - | .delete _, .pop _ => isFalse (by intro h; cases h) - | .pop _, .delete _ => isFalse (by intro h; cases h) - | .push _ _, .letDecl _ _ _ => isFalse (by intro h; cases h) - | .letDecl _ _ _, .push _ _ => isFalse (by intro h; cases h) - | .push _ _, .assign _ _ _ => isFalse (by intro h; cases h) - | .assign _ _ _, .push _ _ => isFalse (by intro h; cases h) - | .push _ _, .require _ => isFalse (by intro h; cases h) - | .require _, .push _ _ => isFalse (by intro h; cases h) - | .push _ _, .while _ _ => isFalse (by intro h; cases h) - | .while _ _, .push _ _ => isFalse (by intro h; cases h) - | .push _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .push _ _ => isFalse (by intro h; cases h) - | .push _ _, .new _ _ _ _ _ => isFalse (by intro h; cases h) - | .new _ _ _ _ _, .push _ _ => isFalse (by intro h; cases h) - | .push _ _, .internalCall _ _ _ => isFalse (by intro h; cases h) - | .internalCall _ _ _, .push _ _ => isFalse (by intro h; cases h) - | .push _ _, .externalCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .externalCall _ _ _ _ _ _, .push _ _ => isFalse (by intro h; cases h) - | .push _ _, .lowLevelCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .lowLevelCall _ _ _ _ _ _, .push _ _ => isFalse (by intro h; cases h) - | .push _ _, .checkedCall _ _ _ _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .checkedCall _ _ _ _ _ _ _ _ _, .push _ _ => isFalse (by intro h; cases h) - | .push _ _, .return _ => isFalse (by intro h; cases h) - | .return _, .push _ _ => isFalse (by intro h; cases h) - | .push _ _, .break => isFalse (by intro h; cases h) - | .break, .push _ _ => isFalse (by intro h; cases h) - | .push _ _, .continue => isFalse (by intro h; cases h) - | .continue, .push _ _ => isFalse (by intro h; cases h) - | .push _ _, .pop _ => isFalse (by intro h; cases h) - | .pop _, .push _ _ => isFalse (by intro h; cases h) - | .pop _, .letDecl _ _ _ => isFalse (by intro h; cases h) - | .letDecl _ _ _, .pop _ => isFalse (by intro h; cases h) - | .pop _, .assign _ _ _ => isFalse (by intro h; cases h) - | .assign _ _ _, .pop _ => isFalse (by intro h; cases h) - | .pop _, .require _ => isFalse (by intro h; cases h) - | .require _, .pop _ => isFalse (by intro h; cases h) - | .pop _, .while _ _ => isFalse (by intro h; cases h) - | .while _ _, .pop _ => isFalse (by intro h; cases h) - | .pop _, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .pop _ => isFalse (by intro h; cases h) - | .pop _, .new _ _ _ _ _ => isFalse (by intro h; cases h) - | .new _ _ _ _ _, .pop _ => isFalse (by intro h; cases h) - | .pop _, .internalCall _ _ _ => isFalse (by intro h; cases h) - | .internalCall _ _ _, .pop _ => isFalse (by intro h; cases h) - | .pop _, .externalCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .externalCall _ _ _ _ _ _, .pop _ => isFalse (by intro h; cases h) - | .pop _, .lowLevelCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .lowLevelCall _ _ _ _ _ _, .pop _ => isFalse (by intro h; cases h) - | .pop _, .checkedCall _ _ _ _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .checkedCall _ _ _ _ _ _ _ _ _, .pop _ => isFalse (by intro h; cases h) - | .pop _, .return _ => isFalse (by intro h; cases h) - | .return _, .pop _ => isFalse (by intro h; cases h) - | .pop _, .break => isFalse (by intro h; cases h) - | .break, .pop _ => isFalse (by intro h; cases h) - | .pop _, .continue => isFalse (by intro h; cases h) - | .continue, .pop _ => isFalse (by intro h; cases h) - | .for ix cx px bx, .for iy cy py by_ => - match Stmt.decEqList ix iy, Expr.decEq cx cy, Stmt.decEqList px py, Stmt.decEqList bx by_ with - | isTrue hi, isTrue hc, isTrue hp, isTrue hb => isTrue (by cases hi; cases hc; cases hp; cases hb; rfl) - | isFalse hi, _, _, _ => isFalse (by intro h; cases h; exact hi rfl) - | _, isFalse hc, _, _ => isFalse (by intro h; cases h; exact hc rfl) - | _, _, isFalse hp, _ => isFalse (by intro h; cases h; exact hp rfl) - | _, _, _, isFalse hb => isFalse (by intro h; cases h; exact hb rfl) - | .for _ _ _ _, .letDecl _ _ _ => isFalse (by intro h; cases h) - | .letDecl _ _ _, .for _ _ _ _ => isFalse (by intro h; cases h) - | .for _ _ _ _, .letStorage _ _ => isFalse (by intro h; cases h) - | .letStorage _ _, .for _ _ _ _ => isFalse (by intro h; cases h) - | .for _ _ _ _, .assign _ _ _ => isFalse (by intro h; cases h) - | .assign _ _ _, .for _ _ _ _ => isFalse (by intro h; cases h) - | .for _ _ _ _, .require _ => isFalse (by intro h; cases h) - | .require _, .for _ _ _ _ => isFalse (by intro h; cases h) - | .for _ _ _ _, .while _ _ => isFalse (by intro h; cases h) - | .while _ _, .for _ _ _ _ => isFalse (by intro h; cases h) - | .for _ _ _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .for _ _ _ _ => isFalse (by intro h; cases h) - | .for _ _ _ _, .new _ _ _ _ _ => isFalse (by intro h; cases h) - | .new _ _ _ _ _, .for _ _ _ _ => isFalse (by intro h; cases h) - | .for _ _ _ _, .internalCall _ _ _ => isFalse (by intro h; cases h) - | .internalCall _ _ _, .for _ _ _ _ => isFalse (by intro h; cases h) - | .for _ _ _ _, .externalCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .externalCall _ _ _ _ _ _, .for _ _ _ _ => isFalse (by intro h; cases h) - | .for _ _ _ _, .lowLevelCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .lowLevelCall _ _ _ _ _ _, .for _ _ _ _ => isFalse (by intro h; cases h) - | .for _ _ _ _, .checkedCall _ _ _ _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .checkedCall _ _ _ _ _ _ _ _ _, .for _ _ _ _ => isFalse (by intro h; cases h) - | .for _ _ _ _, .return _ => isFalse (by intro h; cases h) - | .return _, .for _ _ _ _ => isFalse (by intro h; cases h) - | .for _ _ _ _, .break => isFalse (by intro h; cases h) - | .break, .for _ _ _ _ => isFalse (by intro h; cases h) - | .for _ _ _ _, .continue => isFalse (by intro h; cases h) - | .continue, .for _ _ _ _ => isFalse (by intro h; cases h) - | .for _ _ _ _, .push _ _ => isFalse (by intro h; cases h) - | .push _ _, .for _ _ _ _ => isFalse (by intro h; cases h) - | .for _ _ _ _, .pop _ => isFalse (by intro h; cases h) - | .pop _, .for _ _ _ _ => isFalse (by intro h; cases h) - | .for _ _ _ _, .delete _ => isFalse (by intro h; cases h) - | .delete _, .for _ _ _ _ => isFalse (by intro h; cases h) - | .delegateCall _ _ _ _, .letDecl _ _ _ => isFalse (by intro h; cases h) - | .letDecl _ _ _, .delegateCall _ _ _ _ => isFalse (by intro h; cases h) - | .delegateCall _ _ _ _, .letStorage _ _ => isFalse (by intro h; cases h) - | .letStorage _ _, .delegateCall _ _ _ _ => isFalse (by intro h; cases h) - | .delegateCall _ _ _ _, .assign _ _ _ => isFalse (by intro h; cases h) - | .assign _ _ _, .delegateCall _ _ _ _ => isFalse (by intro h; cases h) - | .delegateCall _ _ _ _, .require _ => isFalse (by intro h; cases h) - | .require _, .delegateCall _ _ _ _ => isFalse (by intro h; cases h) - | .delegateCall _ _ _ _, .while _ _ => isFalse (by intro h; cases h) - | .while _ _, .delegateCall _ _ _ _ => isFalse (by intro h; cases h) - | .delegateCall _ _ _ _, .for _ _ _ _ => isFalse (by intro h; cases h) - | .for _ _ _ _, .delegateCall _ _ _ _ => isFalse (by intro h; cases h) - | .delegateCall _ _ _ _, .ite _ _ _ => isFalse (by intro h; cases h) - | .ite _ _ _, .delegateCall _ _ _ _ => isFalse (by intro h; cases h) - | .delegateCall _ _ _ _, .new _ _ _ _ _ => isFalse (by intro h; cases h) - | .new _ _ _ _ _, .delegateCall _ _ _ _ => isFalse (by intro h; cases h) - | .delegateCall _ _ _ _, .internalCall _ _ _ => isFalse (by intro h; cases h) - | .internalCall _ _ _, .delegateCall _ _ _ _ => isFalse (by intro h; cases h) - | .delegateCall _ _ _ _, .externalCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .externalCall _ _ _ _ _ _, .delegateCall _ _ _ _ => isFalse (by intro h; cases h) - | .delegateCall _ _ _ _, .lowLevelCall _ _ _ _ _ _ => isFalse (by intro h; cases h) - | .lowLevelCall _ _ _ _ _ _, .delegateCall _ _ _ _ => isFalse (by intro h; cases h) - | .delegateCall _ _ _ _, .checkedCall _ _ _ _ _ _ _ _ _ => - isFalse (by intro h; cases h) - | .checkedCall _ _ _ _ _ _ _ _ _, .delegateCall _ _ _ _ => - isFalse (by intro h; cases h) - | .delegateCall _ _ _ _, .return _ => isFalse (by intro h; cases h) - | .return _, .delegateCall _ _ _ _ => isFalse (by intro h; cases h) - | .delegateCall _ _ _ _, .break => isFalse (by intro h; cases h) - | .break, .delegateCall _ _ _ _ => isFalse (by intro h; cases h) - | .delegateCall _ _ _ _, .continue => isFalse (by intro h; cases h) - | .continue, .delegateCall _ _ _ _ => isFalse (by intro h; cases h) - | .delegateCall _ _ _ _, .push _ _ => isFalse (by intro h; cases h) - | .push _ _, .delegateCall _ _ _ _ => isFalse (by intro h; cases h) - | .delegateCall _ _ _ _, .pop _ => isFalse (by intro h; cases h) - | .pop _, .delegateCall _ _ _ _ => isFalse (by intro h; cases h) - | .delegateCall _ _ _ _, .delete _ => isFalse (by intro h; cases h) - | .delete _, .delegateCall _ _ _ _ => isFalse (by intro h; cases h) - - private def Stmt.decEqList : (as bs : List Stmt) -> Decidable (as = bs) + private def Stmt.decEq (a b : Stmt) : Decidable (a = b) := by + cases a <;> cases b + all_goals first + | exact isFalse (by intro h; contradiction) + | skip + next nx tx ex ny ty ey => + letI : Decidable (ex = ey) := Expr.decEq ex ey + exact decEqOfIff (nx = ny ∧ tx = ty ∧ ex = ey) + (by rintro ⟨rfl, rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl, rfl⟩) + next nx rx ny ry => + letI : Decidable (rx = ry) := StorageRef.decEq rx ry + exact decEqOfIff (nx = ny ∧ rx = ry) + (by rintro ⟨rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl⟩) + next nx ny => + exact decEqOfIff (nx = ny) (by intro h; cases h; rfl) (by intro h; cases h; rfl) + next ox rx ex oy ry ey => + letI : Decidable (rx = ry) := StorageRef.decEq rx ry + letI : Decidable (ex = ey) := Expr.decEq ex ey + exact decEqOfIff (ox = oy ∧ rx = ry ∧ ex = ey) + (by rintro ⟨rfl, rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl, rfl⟩) + next ex ey => + letI : Decidable (ex = ey) := Expr.decEq ex ey + exact decEqOfIff (ex = ey) (by intro h; cases h; rfl) (by intro h; cases h; rfl) + next cx bx cy bys => + letI : Decidable (cx = cy) := Expr.decEq cx cy + letI : Decidable (bx = bys) := Stmt.decEqList bx bys + exact decEqOfIff (cx = cy ∧ bx = bys) + (by rintro ⟨rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl⟩) + next ix cx px bx iy cy py bys => + letI : Decidable (ix = iy) := Stmt.decEqList ix iy + letI : Decidable (cx = cy) := Expr.decEq cx cy + letI : Decidable (px = py) := Stmt.decEqList px py + letI : Decidable (bx = bys) := Stmt.decEqList bx bys + exact decEqOfIff (ix = iy ∧ cx = cy ∧ px = py ∧ bx = bys) + (by rintro ⟨rfl, rfl, rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl, rfl, rfl⟩) + next cx tx fx cy ty fy => + letI : Decidable (cx = cy) := Expr.decEq cx cy + letI : Decidable (tx = ty) := Stmt.decEqList tx ty + letI : Decidable (fx = fy) := Stmt.decEqList fx fy + exact decEqOfIff (cx = cy ∧ tx = ty ∧ fx = fy) + (by rintro ⟨rfl, rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl, rfl⟩) + next nx vx argsx retx saltx ny vy argsy rety salty => + letI : Decidable (vx = vy) := Expr.decEq vx vy + exact decEqOfIff (nx = ny ∧ vx = vy ∧ argsx = argsy ∧ retx = rety ∧ saltx = salty) + (by rintro ⟨rfl, rfl, rfl, rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl, rfl, rfl, rfl⟩) + next nx xs rx ny ys ry => + exact decEqOfIff (nx = ny ∧ xs = ys ∧ rx = ry) + (by rintro ⟨rfl, rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl, rfl⟩) + next rx nx vx argsx retx permx ry ny vy argsy rety permy => + letI : Decidable (rx = ry) := Expr.decEq rx ry + letI : Decidable (vx = vy) := Expr.decEq vx vy + exact decEqOfIff + (rx = ry ∧ nx = ny ∧ vx = vy ∧ argsx = argsy ∧ retx = rety ∧ permx = permy) + (by rintro ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩) + next tx vx cdx okx datax permx ty vy cdy oky datay permy => + letI : Decidable (tx = ty) := Expr.decEq tx ty + letI : Decidable (vx = vy) := Expr.decEq vx vy + letI : Decidable (cdx = cdy) := Expr.decEq cdx cdy + exact decEqOfIff + (tx = ty ∧ vx = vy ∧ cdx = cdy ∧ okx = oky ∧ datax = datay ∧ permx = permy) + (by rintro ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl, rfl, rfl, rfl, rfl⟩) + next tx cdx okx datax ty cdy oky datay => + letI : Decidable (tx = ty) := Expr.decEq tx ty + letI : Decidable (cdx = cdy) := Expr.decEq cdx cdy + exact decEqOfIff (tx = ty ∧ cdx = cdy ∧ okx = oky ∧ datax = datay) + (by rintro ⟨rfl, rfl, rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl, rfl, rfl⟩) + next rx nx vx argsx retx sx errx fx permx ry ny vy argsy rety sy erry fy permy => + letI : Decidable (rx = ry) := Expr.decEq rx ry + letI : Decidable (vx = vy) := Expr.decEq vx vy + letI : Decidable (sx = sy) := Stmt.decEqList sx sy + letI : Decidable (fx = fy) := Stmt.decEqList fx fy + exact decEqOfIff + (rx = ry ∧ nx = ny ∧ vx = vy ∧ argsx = argsy ∧ retx = rety ∧ sx = sy ∧ + errx = erry ∧ fx = fy ∧ permx = permy) + (by rintro ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩) + next xs ys => + exact decEqOfIff (xs = ys) (by intro h; cases h; rfl) (by intro h; cases h; rfl) + next => + exact isTrue rfl + next => + exact isTrue rfl + next rx vx ry vy => + letI : Decidable (rx = ry) := StorageRef.decEq rx ry + exact decEqOfIff (rx = ry ∧ vx = vy) + (by rintro ⟨rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl⟩) + next rx ry => + letI : Decidable (rx = ry) := StorageRef.decEq rx ry + exact decEqOfIff (rx = ry) (by intro h; cases h; rfl) (by intro h; cases h; rfl) + next rx ry => + letI : Decidable (rx = ry) := StorageRef.decEq rx ry + exact decEqOfIff (rx = ry) (by intro h; cases h; rfl) (by intro h; cases h; rfl) + + private def Stmt.decEqList : (as bs : List Stmt) → Decidable (as = bs) | [], [] => isTrue rfl | a :: as, b :: bs => - match Stmt.decEq a b, Stmt.decEqList as bs with - | isTrue ha, isTrue hs => isTrue (by cases ha; cases hs; rfl) - | isFalse ha, _ => isFalse (by intro h; cases h; exact ha rfl) - | _, isFalse hs => isFalse (by intro h; cases h; exact hs rfl) + letI : Decidable (a = b) := Stmt.decEq a b + letI : Decidable (as = bs) := Stmt.decEqList as bs + decEqOfIff (a = b ∧ as = bs) + (by rintro ⟨rfl, rfl⟩; rfl) + (by intro h; cases h; exact ⟨rfl, rfl⟩) | [], _ :: _ => isFalse (by intro h; cases h) | _ :: _, [] => isFalse (by intro h; cases h) end -instance : DecidableEq Stmt := - Stmt.decEq +instance : DecidableEq Stmt := Stmt.decEq deriving instance DecidableEq for Param - deriving instance DecidableEq for StorageDecl - deriving instance DecidableEq for ConstructorDecl - deriving instance DecidableEq for StructDecl - deriving instance DecidableEq for FunctionDecl - deriving instance DecidableEq for TransitionDecl - deriving instance DecidableEq for ContractDecl end Solm