| import WordDialect |
| import WordIR |
|
|
| /-! |
| # Forth.Semantics |
|
|
| Reference semantics of the supported Forth subset, defined directly on a Forth state |
| (data stack + memory) with no reference to the machine or the IR. The translation to |
| Universal Word IR is proved correct against this definition. |
|
|
| Conventions (ANS Forth): |
| * `/` is signed division truncating toward zero (symmetric division) |
| * `MOD` is the remainder consistent with `/`: `a MOD b = a - (a / b) * b`, so its sign follows |
| `a`; `MOD` by zero traps `divideByZero`, like `/`. |
| * Truth flags are all-ones (`-1`) for true and `0` for false |
| anything else into `0`. |
| * `@ ( addr -- x )`, `! ( x addr -- )`; memory is word-addressed. |
| * `lshift`/`rshift` are logical shifts. |
| * `/MOD ( a b -- rem quot )` is `MOD` and `/` together |
| `MAX` compare as signed numbers (`ABS` of the most negative number is itself, as it wraps). |
| `2DUP 2DROP 2SWAP` act on pairs. |
| * Double-cell numbers are pairs `( lo hi )`, `hi` on top, standing for `hi * 2^n + lo`. |
| `UM* ( a b -- lo hi )` is the full unsigned product. `UM/MOD ( lo hi u -- rem quot )` divides |
| the unsigned double-cell number by `u`; it traps `divideByZero` unless `hi < u`, which is |
| exactly when the quotient fits in one word (so also when `u = 0`). `M* ( a b -- lo hi )` is the |
| full signed product: `lo` and `hi` are the two words of `a * b` as a `2n`-bit two's-complement |
| number (`hi` is `a * b / 2^n`, rounded down). `SM/REM ( lo hi v -- rem quot )` divides the |
| signed double-cell number `hi * 2^n + lo` by `v` with truncation toward zero (`Int.tdiv` and |
| `Int.tmod`, like `/` and `MOD`) |
| fit in a signed word. |
| * `FM/MOD ( lo hi v -- rem quot )` is floored division of the same double-cell number |
| (`Int.fdiv` and `Int.fmod`: the quotient rounds toward negative infinity and the remainder |
| takes the sign of `v`) |
| * `*/MOD ( n1 n2 n3 -- rem quot )` divides the full product `n1 * n2` (never wrapped) by `n3`, as |
| `M*` then `SM/REM`, trapping in the same cases |
|
|
| Memory: `FState.mem` is the whole IR memory |
| cells. The `VARIABLE`s of a program are the cells `0 … vars - 1` (`Program.vars`) |
| may assume exactly that those cells are valid (`Program.MemOk`) and nothing about any other |
| cell, nor about the initial contents of any cell. A variable's name pushes its address, so |
| after parsing it is a literal |
|
|
| `EXIT` leaves the word being executed and `LEAVE` the innermost loop, so a run of a block ends |
| in one of four ways (`Res`): it falls off the end, it executes `EXIT`, it executes `LEAVE`, or it |
| traps. |
|
|
| Return-data stack: `FState.rstack` is a stack of words *separate from the call frames*, exactly |
| like the IR's auxiliary stack `astack` (which a call or return never touches). `>R` moves the |
| data-stack top onto it (`stackUnderflow` if the data stack is empty), `R>` moves its top back and |
| `R@` copies it (both `returnUnderflow` if it is empty). Because call frames live elsewhere, using |
| it unbalanced across `EXIT`, a call or a return is *defined* behaviour here (the values simply |
| stay on it), whereas ANS Forth leaves it undefined. |
|
|
| `limit start DO body LOOP` (`Block.doLoop`): pushes `limit`, then `start` (the index) onto the |
| return-data stack (`stackUnderflow` if the data stack has fewer than two items), then runs |
| `body` at least once. After each run of `body` the two top return-data items are taken as |
| `index` (top) and `limit` (`returnUnderflow` if there are fewer than two) |
| `index + 1`, and the loop ends, dropping both, exactly when `index + 1 = limit` (modular |
| equality, so `0 0 DO … LOOP` runs `2^n` times |
| the equal case, which is the only case for a loop that counts up by one). Otherwise the |
| parameters `index + 1` and `limit` are put back and `body` runs again. `I` (`Op.loopI`) copies the |
| top of the return-data stack (the innermost index |
| (`Op.loopJ`) its third item (the next outer index): both are defined everywhere, trapping |
| `returnUnderflow` when the stack is too short, so they are also allowed outside a loop. Loop |
| parameters live on the return-data stack, so they survive calls and recursion. An `EXIT` (or a |
| trap) inside a loop body ends the loop and the word *without* removing the loop parameters: they |
| stay on the return-data stack, just as the compiled `RET` leaves the IR's auxiliary stack alone. |
| `UNLOOP` (`Op.unloop`) removes the top two return-data items (`returnUnderflow` if there are |
| fewer), so `UNLOOP EXIT` leaves a loop and its word cleanly. |
|
|
| `limit start DO body step +LOOP` (`Block.plusLoop`) is the same, except that after each run of |
| `body` the step is taken from the data stack (`returnUnderflow` first if the return-data stack |
| holds fewer than two items, then `stackUnderflow` if the data stack is empty), the index becomes |
| `index + step`, and the loop ends when `loopCrossed index limit step` holds: the index crossed |
| the boundary between `limit - 1` and `limit` (ANS Forth's rule, see `Forth.LoopProps`). |
|
|
| `LEAVE` (`Block.leave`) removes the loop parameters (`returnUnderflow` if there are fewer than |
| two return-data items) and ends the innermost enclosing loop at once: its result `Res.leave st` |
| propagates out of `IF` and `BEGIN … UNTIL` like `EXIT`, and the loop continues with the code |
| after `LOOP`/`+LOOP` from `st`. The parser only accepts `LEAVE` inside a loop of its own block |
| elsewhere it is still defined: it ends a called word like `EXIT` (`Res.returned`), and the main |
| block like falling off its end. `?DO` needs no rule: it is parsed to an `IF` around `DO`. |
|
|
| `BEGIN cond WHILE body REPEAT` (`Block.whileL`) runs `cond`, which leaves a flag (`stackUnderflow` |
| if the data stack is then empty). A false flag ends the loop |
| again with `cond`. `EXIT`, `LEAVE` and traps in `cond` or `body` end it like any other block. |
| -/ |
|
|
| namespace WordDialect |
| namespace Forth |
|
|
| open IR |
|
|
| inductive Op where |
| | lit (z : Int) |
| | dup | drop | swap | over | rot |
| | add | sub | mul | div | mod |
| | and | or | xor | invert | lshift | rshift |
| | eq | ne | lt | gt | ult | ugt | zeq |
| | fetch | store |
| | tor | fromr | rfetch | loopI | loopJ | unloop |
| | twoDup | twoDrop | twoSwap | divMod | negate | abs | min | max |
| | umStar | umDivMod | mStar | smRem | starSlashMod | starSlash | fmMod |
| deriving DecidableEq, Repr |
|
|
| /-- A Forth state: the data stack, memory, and the return-data stack (`>R`/`R>`/`R@` and the |
| `DO … LOOP` parameters |
| structure FState (n : Nat) where |
| stack : List (Word n) |
| mem : Memory n |
| rstack : List (Word n) |
|
|
|
|
| namespace Op |
|
|
| def sem {n : Nat} : Op → FState n → Except Trap (FState n) |
| | .lit z, st => .ok { st with stack := BitVec.ofInt n z :: st.stack } |
| | .dup, ⟨a :: d, m, r⟩ => .ok ⟨a :: a :: d, m, r⟩ |
| | .drop, ⟨_ :: d, m, r⟩ => .ok ⟨d, m, r⟩ |
| | .swap, ⟨b :: a :: d, m, r⟩ => .ok ⟨a :: b :: d, m, r⟩ |
| | .over, ⟨b :: a :: d, m, r⟩ => .ok ⟨a :: b :: a :: d, m, r⟩ |
| | .rot, ⟨c :: b :: a :: d, m, r⟩ => .ok ⟨a :: c :: b :: d, m, r⟩ |
| | .add, ⟨b :: a :: d, m, r⟩ => .ok ⟨(a + b) :: d, m, r⟩ |
| | .sub, ⟨b :: a :: d, m, r⟩ => .ok ⟨(a - b) :: d, m, r⟩ |
| | .mul, ⟨b :: a :: d, m, r⟩ => .ok ⟨(a * b) :: d, m, r⟩ |
| | .div, ⟨b :: a :: d, m, r⟩ => |
| if b = 0#n then .error .divideByZero else .ok ⟨a.sdiv b :: d, m, r⟩ |
| | .mod, ⟨b :: a :: d, m, r⟩ => |
| if b = 0#n then .error .divideByZero else .ok ⟨(a - a.sdiv b * b) :: d, m, r⟩ |
| | .and, ⟨b :: a :: d, m, r⟩ => .ok ⟨(a &&& b) :: d, m, r⟩ |
| | .or, ⟨b :: a :: d, m, r⟩ => .ok ⟨(a ||| b) :: d, m, r⟩ |
| | .xor, ⟨b :: a :: d, m, r⟩ => .ok ⟨(a ^^^ b) :: d, m, r⟩ |
| | .invert, ⟨a :: d, m, r⟩ => .ok ⟨(~~~a) :: d, m, r⟩ |
| | .lshift, ⟨u :: x :: d, m, r⟩ => .ok ⟨Word.shl x u :: d, m, r⟩ |
| | .rshift, ⟨u :: x :: d, m, r⟩ => .ok ⟨Word.shr x u :: d, m, r⟩ |
| | .eq, ⟨b :: a :: d, m, r⟩ => .ok ⟨flag (Cond.eval .eq a b) :: d, m, r⟩ |
| | .ne, ⟨b :: a :: d, m, r⟩ => .ok ⟨flag (Cond.eval .ne a b) :: d, m, r⟩ |
| | .lt, ⟨b :: a :: d, m, r⟩ => .ok ⟨flag (Cond.eval .slt a b) :: d, m, r⟩ |
| | .gt, ⟨b :: a :: d, m, r⟩ => .ok ⟨flag (Cond.eval .sgt a b) :: d, m, r⟩ |
| | .ult, ⟨b :: a :: d, m, r⟩ => .ok ⟨flag (Cond.eval .ult a b) :: d, m, r⟩ |
| | .ugt, ⟨b :: a :: d, m, r⟩ => .ok ⟨flag (Cond.eval .ugt a b) :: d, m, r⟩ |
| | .zeq, ⟨a :: d, m, r⟩ => .ok ⟨flag (Cond.eval .eq a 0#n) :: d, m, r⟩ |
| | .fetch, ⟨a :: d, m, r⟩ => |
| match m.read? a with |
| | some v => .ok ⟨v :: d, m, r⟩ |
| | none => .error .badAddress |
| | .store, ⟨a :: v :: d, m, r⟩ => |
| match m.write? a v with |
| | some m' => .ok ⟨d, m', r⟩ |
| | none => .error .badAddress |
| | .twoDup, ⟨b :: a :: d, m, r⟩ => .ok ⟨b :: a :: b :: a :: d, m, r⟩ |
| | .twoDrop, ⟨_ :: _ :: d, m, r⟩ => .ok ⟨d, m, r⟩ |
| | .twoSwap, ⟨x4 :: x3 :: x2 :: x1 :: d, m, r⟩ => .ok ⟨x2 :: x1 :: x4 :: x3 :: d, m, r⟩ |
| | .divMod, ⟨b :: a :: d, m, r⟩ => |
| if b = 0#n then .error .divideByZero else .ok ⟨a.sdiv b :: (a - a.sdiv b * b) :: d, m, r⟩ |
| | .negate, ⟨a :: d, m, r⟩ => .ok ⟨(0#n - a) :: d, m, r⟩ |
| | .abs, ⟨a :: d, m, r⟩ => .ok ⟨(if Cond.eval .slt a 0#n then 0#n - a else a) :: d, m, r⟩ |
| | .min, ⟨b :: a :: d, m, r⟩ => .ok ⟨(if Cond.eval .slt a b then a else b) :: d, m, r⟩ |
| | .max, ⟨b :: a :: d, m, r⟩ => .ok ⟨(if Cond.eval .sgt a b then a else b) :: d, m, r⟩ |
| | .umStar, ⟨b :: a :: d, m, r⟩ => |
| .ok ⟨BitVec.ofNat n (a.toNat * b.toNat / 2 ^ n) :: BitVec.ofNat n (a.toNat * b.toNat) :: d, m, r⟩ |
| | .umDivMod, ⟨u :: hi :: lo :: d, m, r⟩ => |
| if hi.toNat < u.toNat then |
| .ok ⟨BitVec.ofNat n ((hi.toNat * 2 ^ n + lo.toNat) / u.toNat) :: |
| BitVec.ofNat n ((hi.toNat * 2 ^ n + lo.toNat) % u.toNat) :: d, m, r⟩ |
| else .error .divideByZero |
| | .mStar, ⟨b :: a :: d, m, r⟩ => |
| .ok ⟨BitVec.ofInt n (a.toInt * b.toInt / (2 ^ n : Nat)) :: BitVec.ofInt n (a.toInt * b.toInt) :: d, |
| m, r⟩ |
| | .smRem, ⟨v :: hi :: lo :: d, m, r⟩ => |
| if v.toInt ≠ 0 ∧ -(2 ^ (n - 1) : Int) ≤ (hi.toInt * 2 ^ n + lo.toNat).tdiv v.toInt ∧ |
| (hi.toInt * 2 ^ n + lo.toNat).tdiv v.toInt < 2 ^ (n - 1) then |
| .ok ⟨BitVec.ofInt n ((hi.toInt * 2 ^ n + lo.toNat).tdiv v.toInt) :: |
| BitVec.ofInt n ((hi.toInt * 2 ^ n + lo.toNat).tmod v.toInt) :: d, m, r⟩ |
| else .error .divideByZero |
| | .fmMod, ⟨v :: hi :: lo :: d, m, r⟩ => |
| if v.toInt ≠ 0 ∧ -(2 ^ (n - 1) : Int) ≤ (hi.toInt * 2 ^ n + lo.toNat).fdiv v.toInt ∧ |
| (hi.toInt * 2 ^ n + lo.toNat).fdiv v.toInt < 2 ^ (n - 1) then |
| .ok ⟨BitVec.ofInt n ((hi.toInt * 2 ^ n + lo.toNat).fdiv v.toInt) :: |
| BitVec.ofInt n ((hi.toInt * 2 ^ n + lo.toNat).fmod v.toInt) :: d, m, r⟩ |
| else .error .divideByZero |
| | .starSlashMod, ⟨c :: b :: a :: d, m, r⟩ => |
| if c.toInt ≠ 0 ∧ -(2 ^ (n - 1) : Int) ≤ (a.toInt * b.toInt).tdiv c.toInt ∧ |
| (a.toInt * b.toInt).tdiv c.toInt < 2 ^ (n - 1) then |
| .ok ⟨BitVec.ofInt n ((a.toInt * b.toInt).tdiv c.toInt) :: |
| BitVec.ofInt n ((a.toInt * b.toInt).tmod c.toInt) :: d, m, r⟩ |
| else .error .divideByZero |
| | .starSlash, ⟨c :: b :: a :: d, m, r⟩ => |
| if c.toInt ≠ 0 ∧ -(2 ^ (n - 1) : Int) ≤ (a.toInt * b.toInt).tdiv c.toInt ∧ |
| (a.toInt * b.toInt).tdiv c.toInt < 2 ^ (n - 1) then |
| .ok ⟨BitVec.ofInt n ((a.toInt * b.toInt).tdiv c.toInt) :: d, m, r⟩ |
| else .error .divideByZero |
| | .tor, ⟨a :: d, m, r⟩ => .ok ⟨d, m, a :: r⟩ |
| | .fromr, ⟨d, m, a :: r⟩ => .ok ⟨a :: d, m, r⟩ |
| | .fromr, ⟨_, _, []⟩ => .error .returnUnderflow |
| | .rfetch, ⟨d, m, a :: r⟩ => .ok ⟨a :: d, m, a :: r⟩ |
| | .rfetch, ⟨_, _, []⟩ => .error .returnUnderflow |
| | .loopI, ⟨d, m, a :: r⟩ => .ok ⟨a :: d, m, a :: r⟩ |
| | .loopI, ⟨_, _, []⟩ => .error .returnUnderflow |
| | .loopJ, ⟨d, m, a :: b :: c :: r⟩ => .ok ⟨c :: d, m, a :: b :: c :: r⟩ |
| | .loopJ, _ => .error .returnUnderflow |
| | .unloop, ⟨d, m, _ :: _ :: r⟩ => .ok ⟨d, m, r⟩ |
| | .unloop, _ => .error .returnUnderflow |
| | _, _ => .error .stackUnderflow |
|
|
| /-- The operations whose code is a loop rather than straight-line code. -/ |
| def loopy : Op → Bool |
| | .umStar | .umDivMod | .mStar | .smRem | .starSlashMod | .starSlash | .fmMod => true |
| | _ => false |
|
|
| end Op |
|
|
| /-- A Forth block. `ite t e rest` is `IF t ELSE e THEN rest`; `untilL body rest` is |
| `BEGIN body UNTIL rest`; `call i rest` executes the colon definition with index `i` in the |
| dictionary, then `rest`; `exit rest` is `EXIT`, which leaves the current word (`rest` is dead |
| code, kept so that a block records its source text) |
| `DO body LOOP rest`; `plusLoop body rest` is `DO body +LOOP rest`; `leave rest` is `LEAVE` |
| (`rest` is dead code too) |
| inductive Block where |
| | nil |
| | op (o : Op) (rest : Block) |
| | ite (t e rest : Block) |
| | untilL (body rest : Block) |
| | call (i : Nat) (rest : Block) |
| | exit (rest : Block) |
| | doLoop (body rest : Block) |
| | plusLoop (body rest : Block) |
| | leave (rest : Block) |
| | whileL (cond body rest : Block) |
| deriving DecidableEq, Repr |
|
|
| /-- A Forth program: a dictionary of colon definitions (word `i` is `defs[i]`), the main |
| block, and the number of `VARIABLE` cells (memory cells `0 … vars - 1`). Definitions may call |
| themselves and each other. -/ |
| structure Program where |
| defs : List Block |
| main : Block |
| vars : Nat := 0 |
| deriving DecidableEq, Repr |
|
|
| /-- The memory a program may assume: every variable cell is valid. -/ |
| def Program.MemOk {n : Nat} (P : Program) (mem : Memory n) : Prop := |
| ∀ a, a < P.vars → mem.valid (BitVec.ofNat n a) = true |
|
|
| /-- How a run of a block ends: it fell off the end (`ok`), it executed `EXIT` (`exit`), it |
| executed `LEAVE` (`leave`, with the loop parameters already removed), or it trapped (`error`). -/ |
| inductive Res (n : Nat) where |
| | ok (st : FState n) |
| | exit (st : FState n) |
| | leave (st : FState n) |
| | error (t : Trap) |
|
|
| namespace Res |
|
|
| def isOk {n : Nat} : Res n → Bool |
| | .ok _ => true |
| | _ => false |
|
|
| /-- `EXIT` or a trap: the results a loop does not catch (it catches `LEAVE`). -/ |
| def isStop {n : Nat} : Res n → Bool |
| | .exit _ => true |
| | .error _ => true |
| | _ => false |
|
|
| /-- The state a called word returns with: after falling off its end, after `EXIT`, or after a |
| `LEAVE` outside any loop of the word. -/ |
| def returned {n : Nat} : Res n → Option (FState n) |
| | .ok st => some st |
| | .exit st => some st |
| | .leave st => some st |
| | .error _ => none |
|
|
| end Res |
|
|
| /-- The `+LOOP` exit test, on the index `i`, limit `l` and step `k`: with `o = i - l`, the sign of |
| `((k + o) xor o) and (o xor k)`, i.e. `o + k` and `o` differ in sign while `o` and `k` differ in |
| sign too. This is the signed overflow of `(o - 2^(n-1)) + k`, i.e. ANS Forth's rule that the loop |
| ends when the index crosses the boundary between `l - 1` and `l` |
| (`Forth.loopCrossed_eq_saddOverflow`) |
| (`Forth.loopCrossed_one`). -/ |
| def loopCrossed {n : Nat} (i l k : Word n) : Bool := |
| Cond.eval .slt (((k + (i - l)) ^^^ (i - l)) &&& ((i - l) ^^^ k)) 0#n |
|
|
| /-- Big-step semantics. `Run defs b st r` says running `b` from `st`, with dictionary `defs`, |
| produces result `r`. Non-terminating runs (including unbounded recursion) have no derivation. |
|
|
| An abrupt result (`exit` or `error`, i.e. `isOk = false`) of a sub-block ends the enclosing |
| block with the same result. A call continues after the callee returns, whether the callee fell |
| off its end or executed `EXIT`; an `EXIT` thus never propagates out of a call. |
|
|
| Calling an index outside the dictionary is an explicit error, `badPc`: it is the trap the |
| lowered code raises, since such a call targets the address just past the program. The parser |
| never produces such a call. -/ |
| inductive Run {n : Nat} (defs : List Block) : Block → FState n → Res n → Prop where |
| | nil {st} : Run defs .nil st (.ok st) |
| | exit {rest st} : Run defs (.exit rest) st (.exit st) |
| | opOk {o rest st st' r} : |
| o.sem st = .ok st' → Run defs rest st' r → Run defs (.op o rest) st r |
| | opErr {o rest st t} : |
| o.sem st = .error t → Run defs (.op o rest) st (.error t) |
| | iteUnder {t e rest m rs} : |
| Run defs (.ite t e rest) ⟨[], m, rs⟩ (.error .stackUnderflow) |
| | iteTrue {t e rest c d m rs st1 r} : |
| Word.isTrue c = true → Run defs t ⟨d, m, rs⟩ (.ok st1) → Run defs rest st1 r → |
| Run defs (.ite t e rest) ⟨c :: d, m, rs⟩ r |
| | iteTrueStop {t e rest c d m rs r} : |
| Word.isTrue c = true → Run defs t ⟨d, m, rs⟩ r → r.isOk = false → |
| Run defs (.ite t e rest) ⟨c :: d, m, rs⟩ r |
| | iteFalse {t e rest c d m rs st1 r} : |
| Word.isTrue c = false → Run defs e ⟨d, m, rs⟩ (.ok st1) → Run defs rest st1 r → |
| Run defs (.ite t e rest) ⟨c :: d, m, rs⟩ r |
| | iteFalseStop {t e rest c d m rs r} : |
| Word.isTrue c = false → Run defs e ⟨d, m, rs⟩ r → r.isOk = false → |
| Run defs (.ite t e rest) ⟨c :: d, m, rs⟩ r |
| | untilBodyStop {body rest st r} : |
| Run defs body st r → r.isOk = false → Run defs (.untilL body rest) st r |
| | untilUnder {body rest st m rs} : |
| Run defs body st (.ok ⟨[], m, rs⟩) → Run defs (.untilL body rest) st (.error .stackUnderflow) |
| | untilDone {body rest st c d m rs r} : |
| Run defs body st (.ok ⟨c :: d, m, rs⟩) → Word.isTrue c = true → Run defs rest ⟨d, m, rs⟩ r → |
| Run defs (.untilL body rest) st r |
| | untilAgain {body rest st c d m rs r} : |
| Run defs body st (.ok ⟨c :: d, m, rs⟩) → Word.isTrue c = false → |
| Run defs (.untilL body rest) ⟨d, m, rs⟩ r → Run defs (.untilL body rest) st r |
| | whileCondStop {cond body rest st r} : |
| Run defs cond st r → r.isOk = false → Run defs (.whileL cond body rest) st r |
| | whileUnder {cond body rest st m rs} : |
| Run defs cond st (.ok ⟨[], m, rs⟩) → |
| Run defs (.whileL cond body rest) st (.error .stackUnderflow) |
| | whileExit {cond body rest st c d m rs r} : |
| Run defs cond st (.ok ⟨c :: d, m, rs⟩) → Word.isTrue c = false → |
| Run defs rest ⟨d, m, rs⟩ r → Run defs (.whileL cond body rest) st r |
| | whileBodyStop {cond body rest st c d m rs r} : |
| Run defs cond st (.ok ⟨c :: d, m, rs⟩) → Word.isTrue c = true → |
| Run defs body ⟨d, m, rs⟩ r → r.isOk = false → Run defs (.whileL cond body rest) st r |
| | whileAgain {cond body rest st c d m rs st2 r} : |
| Run defs cond st (.ok ⟨c :: d, m, rs⟩) → Word.isTrue c = true → |
| Run defs body ⟨d, m, rs⟩ (.ok st2) → Run defs (.whileL cond body rest) st2 r → |
| Run defs (.whileL cond body rest) st r |
| | callOk {i rest st body r1 st1 r} : |
| defs[i]? = some body → Run defs body st r1 → r1.returned = some st1 → |
| Run defs rest st1 r → Run defs (.call i rest) st r |
| | callErr {i rest st body x} : |
| defs[i]? = some body → Run defs body st (.error x) → Run defs (.call i rest) st (.error x) |
| | callUndef {i rest st} : |
| defs[i]? = none → Run defs (.call i rest) st (.error .badPc) |
| | leaveOk {rest d m a b rs} : |
| Run defs (.leave rest) ⟨d, m, a :: b :: rs⟩ (.leave ⟨d, m, rs⟩) |
| | leaveUnder {rest st} : |
| st.rstack.length < 2 → Run defs (.leave rest) st (.error .returnUnderflow) |
| | doUnder {body rest st} : |
| st.stack.length < 2 → Run defs (.doLoop body rest) st (.error .stackUnderflow) |
| | doBodyStop {body rest i l d m rs r} : |
| Run defs body ⟨d, m, i :: l :: rs⟩ r → r.isStop = true → |
| Run defs (.doLoop body rest) ⟨i :: l :: d, m, rs⟩ r |
| | doLeave {body rest i l d m rs st1 r} : |
| Run defs body ⟨d, m, i :: l :: rs⟩ (.leave st1) → Run defs rest st1 r → |
| Run defs (.doLoop body rest) ⟨i :: l :: d, m, rs⟩ r |
| | doTestUnder {body rest i l d m rs st1} : |
| Run defs body ⟨d, m, i :: l :: rs⟩ (.ok st1) → st1.rstack.length < 2 → |
| Run defs (.doLoop body rest) ⟨i :: l :: d, m, rs⟩ (.error .returnUnderflow) |
| | doDone {body rest i l d m rs i1 l1 d1 m1 rs1 r} : |
| Run defs body ⟨d, m, i :: l :: rs⟩ (.ok ⟨d1, m1, i1 :: l1 :: rs1⟩) → i1 + 1#n = l1 → |
| Run defs rest ⟨d1, m1, rs1⟩ r → Run defs (.doLoop body rest) ⟨i :: l :: d, m, rs⟩ r |
| | doAgain {body rest i l d m rs i1 l1 d1 m1 rs1 r} : |
| Run defs body ⟨d, m, i :: l :: rs⟩ (.ok ⟨d1, m1, i1 :: l1 :: rs1⟩) → i1 + 1#n ≠ l1 → |
| Run defs (.doLoop body rest) ⟨(i1 + 1#n) :: l1 :: d1, m1, rs1⟩ r → |
| Run defs (.doLoop body rest) ⟨i :: l :: d, m, rs⟩ r |
| | plusUnder {body rest st} : |
| st.stack.length < 2 → Run defs (.plusLoop body rest) st (.error .stackUnderflow) |
| | plusBodyStop {body rest i l d m rs r} : |
| Run defs body ⟨d, m, i :: l :: rs⟩ r → r.isStop = true → |
| Run defs (.plusLoop body rest) ⟨i :: l :: d, m, rs⟩ r |
| | plusLeave {body rest i l d m rs st1 r} : |
| Run defs body ⟨d, m, i :: l :: rs⟩ (.leave st1) → Run defs rest st1 r → |
| Run defs (.plusLoop body rest) ⟨i :: l :: d, m, rs⟩ r |
| | plusTestUnder {body rest i l d m rs st1} : |
| Run defs body ⟨d, m, i :: l :: rs⟩ (.ok st1) → st1.rstack.length < 2 → |
| Run defs (.plusLoop body rest) ⟨i :: l :: d, m, rs⟩ (.error .returnUnderflow) |
| | plusStepUnder {body rest i l d m rs i1 l1 m1 rs1} : |
| Run defs body ⟨d, m, i :: l :: rs⟩ (.ok ⟨[], m1, i1 :: l1 :: rs1⟩) → |
| Run defs (.plusLoop body rest) ⟨i :: l :: d, m, rs⟩ (.error .stackUnderflow) |
| | plusDone {body rest i l d m rs i1 l1 k d1 m1 rs1 r} : |
| Run defs body ⟨d, m, i :: l :: rs⟩ (.ok ⟨k :: d1, m1, i1 :: l1 :: rs1⟩) → |
| loopCrossed i1 l1 k = true → |
| Run defs rest ⟨d1, m1, rs1⟩ r → Run defs (.plusLoop body rest) ⟨i :: l :: d, m, rs⟩ r |
| | plusAgain {body rest i l d m rs i1 l1 k d1 m1 rs1 r} : |
| Run defs body ⟨d, m, i :: l :: rs⟩ (.ok ⟨k :: d1, m1, i1 :: l1 :: rs1⟩) → |
| loopCrossed i1 l1 k = false → |
| Run defs (.plusLoop body rest) ⟨(i1 + k) :: l1 :: d1, m1, rs1⟩ r → |
| Run defs (.plusLoop body rest) ⟨i :: l :: d, m, rs⟩ r |
|
|
| /-- The run relation is functional: a block and a state determine the result. -/ |
| theorem Run.deterministic {n : Nat} {defs : List Block} {b : Block} {st : FState n} |
| {r₁ r₂ : Res n} |
| (h₁ : Run defs b st r₁) (h₂ : Run defs b st r₂) : r₁ = r₂ := by |
| induction h₁ generalizing r₂ with |
| | nil => cases h₂ |
| | exit => cases h₂ |
| | opOk hs _ ih => |
| cases h₂ with |
| | opOk hs' h' => rw [hs] at hs' |
| | opErr hs' => rw [hs] at hs' |
| | opErr hs => |
| cases h₂ with |
| | opOk hs' _ => rw [hs] at hs' |
| | opErr hs' => rw [hs] at hs' |
| | iteUnder => cases h₂ < |
| | iteTrue hc ht hr iht ihr => |
| cases h₂ with |
| | iteTrue _ ht' hr' => |
| have := iht ht' |
| | iteTrueStop _ ht' hk => have := iht ht' |
| | iteFalse hc' => rw [hc] at hc' |
| | iteFalseStop hc' => rw [hc] at hc' |
| | iteTrueStop hc ht hk iht => |
| cases h₂ with |
| | iteTrue _ ht' _ => have := iht ht' |
| | iteTrueStop _ ht' => exact iht ht' |
| | iteFalse hc' => rw [hc] at hc' |
| | iteFalseStop hc' => rw [hc] at hc' |
| | iteFalse hc he hr ihe ihr => |
| cases h₂ with |
| | iteTrue hc' => rw [hc] at hc' |
| | iteTrueStop hc' => rw [hc] at hc' |
| | iteFalse _ he' hr' => |
| have := ihe he' |
| | iteFalseStop _ he' hk => have := ihe he' |
| | iteFalseStop hc he hk ihe => |
| cases h₂ with |
| | iteTrue hc' => rw [hc] at hc' |
| | iteTrueStop hc' => rw [hc] at hc' |
| | iteFalse _ he' _ => have := ihe he' |
| | iteFalseStop _ he' => exact ihe he' |
| | untilBodyStop hb hk ihb => |
| cases h₂ with |
| | untilBodyStop hb' => exact ihb hb' |
| | untilUnder hb' => have := ihb hb' |
| | untilDone hb' => have := ihb hb' |
| | untilAgain hb' => have := ihb hb' |
| | untilUnder hb ihb => |
| cases h₂ with |
| | untilBodyStop hb' hk => have := ihb hb' |
| | untilUnder hb' => rfl |
| | untilDone hb' => have := ihb hb' |
| | untilAgain hb' => have := ihb hb' |
| | untilDone hb hc hr ihb ihr => |
| cases h₂ with |
| | untilBodyStop hb' hk => have := ihb hb' |
| | untilUnder hb' => have := ihb hb' |
| | untilDone hb' _ hr' => have := ihb hb' |
| | untilAgain hb' hc' _ => have := ihb hb' |
| | untilAgain hb hc hl ihb ihl => |
| cases h₂ with |
| | untilBodyStop hb' hk => have := ihb hb' |
| | untilUnder hb' => have := ihb hb' |
| | untilDone hb' hc' _ => have := ihb hb' |
| | untilAgain hb' _ hl' => have := ihb hb' |
| | whileCondStop hc hk ihc => |
| cases h₂ with |
| | whileCondStop hc' => exact ihc hc' |
| | whileUnder hc' => have := ihc hc' |
| | whileExit hc' => have := ihc hc' |
| | whileBodyStop hc' => have := ihc hc' |
| | whileAgain hc' => have := ihc hc' |
| | whileUnder hc ihc => |
| cases h₂ with |
| | whileCondStop hc' hk => have := ihc hc' |
| | whileUnder => rfl |
| | whileExit hc' => have := ihc hc' |
| | whileBodyStop hc' => have := ihc hc' |
| | whileAgain hc' => have := ihc hc' |
| | whileExit hc hf hr ihc ihr => |
| cases h₂ with |
| | whileCondStop hc' hk => have := ihc hc' |
| | whileUnder hc' => have := ihc hc' |
| | whileExit hc' _ hr' => have := ihc hc' |
| | whileBodyStop hc' ht => have := ihc hc' |
| | whileAgain hc' ht => have := ihc hc' |
| | whileBodyStop hc ht hb hk ihc ihb => |
| cases h₂ with |
| | whileCondStop hc' hk' => have := ihc hc' |
| | whileUnder hc' => have := ihc hc' |
| | whileExit hc' hf => have := ihc hc' |
| | whileBodyStop hc' _ hb' => have := ihc hc' |
| | whileAgain hc' _ hb' => have := ihc hc' |
| | whileAgain hc ht hb hl ihc ihb ihl => |
| cases h₂ with |
| | whileCondStop hc' hk' => have := ihc hc' |
| | whileUnder hc' => have := ihc hc' |
| | whileExit hc' hf => have := ihc hc' |
| | whileBodyStop hc' _ hb' hk => have := ihc hc' |
| | whileAgain hc' _ hb' hl' => have := ihc hc' |
| | callOk hd hb hret hr ihb ihr => |
| cases h₂ with |
| | callOk hd' hb' hret' hr' => |
| rw [hd] at hd' |
| rw [hret] at hret' |
| | callErr hd' hb' => |
| rw [hd] at hd' |
| | callUndef hd' => rw [hd] at hd' |
| | callErr hd hb ihb => |
| cases h₂ with |
| | callOk hd' hb' hret' => |
| rw [hd] at hd' |
| | callErr hd' hb' => rw [hd] at hd' |
| | callUndef hd' => rw [hd] at hd' |
| | callUndef hd => |
| cases h₂ with |
| | callOk hd' => rw [hd] at hd' |
| | callErr hd' => rw [hd] at hd' |
| | callUndef => rfl |
| | leaveOk => cases h₂ with |
| | leaveOk => rfl |
| | leaveUnder hl => (simp at hl |
| | leaveUnder hl => cases h₂ with |
| | leaveOk => (simp at hl |
| | leaveUnder => rfl |
| | doUnder hl => |
| cases h₂ with |
| | doUnder => rfl |
| | _ => (simp at hl |
| | doBodyStop hb hk ihb => |
| cases h₂ with |
| | doUnder hl => (simp at hl |
| | doBodyStop hb' => exact ihb hb' |
| | doLeave hb' => have := ihb hb' |
| | doTestUnder hb' => have := ihb hb' |
| | doDone hb' => have := ihb hb' |
| | doAgain hb' => have := ihb hb' |
| | doLeave hb hr ihb ihr => |
| cases h₂ with |
| | doUnder hl => (simp at hl |
| | doBodyStop hb' hk => have := ihb hb' |
| | doLeave hb' hr' => have := ihb hb' |
| | doTestUnder hb' => have := ihb hb' |
| | doDone hb' => have := ihb hb' |
| | doAgain hb' => have := ihb hb' |
| | doTestUnder hb hl ihb => |
| cases h₂ with |
| | doUnder hl' => (simp at hl' |
| | doBodyStop hb' hk => have := ihb hb' |
| | doLeave hb' => have := ihb hb' |
| | doTestUnder => rfl |
| | doDone hb' => have := ihb hb' |
| | doAgain hb' => have := ihb hb' |
| | doDone hb he hr ihb ihr => |
| cases h₂ with |
| | doUnder hl => (simp at hl |
| | doBodyStop hb' hk => have := ihb hb' |
| | doLeave hb' => have := ihb hb' |
| | doTestUnder hb' hl => have := ihb hb' |
| | doDone hb' _ hr' => have := ihb hb' |
| | doAgain hb' hne _ => have := ihb hb' |
| | doAgain hb hne hl ihb ihl => |
| cases h₂ with |
| | doUnder hl' => (simp at hl' |
| | doBodyStop hb' hk => have := ihb hb' |
| | doLeave hb' => have := ihb hb' |
| | doTestUnder hb' hl' => have := ihb hb' |
| | doDone hb' he _ => have := ihb hb' |
| | doAgain hb' _ hl' => have := ihb hb' |
| | plusUnder hl => |
| cases h₂ with |
| | plusUnder => rfl |
| | _ => (simp at hl |
| | plusBodyStop hb hk ihb => |
| cases h₂ with |
| | plusUnder hl => (simp at hl |
| | plusBodyStop hb' => exact ihb hb' |
| | plusLeave hb' => have := ihb hb' |
| | plusTestUnder hb' => have := ihb hb' |
| | plusStepUnder hb' => have := ihb hb' |
| | plusDone hb' => have := ihb hb' |
| | plusAgain hb' => have := ihb hb' |
| | plusLeave hb hr ihb ihr => |
| cases h₂ with |
| | plusUnder hl => (simp at hl |
| | plusBodyStop hb' hk => have := ihb hb' |
| | plusLeave hb' hr' => have := ihb hb' |
| | plusTestUnder hb' => have := ihb hb' |
| | plusStepUnder hb' => have := ihb hb' |
| | plusDone hb' => have := ihb hb' |
| | plusAgain hb' => have := ihb hb' |
| | plusTestUnder hb hl ihb => |
| cases h₂ with |
| | plusUnder hl' => (simp at hl' |
| | plusBodyStop hb' hk => have := ihb hb' |
| | plusLeave hb' => have := ihb hb' |
| | plusTestUnder => rfl |
| | plusStepUnder hb' => have := ihb hb' |
| | plusDone hb' => have := ihb hb' |
| | plusAgain hb' => have := ihb hb' |
| | plusStepUnder hb ihb => |
| cases h₂ with |
| | plusUnder hl' => (simp at hl' |
| | plusBodyStop hb' hk => have := ihb hb' |
| | plusLeave hb' => have := ihb hb' |
| | plusTestUnder hb' hl => have := ihb hb' |
| | plusStepUnder => rfl |
| | plusDone hb' => have := ihb hb' |
| | plusAgain hb' => have := ihb hb' |
| | plusDone hb he hr ihb ihr => |
| cases h₂ with |
| | plusUnder hl => (simp at hl |
| | plusBodyStop hb' hk => have := ihb hb' |
| | plusLeave hb' => have := ihb hb' |
| | plusTestUnder hb' hl => have := ihb hb' |
| | plusStepUnder hb' => have := ihb hb' |
| | plusDone hb' _ hr' => have := ihb hb' |
| | plusAgain hb' hne _ => have := ihb hb' |
| | plusAgain hb hne hl ihb ihl => |
| cases h₂ with |
| | plusUnder hl' => (simp at hl' |
| | plusBodyStop hb' hk => have := ihb hb' |
| | plusLeave hb' => have := ihb hb' |
| | plusTestUnder hb' hl' => have := ihb hb' |
| | plusStepUnder hb' => have := ihb hb' |
| | plusDone hb' he _ => have := ihb hb' |
| | plusAgain hb' _ hl' => have := ihb hb' |
|
|
| end Forth |
| end WordDialect |
|
|
