| import WordDialect.Machine |
|
|
| /-! |
| # WordDialect.Stack |
|
|
| Stack-operation correctness for `exec`. |
|
|
| * `exec_underflow`: an instruction whose operands are not all present traps with |
| `stackUnderflow` and does nothing else. |
| * `exec_not_underflow`: with enough operands, the instruction never traps with |
| `stackUnderflow`. |
| * `exec_depth`: whenever an instruction continues, the data-stack depth changes by exactly |
| `pushes - pops`. |
| -/ |
|
|
| namespace WordDialect |
|
|
| namespace Instr |
|
|
| /-- Operands consumed from the data stack. -/ |
| def pops {n : Nat} : Instr n → Nat |
| | .word _ | .ptr _ | .jmp _ | .call _ | .ret | .push _ | .halt | .fromr | .rfetch => 0 |
| | .load | .not | .branch _ | .pop _ | .dup | .drop | .tor => 1 |
| | .store | .add | .sub | .mul | .div | .sdiv | .and | .or | .xor |
| | .shl | .shr | .rotl | .rotr | .cmp _ | .swap | .over => 2 |
| | .select | .rot => 3 |
|
|
| /-- Results produced on the data stack. -/ |
| def pushes {n : Nat} : Instr n → Nat |
| | .word _ | .ptr _ | .load | .push _ | .fromr | .rfetch => 1 |
| | .add | .sub | .mul | .div | .sdiv | .and | .or | .xor | .not |
| | .shl | .shr | .rotl | .rotr | .cmp _ | .select => 1 |
| | .store | .jmp _ | .branch _ | .call _ | .ret | .pop _ | .drop | .halt | .tor => 0 |
| | .dup => 2 |
| | .swap => 2 |
| | .over => 3 |
| | .rot => 3 |
|
|
| end Instr |
|
|
| theorem exec_underflow {n : Nat} (i : Instr n) (s : State n) |
| (h : s.dstack.length < i.pops) : exec i s = .trapped .stackUnderflow := by |
| obtain ⟨pc, d, rs, as, regs, mem⟩ := s |
| cases i <;> simp only [Instr.pops] at h <;> |
| (rcases d with _ | ⟨x, _ | ⟨y, _ | ⟨z, d⟩⟩⟩ <;> |
| first | (simp at h; done) | (simp at h; omega) | (exfalso; omega) | simp [exec]) |
|
|
| theorem exec_not_underflow {n : Nat} (i : Instr n) (s : State n) |
| (h : i.pops ≤ s.dstack.length) : exec i s ≠ .trapped .stackUnderflow := by |
| obtain ⟨pc, d, rs, as, regs, mem⟩ := s |
| cases i <;> simp only [Instr.pops] at h <;> |
| (rcases d with _ | ⟨x, _ | ⟨y, _ | ⟨z, d⟩⟩⟩ <;> |
| first | (simp at h; done) | (simp at h; omega) | (exfalso; omega) | |
| (simp [exec, State.fall]; try split <;> simp)) |
|
|
| end WordDialect |
|
|
