From a8d2679287c9ea856ac7ca9eba7d7edb62b2336b Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Fri, 22 Nov 2024 02:50:18 +0100 Subject: [PATCH] fix CI --- .github/workflows/build.yml | 5 +- examples/hello_mmc.mm0 | 7 + examples/join/hello_mmc.mm0 | 2490 +++++++++++++++++++++++++++++++++++ 3 files changed, 2501 insertions(+), 1 deletion(-) create mode 100644 examples/hello_mmc.mm0 create mode 100644 examples/join/hello_mmc.mm0 diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 72ffa364..fc331fdf 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -131,12 +131,15 @@ jobs: working-directory: examples # run: mm0-c compiler.mmb < x86_join.mm0 run: mm0-c compiler.mmb < compiler_join.mm0 + - name: hello_mmc_join.mm0 + working-directory: examples + run: mm0-rs join hello_mmc.mm0 | tee hello_mmc_join.mm0 - name: hello_mmc.mm1 working-directory: examples run: mm0-rs compile -W hello_mmc.mm1 hello_mmc.mmb - name: hello_mmc.mmb working-directory: examples - run: mm0-c hello_mmc.mmb < compiler_join.mm0 + run: mm0-c hello_mmc.mmb < hello_mmc_join.mm0 - name: hol.mm1 working-directory: examples run: mm0-rs compile -W hol.mm1 hol.mmb diff --git a/examples/hello_mmc.mm0 b/examples/hello_mmc.mm0 new file mode 100644 index 00000000..3a220c9e --- /dev/null +++ b/examples/hello_mmc.mm0 @@ -0,0 +1,7 @@ +import "compiler.mm0"; + +def test: string; + +theorem test_isBasicElf: $ isBasicElf test $; +theorem test_ok {k vs x: nat}: + $ A. k (initialConfig test k -> terminates_ensuring k (S\ vs, S\ x, sn 0)) $; diff --git a/examples/join/hello_mmc.mm0 b/examples/join/hello_mmc.mm0 new file mode 100644 index 00000000..053ed115 --- /dev/null +++ b/examples/join/hello_mmc.mm0 @@ -0,0 +1,2490 @@ +-- This is an autogenerated file constructed by `mm0-rs join hello_mmc.mm0`. +-- It concatenates the files: +-- * peano.mm0 +-- * peano_hex.mm0 +-- * x86.mm0 +-- * compiler.mm0 +-- * hello_mmc.mm0 + +--------------- +-- peano.mm0 -- +--------------- +delimiter $ ( { ~ $ $ } ) , $; +--| Well formed formulas, or propositions - true or false. +strict provable sort wff; +--| Implication: if p, then q. +term im (p q: wff): wff; infixr im: $->$ prec 25; +--| Negation: p is false. +term not (p: wff): wff; prefix not: $~$ prec 41; + +--| Axiom 1 of Lukasiewicz' axioms for classical propositional logic. +axiom ax_1 (a b: wff): $ a -> b -> a $; +--| Axiom 2 of Lukasiewicz' axioms for classical propositional logic. +axiom ax_2 (a b c: wff): $ (a -> b -> c) -> (a -> b) -> a -> c $; +--| Axiom 3 of Lukasiewicz' axioms for classical propositional logic. +axiom ax_3 (a b: wff): $ (~a -> ~b) -> b -> a $; +--| Modus ponens: from `a -> b` and `a`, infer `b`. +axiom ax_mp (a b: wff): $ a -> b $ > $ a $ > $ b $; + +--| Conjunction: `a` and `b` are both true. +def an (a b: wff): wff = $ ~(a -> ~b) $; +infixl an: $/\$ prec 34; + +--| If and only if: `a` implies `b`, and `b` implies `a`. +def iff (a b: wff): wff = $ (a -> b) /\ (b -> a) $; +infixl iff: $<->$ prec 20; + +--| Disjunction: either `a` is true or `b` is true. +def or (a b: wff): wff = $ ~a -> b $; +infixl or: $\/$ prec 30; + +--| Selection: `ifp p a b` is equivalent to `a` if `p` is true, +--| and equivalent to `b` if `p` is false. +def ifp (p a b: wff): wff; +theorem ifppos (p a b: wff): $ p -> (ifp p a b <-> a) $; +theorem ifpneg (p a b: wff): $ ~p -> (ifp p a b <-> b) $; + +--| The constant `true`. +term tru: wff; prefix tru: $T.$ prec max; +--| `true` is true. +axiom itru: $ T. $; +--| The constant `false`. +def fal: wff = $ ~T. $; prefix fal: $F.$ prec max; + +--| The sort of natural numbers, or nonnegative integers. +--| In Peano Arithmetic this is the domain of discourse, +--| the basic sort over which quantifiers range. +sort nat; + +--| The for-all quantifier. `A. x p` means +--| "for all natural numbers `x`, `p` holds", +--| where `(p: wff x)` in the declaration indicates that `p` may contain +--| free occurrences of variable `x` that are bound by this quantifier. +term al {x: nat} (p: wff x): wff; prefix al: $A.$ prec 41; + +--| The exists quantifier. `E. x p` means +--| "there is a natural number `x`, such that `p` holds", +--| where `(p: wff x)` in the declaration indicates that `p` may contain +--| free occurrences of variable `x` that are bound by this quantifier. +def ex {x: nat} (p: wff x): wff = $ ~(A. x ~p) $; +prefix ex: $E.$ prec 41; + +--| Equality of natural numbers: `a = b` +--| means that `a` and `b` have the same value. +term eq (a b: nat): wff; infixl eq: $=$ prec 50; + +--| The axiom of generalization. If `|- p` is derivable +--| (the lack of a precondition means this is a proof in the empty context), +--| then `p` is universally true, so `|- A. x p` is also true. +axiom ax_gen {x: nat} (p: wff x): $ p $ > $ A. x p $; + +--| Axiom 4 for predicate logic: forall distributes over implication. +axiom ax_4 {x: nat} (p q: wff x): $ A. x (p -> q) -> A. x p -> A. x q $; + +--| Axiom 5 for predicate logic: If `p` does not contain an occurrence of `x` +--| (note that `(p: wff)` in contrast to `(p: wff x)` means that `p` cannot +--| depend on variable `x`), then `p` implies `A. x p` +--| because the quantifier is trivial. +axiom ax_5 {x: nat} (p: wff): $ p -> A. x p $; + +--| Axiom 6 for predicate logic: for any term `a` (which cannot depend on `x`), +--| there exists an `x` which is equal to `a`. +axiom ax_6 (a: nat) {x: nat}: $ E. x x = a $; + +--| Axiom 7 for predicate logic: equality satisfies the euclidean property +--| (which implies symmetry and transitivity, and reflexivity given axiom 6). +axiom ax_7 (a b c: nat): $ a = b -> a = c -> b = c $; + +-- axiom 9 has been proven redundant; axiom 8 is displaced below + +--| Axiom 10 for predicate logic: `x` is bound in `~(A. x p)`, so we can +--| safely introduce a `A. x` quantifier. (This axiom is used to internalize +--| the notion of "bound in" when axiom 5 does not apply.) +axiom ax_10 {x: nat} (p: wff x): $ ~(A. x p) -> A. x ~(A. x p) $; + +--| Axiom 11 for predicate logic: forall quantifiers commute. +axiom ax_11 {x y: nat} (p: wff x y): $ A. x A. y p -> A. y A. x p $; + +--| Axiom 12 for predicate logic: If `x` is some fixed `a` and `p(x)` holds, +--| then for all `x` which are equal to `a`, `p(x)` holds. This expresses the +--| substitution property of `=`, but the name shadowing on `x` allows us to +--| express this without changing `p`, +--| because we haven't defined proper substitution yet. +axiom ax_12 {x: nat} (a: nat) (p: wff x): $ x = a -> p -> A. x (x = a -> p) $; + +--| Not equal: `a != b` means `a` and `b` are distinct natural numbers. +def ne (a b: nat): wff = $ ~ a = b $; infixl ne: $!=$ prec 50; + +--| Proper substitution. `[a / x] p` is `p`, with free occurrences of `x` in +--| `p` replaced by `a`. If we write `p(x)`, this may also be denoted as `p(a)`. +--| (Note that this is only provably equivalent to `p(a)`; +--| `[0 / x] (x < x + y)` is equivalent but not syntactically identical to +--| `0 < 0 + y`, and it requires a rewriting/substitution proof to show.) +def sb (a: nat) {x .y: nat} (p: wff x): wff = +$ A. y (y = a -> A. x (x = y -> p)) $; +notation sb (a: nat) {x: nat} (p: wff x): wff = + ($[$:41) a ($/$:0) x ($]$:0) p; + +--| The sort of sets of natural numbers. Because we are working in +--| Peano Arithmetic, we cannot quantify over variables of this type, and these +--| should be thought of only as sugar for formulas with one free variable. +--| This is a conservative extension of PA. +strict sort set; + +--| A "class abstraction" `{x | p(x)}` is the set of natural numbers `x` such that `p(x)` holds. +term ab {x: nat} (p: wff x): set; +notation ab {x: nat} (p: wff x): set = (${$:max) x ($|$:0) p ($}$:0); + +--| Given a natural number `a` and a set `A`, `a e. A` (read `e.` as epsilon) +--| means `a` is in the set `A`. +term el (a: nat) (A: set): wff; infixl el: $e.$ prec 50; + +--| `a` is in `{x | p(x)}` iff `p(a)` holds. +axiom elab (a: nat) {x: nat} (p: wff x): $ a e. {x | p} <-> [ a / x ] p $; + +--| Elementhood respects equality. This is a theorem for most definitions +--| but has to be axiomatized for primitive term constructors like `e.` +--| This is Axiom 8 of predicate logic (which has an instance for every +--| primitive predicate in the language). +axiom ax_8 (a b: nat) (A: set): $ a = b -> a e. A -> b e. A $; + +--| `A == B` is equality for sets. Two sets are equal if they have the +--| same elements. +def eqs (A B: set) {.x: nat}: wff = $ A. x (x e. A <-> x e. B) $; +infixl eqs: $==$ prec 50; + +--| `A C_ B` means `A` is a subset of `B`. +def subset (A B: set) (.x: nat): wff = $ A. x (x e. A -> x e. B) $; +infixl subset: $C_$ prec 50; + +--| `A i^i B` is the intersection of sets `A` and `B`. +def Inter (A B: set) (.x: nat): set = $ {x | x e. A /\ x e. B} $; +infixl Inter: $i^i$ prec 70; + +--| `A u. B` is the union of sets `A` and `B`. +def Union (A B: set) (.x: nat): set = $ {x | x e. A \/ x e. B} $; +infixl Union: $u.$ prec 65; + +--| `Compl A` is the complement of `A`, the set of all natural numbers not in `A`. +def Compl (A: set) (.x: nat): set = $ {x | ~x e. A} $; + +--| `Univ`, or `_V` is the set of all natural numbers. +def Univ (.x: nat): set = $ {x | T.} $; prefix Univ: $_V$ prec max; + +--| Substitution for sets. `S[a / x] A` is the set `A` when +--| free variable `x` is evaluated at `a`. +def sbs (a: nat) {x .y: nat} (A: set x): set = $ {y | [ a / x ] y e. A} $; +notation sbs (a: nat) {x: nat} (A: set x): set = ($S[$:99) a ($/$:0) x ($]$:0) A; + +--| `0` is a natural number. +term d0: nat; prefix d0: $0$ prec max; +--| The successor operation: `suc n` is a natural number when `n` is. +term suc (n: nat): nat; + +def d1: nat = $suc 0$; prefix d1: $1$ prec max; +def d2: nat = $suc 1$; prefix d2: $2$ prec max; +def d3: nat = $suc 2$; prefix d3: $3$ prec max; +def d4: nat = $suc 3$; prefix d4: $4$ prec max; +def d5: nat = $suc 4$; prefix d5: $5$ prec max; +def d6: nat = $suc 5$; prefix d6: $6$ prec max; +def d7: nat = $suc 6$; prefix d7: $7$ prec max; +def d8: nat = $suc 7$; prefix d8: $8$ prec max; +def d9: nat = $suc 8$; prefix d9: $9$ prec max; +def d10: nat = $suc 9$; prefix d10: $10$ prec max; + +--| Zero is not a successor. Axiom 1 of Peano Arithmetic. +axiom peano1 (a: nat): $ suc a != 0 $; +--| The successor function is injective. Axiom 2 of Peano Arithmetic. +axiom peano2 (a b: nat): $ suc a = suc b <-> a = b $; +--| The induction axiom of Peano Arithmetic. If `p(0)` is true, +--| and `p(x)` implies `p(suc x)` for all `x`, then `p(x)` is true for all `x`. +axiom peano5 {x: nat} (p: wff x): + $ [ 0 / x ] p -> A. x (p -> [ suc x / x ] p) -> A. x p $; + +--| The definite description operator: `the A` is the value `a` such that +--| `A = {a}`, if there is such a value, otherwise `0`. +term the (A: set): nat; +--| The positive case of definite description: `A = {a}` then `the A = a`. +axiom theid {x: nat} (A: set) (a: nat): $ A == {x | x = a} -> the A = a $; +--| The negative case of definite description: `A`` is not a singleton then `the A = 0`. +axiom the0 {x y: nat} (A: set): $ ~E. y A == {x | x = y} -> the A = 0 $; + +--| Substitution for numbers. If `b(x)` is an expression denoting a natural number, +--| with free `x`, then `N[a / x] b` is the term `b(a)`. +def sbn (a: nat) {x .y: nat} (b: nat x): nat = $ the {y | [ a / x ] y = b} $; +notation sbn (a: nat) {x: nat} (b: nat x): nat = ($N[$:99) a ($/$:0) x ($]$:0) b; + +--| Addition of natural numbers, a primitive term constructor in PA. +term add (a b: nat): nat; infixl add: $+$ prec 64; +--| Multiplication of natural numbers, a primitive term constructor in PA. +term mul (a b: nat): nat; infixl mul: $*$ prec 70; + +--| Addition respects equalty. +axiom addeq (a b c d: nat): $ a = b -> c = d -> a + c = b + d $; +--| Multiplication respects equalty. +axiom muleq (a b c d: nat): $ a = b -> c = d -> a * c = b * d $; +--| The base case in the definition of addition. +axiom add0 (a: nat): $ a + 0 = a $; +--| The successor case in the definition of addition. +axiom addS (a b: nat): $ a + suc b = suc (a + b) $; +--| The base case in the definition of multiplication. +axiom mul0 (a: nat): $ a * 0 = 0 $; +--| The successor case in the definition of multiplication. +axiom mulS (a b: nat): $ a * suc b = a * b + a $; + +---------------------------------------------------------------------- +-- Axioms end here! This completes the axiomatization of Peano Arithmetic, +-- although we will introduce more (conservative) axioms in `peano_hex.mm0`. +-- The rest is definitions needed for downstream files. +---------------------------------------------------------------------- + +--| (Truncated) subtraction of natural numbers. +--| Note that `a - b = 0` when `a < b`. +def sub (a b: nat) {.x: nat}: nat = $ the {x | b + x = a} $; +infixl sub: $-$ prec 64; + +--| `a <= b` means `a` is less than or equal to `b`. +def le (a b .x: nat): wff = $ E. x a + x = b $; +infixl le: $<=$ prec 50; + +--| `a < b` means `a` is strictly less than `b`. +def lt (a b: nat): wff = $ suc a <= b $; +infixl lt: $<$ prec 50; + +--| `finite A` means `A` is a finite set +--| (here defined as one that is upper bounded by some natural number). +def finite (A: set) (.n .x: nat): wff = $ E. n A. x (x e. A -> x < n) $; + +--| `if p a b` is the if-then-else construct: +--| if `p` is true then `a`, else `b`. +def if (p: wff) (a b: nat): nat; +theorem ifpos (p: wff) (a b: nat): $ p -> if p a b = a $; +theorem ifneg (p: wff) (a b: nat): $ ~p -> if p a b = b $; + +--| `true n` means `n` is "truthy", that is, nonzero. +def true (n: nat): wff = $ n != 0 $; +--| `bool n` means `n` is "boolean", that is, 0 or 1. +def bool (n: nat): wff = $ n < 2 $; +--| `nat p` turns wff `p` into a natural number: if `p` is true then `1`, else `0`. +def nat (p: wff): nat = $ if p 1 0 $; + +--| `min a b` is the smaller of `a` and `b`. +def min (a b: nat): nat = $ if (a < b) a b $; +--| `max a b` is the larger of `a` and `b`. +def max (a b: nat): nat = $ if (a < b) b a $; + +--| `a // b` is the quotient on dividing `a` by `b`. +--| (The double slash is used as in python to remind the reader that +--| this is a rounding-down division, not exact division.) +--| Division by 0 is defined and equal to 0. +def div (a b: nat): nat; infixl div: $//$ prec 70; + +--| `a % b` is the remainder on dividing `a` by `b`. +--| Modulus by 0 is defined and `a % 0 = a`. +def mod (a b: nat): nat; infixl mod: $%$ prec 70; + +theorem div0 (a: nat): $ a // 0 = 0 $; +theorem divmod (a b: nat): $ b * (a // b) + a % b = a $; +theorem modlt (a b: nat): $ b != 0 -> a % b < b $; + +--| `a || b` means that `a` divides `b`, or equivalently, +--| `b` is a multiple of `a`. +def dvd (a b .c: nat): wff = $ E. c c * a = b $; +infixl dvd: $||$ prec 50; + +--| `b0 n` is `n * 2`. +--| It is named for "bit 0" as in binary representation of numbers. +--| +--| `b0` is also used as left injection when creating disjoint unions. +def b0 (n: nat): nat = $ n + n $; +--| `b1 n` is `n * 2 + 1`. +--| It is named for "bit 1" as in binary representation of numbers. +--| +--| `b1` is also used as right injection when creating disjoint unions. +def b1 (n: nat): nat = $ suc (b0 n) $; +--| `odd n` means `n` is odd, not divisible by 2. +def odd (n: nat): wff = $ n % 2 = 1 $; + +--| `a, b` is the pairing operator on natural numbers +--| (or anything that is being encoded as a natural number). +--| It is defined using the Cantor pairing function. +--| It is right associative, i.e. `a, b, c` means `(a, (b, c))`. +def pr (a b: nat): nat = $ (a + b) * suc (a + b) // 2 + b $; +infixr pr: $,$ prec 55; +--| The first component of a pair. +def fst (a: nat): nat; +--| The second component of a pair. +def snd (a: nat): nat; + +theorem pr0: $ 0, 0 = 0 $; +theorem fstpr (a b: nat): $ fst (a, b) = a $; +theorem sndpr (a b: nat): $ snd (a, b) = b $; +theorem fstsnd (a: nat): $ fst a, snd a = a $; + +--| `pi11 ((a, b), c) = a` +def pi11 (n: nat): nat = $ fst (fst n) $; +--| `pi12 ((a, b), c) = b` +def pi12 (n: nat): nat = $ snd (fst n) $; +--| `pi21 (a, (b, c)) = b` +def pi21 (n: nat): nat = $ fst (snd n) $; +--| `pi22 (a, (b, c)) = c` +def pi22 (n: nat): nat = $ snd (snd n) $; +--| `pi221 (a, (b, (c, d))) = c` +def pi221 (n: nat): nat = $ fst (pi22 n) $; +--| `pi222 (a, (b, (c, d))) = d` +def pi222 (n: nat): nat = $ snd (pi22 n) $; + +--| `isfun A` means `A` is a function, +--| i.e. if `(x,y)` and `(x,z)` are in `A` then `y = z`. +def isfun (A: set) (.a .b .b2: nat): wff = +$ A. a A. b A. b2 (a, b e. A -> a, b2 e. A -> b = b2) $; + +--| `S\ x, A` is "lambda for relations": `a, b e. S\ x, A(x)` if `b e. A(a)`. +--| It can be iterated to produce n-ary relations. +--| `S\ x, S\ y, {z | p(x,y,z)}` is the set `S` such that +--| `x, y, z e. S` iff `p(x,y,z)`. +def sab {x .z: nat} (A: set x): set = $ {z | snd z e. S[ fst z / x ] A} $; +notation sab {x: nat} (A: set x): set = ($S\$:100) x ($,$:55) A; + +--| Indexed disjoint union, a restricted version of `S\`. +--| `a, b e. X\ x e. A, B(x)` iff `a e. A` and `b e. B(a)`. +def xab {x .z: nat} (A: set) (B: set x): set = +$ {z | fst z e. A /\ snd z e. S[ fst z / x ] B} $; +notation xab {x: nat} (A: set) (B: set x): set = + ($X\$:100) x ($e.$:50) A ($,$:55) B; + +--| `Xp A B` is the cartesian product of sets: +--| `(a,b) e. Xp A B` iff `a e. A` and `b e. B`. +def Xp (A B: set) (.x: nat): set = $ X\ x e. A, B $; + +--| The domain of a binary relation: +--| `x e. Dom A` if there exists `y` such that `(x,y) e. A`. +def Dom (A: set) (.x .y: nat): set = $ {x | E. y x, y e. A} $; +--| The range of a binary relation: +--| `y e. Ran A` if there exists `x` such that `(x,y) e. A`. +def Ran (A: set) (.x .y: nat): set = $ {y | E. x x, y e. A} $; + +--| The image of a relation under a set: `y e. F '' A` +--| if there exists `x e. A` such that `(x,y) e. F`. +def Im (F A: set) (.x .y: nat): set = $ {y | E. x (x e. A /\ x, y e. F)} $; +infixl Im: $''$ prec 80; + +--| The converse of a relation: `(x,y) e. cnv A` if `(y,x) e. A`. +def cnv (A: set) (.x .y: nat): set = $ S\ x, {y | y, x e. A} $; + +--| The relational composition: `(x,z) e. F o> G` if there exists `y` such that +--| `(x,y) e. F` and `(y,z) e. G`. *Warning*: This is also applicable for functions, +--| but it does not match the more conventional right-to-left composition order. +--| `(F o> G) @ x = G @ (F @ x)`. We use an arrow like notation +--| `o>` to remind the reader of this: we apply `F` *then* `G`. +def comp (F G: set) (.x .y .z: nat): set = +$ S\ x, {z | E. y (x, y e. F /\ y, z e. G)} $; +infixr comp: $o>$ prec 91; + +--| The restriction of a relation to a set: `A |` B` is +--| the set of `(x,y) e. A` such that `x e. B`. +def res (A B: set): set = $ A i^i Xp B _V $; +infixl res: $|`$ prec 54; + +--| The lambda operator: `\ x, v(x)` is the set of pairs `(x, v(x))` over +--| all natural numbers `x`. +def lam {x .p: nat} (a: nat x): set = $ {p | E. x p = x, a} $; +notation lam {x: nat} (a: nat x): set = ($\$:53) x ($,$:55) a; + +--| The application operator. If `F` is a function and `x` is a natural number then +--| `F @ x` is `F` evaluated at `x`. That is, it is the value `y` +--| for which `(x,y) e. F`, if there is a unique such number. +def app (F: set) (x .y: nat): nat = $ the {y | x, y e. F} $; +infixl app: $@$ prec 200; + +--| Define a function by cases on a disjoint union. +--| `case A B` is the function such that +--| * `case A B @ b0 n = A @ n` +--| * `case A B @ b1 n = B @ n` +def case (A B: set) (.n: nat): set = +$ \ n, if (odd n) (B @ (n // 2)) (A @ (n // 2)) $; +theorem casel (A B: set) (n: nat): $ case A B @ b0 n = A @ n $; +theorem caser (A B: set) (n: nat): $ case A B @ b1 n = B @ n $; + +--| Disjoint union of sets; also `case` for wff-valued functions. +--| * `b0 n e. Sum A B <-> n e. A` +--| * `b1 n e. Sum A B <-> n e. B` +def Sum (A B: set): set; +theorem Suml (A B: set) (n: nat): $ b0 n e. Sum A B <-> n e. A $; +theorem Sumr (A B: set) (n: nat): $ b1 n e. Sum A B <-> n e. B $; + +--| Simple recursion operator: +--| * `rec 0 = z` +--| * `rec (n+1) = S (rec n)` +def rec (z: nat) (S: set) (n: nat): nat; +theorem rec0 (z: nat) (S: set): $ rec z S 0 = z $; +theorem recS (z: nat) (S: set) (n: nat): + $ rec z S (suc n) = S @ rec z S n $; + +--| The "bind" operator for the option monad, +--| `obind : Option A -> (A -> Option B) -> Option B`. +--| * `obind none F = none` +--| * `obind (some a) F = F a` +def obind (a: nat) (F: set): nat; +theorem obind0 (F: set): $ obind 0 F = 0 $; +theorem obindS (n: nat) (F: set): $ obind (suc n) F = F @ n $; + +--| The power function on natural numbers. +--| * `a ^ 0 = 1` +--| * `a ^ suc b = a * a ^ b` +def pow (a b: nat): nat; infixr pow: $^$ prec 81; +theorem pow0 (a: nat): $ a ^ 0 = 1 $; +theorem powS (a b: nat): $ a ^ suc b = a * a ^ b $; + +--| Left shift for natural numbers: `shl a n = a * 2 ^ n`. +def shl (a n: nat): nat = $ a * 2 ^ n $; +--| Right shift for natural numbers: `shr a n = a // 2 ^ n`. +def shr (a n: nat): nat = $ a // 2 ^ n $; + +--| Lift a natural number to a set, via `a ~> {x | odd (shr a x)}`. +--| That is, `x e. a` if the `x`'th bit of `a` is 1. +--| This mapping is injective, and surjective onto finite sets, +--| so we can view the sort `nat` as a subtype of `set` +--| consisting of the finite sets. +def ns (a .x: nat): set = $ {x | odd (shr a x)} $; coercion ns: nat > set; +theorem axext (a b: nat): $ a == b -> a = b $; +theorem ellt (a b: nat): $ a e. b -> a < b $; +theorem nel0 (a: nat): $ ~ a e. 0 $; + +--| Convert a finite set to a natural number with the same elements. +--| We use this when we wish to construct a natural number +--| from a set expression. It returns a garbage value 0 if the set is not finite. +--| This is the inverse to the `ns` coercion. +def lower (A: set) (.n: nat): nat = $ the {n | n == A} $; +theorem eqlower (A: set): $ finite A <-> A == lower A $; + +--| A singleton set `{a}`, as a `nat` because it is always finite. +def sn (a: nat): nat; +theorem elsn (a b: nat): $ a e. sn b <-> a = b $; + +--| `ins a b` or `a ; b` is the set `{a} u. b`, the set containing `a` +--| and the elements of `b`. It is finite because `b` is. +def ins (a b: nat): nat; infixr ins: $;$ prec 85; +theorem elins (a b c: nat): $ a e. ins b c <-> a = b \/ a e. c $; + +--| `upto n = {x | x < n}` is the set of numbers less than `n`. +def upto (n: nat): nat = $ 2 ^ n - 1 $; +theorem elupto (k n: nat): $ k e. upto n <-> k < n $; + +--| `Bool = {x | bool x}` is the set of boolean values (0 and 1). +def Bool: nat = $ 0 ; sn 1 $; +--| `Option A` is the set `A` disjointly extended with an additional element. +--| We use `0` and `suc` in place of the `none` and `some` constructors. +def Option (A: set) (.n: nat): set = $ {n | n = 0 \/ n - 1 e. A} $; + +--| `Power A` is the set of all (finite) subsets of `A`. +def Power (A: set) (.x: nat): set = $ {x | x C_ A} $; +--| `power a` is the finite set of all subsets of the finite set `a`. +def power (a: nat): nat = $ lower (Power a) $; + +--| `sUnion A` is the set union: the union of all the elements of `A`. +def sUnion (A: set) (.x .y: nat): set = $ {x | E. y (x e. y /\ y e. A)} $; + +--| `cons a b`, or `a : b`, is the list cons operator: +--| `cons : A -> List A -> List A` +def cons (a b: nat): nat = $ suc (a, b) $; infixr cons: $:$ prec 91; + +--| `sep n {x | p(x)}` is `{x e. n | p(x)}`, +--| the set of elements of `n` such that `p(x)`. Because it is a subset of an +--| existing finite set `n`, it is also finite. +--| This is analogous to the separation axiom of ZFC. +def sep (n: nat) (A: set): nat; +theorem elsep (n: nat) (A: set) (a: nat): $ a e. sep n A <-> a e. n /\ a e. A $; + +--| `Arrow A B` (which has no notation but is denoted `A -> B` in comments) +--| is the set of all (finite) functions from `A` to `B`. +def Arrow (A B: set) (.f: nat): set = +$ {f | isfun f /\ Dom f == A /\ Ran f C_ B} $; + +--| `\. x e. a, v(x)` is the finite (restricted) lambda: the regular lambda `\ x, v(x)` +--| restricted to the finite set `a`. Since it is finite, we make it manifestly finite here. +def rlam {x: nat} (a: nat) (v: nat x): nat = $ lower ((\ x, v) |` a) $; +notation rlam {x: nat} (a: nat) (v: nat x): nat = ($\.$:53) x ($e.$:50) a ($,$:55) v; + +--| `write F a b`, sometimes denoted `F[a -> b]` is +--| the function which is `b` at `a` and returns `F @ x` for `x != a`. +def write (F: set) (a b .x .y: nat): set = +$ S\ x, {y | ifp (x = a) (y = b) (x, y e. F)} $; +theorem writeEq (F: set) (a b: nat): $ write F a b @ a = b $; +theorem writeNe (F: set) (a b x: nat): $ x != a -> write F a b @ x = F @ x $; + +--| Strong recursion operator: +--| * `srec n = S (srec 0, ..., srec (n-1))` +def srec (S: set) (n: nat): nat; +theorem srecval {i: nat} (S: set) (n: nat): + $ srec S n = S @ (\. i e. upto n, srec S i) $; + +--| Strong recursion operator (for wffs): +--| * `srecp n <-> (srecp 0, ..., srecp (n-1)) e. A` +def srecp (A: set) (n: nat): wff; +theorem srecpval {i: nat} (A: set) (n: nat): + $ srecp A n <-> n, sep (upto n) {i | srecp A i} e. A $; + +--| The cardinality (number of elements) of a finite set. +def card (s: nat): nat; +theorem card0: $ card 0 = 0 $; +theorem cardS (a s: nat): $ ~a e. s -> card (a ; s) = suc (card s) $; + +--| The list recursion operator: +--| * `lrec 0 = z` +--| * `lrec (a : l) = S (a, l, lrec l)` +def lrec (z: nat) (S: set) (n: nat): nat; +theorem lrec0 (z: nat) (S: set): $ lrec z S 0 = z $; +theorem lrecS (z: nat) (S: set) (a b: nat): + $ lrec z S (a : b) = S @ (a, b, lrec z S b) $; + +--| The set of members of list `l`: `lmems [a, b, c] = {a, b, c}`. +--| +--| `lmems : List A -> Power A` +def lmems (l: nat): nat; +theorem lmems0: $ lmems 0 = 0 $; +theorem lmemsS (a l: nat): $ lmems (a : l) = a ; lmems l $; + +--| `a IN l` means `a` is a member of the list `l`. +--| +--| `lmem : A -> List A -> Bool` +def lmem (a l: nat): wff = $ a e. lmems l $; infixl lmem: $IN$ prec 50; + +--| `all {x | p(x)} l` means every element of the list `l` satisfies `p(x)`. +def all (A: set) (l: nat): wff = $ lmems l C_ A $; + +--| `List A` is the type of lists with elements of type `A`. +--| It is inductively generated by the clauses: +--| * `0 e. List A` +--| * `a e. A -> l e. List A -> a : l e. List A` +def List (A: set) (.n: nat): set = $ {n | all A n} $; + +--| `len l` is the length of the list `l`. +--| +--| `len : List A -> nat` +def len (l: nat): nat; +theorem len0: $ len 0 = 0 $; +theorem lenS (a b: nat): $ len (a : b) = suc (len b) $; + +--| `Array A n` is the subtype of lists which have length `n`. +--| * `0 e. Array A 0` +--| * `a e. A -> l e. Array A n -> a : l e. Array A (n+1)` +def Array (A: set) (n .l: nat): set = $ {l | l e. List A /\ len l = n} $; + +--| `append l1 l2`, or `l1 ++ l2`, is the result of concatenating +--| lists `l1` and `l2`. +--| * `0 ++ l = l` +--| * `(a : l) ++ r = a : (l ++ r)` +--| +--| `append : List A -> List A -> List A` +def append (l1 l2: nat): nat; infixr append: $++$ prec 85; +theorem append0 (l: nat): $ 0 ++ l = l $; +theorem appendS (a l r: nat): $ (a : l) ++ r = a : (l ++ r) $; + +--| `snoc l a` (`cons` written backwards) or `l |> a` is the +--| result of putting `a` at the end of the list `l`: +--| * `l |> a = l ++ (a : 0)`. +--| +--| `snoc : List A -> A -> List A` +def snoc (l a: nat): nat; infixl snoc: $|>$ prec 84; +theorem snoc0 (a: nat): $ 0 |> a = a : 0 $; +theorem snocS (a b c: nat): $ (a : b) |> c = a : (b |> c) $; +theorem snoclt (a b: nat): $ a < a |> b $; + +--| `nth n l` is the element of list `l` at position `n`, +--| returning `0` (i.e. `none`) if the index is out of range. +--| * `nth n 0 = none` +--| * `nth 0 (a : l) = some a` +--| * `nth (n+1) (a : l) = nth n l` +--| +--| `nth : nat -> List A -> Option A` +def nth (n l: nat): nat; +theorem nth0 (n: nat): $ nth n 0 = 0 $; +theorem nthZ (a l: nat): $ nth 0 (a : l) = suc a $; +theorem nthS (n a l: nat): $ nth (suc n) (a : l) = nth n l $; + +--| `repeat a n` is the list of `n` repetitions of `a`. +--| +--| `repeat : A -> nat -> List A` +def repeat (a n: nat): nat; +theorem repeat0 (a: nat): $ repeat a 0 = 0 $; +theorem repeatS (a n: nat): $ repeat a (suc n) = a : repeat a n $; + +--| `map F l` is the list obtained by applying the function `F` +--| to every element of the list `l` to get another of the same length. +--| * `map F 0 = 0` +--| * `map F (a : l) = F a : map F l` +--| +--| `map : (A -> B) -> list A -> list B` +def map (F: set) (l: nat): nat; +theorem map0 (F: set): $ map F 0 = 0 $; +theorem mapS (F: set) (a l: nat): + $ map F (a : l) = F @ a : map F l $; + +--| `ljoin L` is the "join" operation of the list monad: +--| it appends all the elements of the list of lists `L`. +--| * `ljoin 0 = 0` +--| * `ljoin (l : L) = l ++ ljoin L` +--| +--| `ljoin : list (list A) -> list A` +def ljoin (L: nat): nat; +theorem ljoin0: $ ljoin 0 = 0 $; +theorem ljoinS (l L: nat): $ ljoin (l : L) = l ++ ljoin L $; + +--| `sublistAt n L1 L2` means that `L2 = L1[n..n+a]` +--| where `a` is the length of `L2`. +--| +--| `sublistAt : nat -> List A -> List A -> Bool` +def sublistAt (n L1 L2 .l .r: nat): wff = +$ E. l E. r (L1 = l ++ L2 ++ r /\ len l = n) $; + +--| `L1, L2 e. all2 R` means that `L1` and `L2` are +--| lists of the same length that are pairwise related by `R`. +--| +--| `all2 : (A -> B -> Bool) -> (list A -> list B -> Bool)` +def all2 (R: set) {.l1 .l2 .x .y .n: nat}: set = +$ S\ l1, {l2 | len l1 = len l2 /\ A. n A. x A. y + (nth n l1 = suc x -> nth n l2 = suc y -> x, y e. R)} $; + +--| `L1, L2 e. ex2 R` means that `L1` and `L2` are +--| lists of the same length for which some pair is related by `R`. +--| +--| `ex2 : (A -> B -> Bool) -> (list A -> list B -> Bool)` +def ex2 (R: set) {.l1 .l2 .x .y .n: nat}: set = +$ S\ l1, {l2 | len l1 = len l2 /\ E. n E. x E. y + (nth n l1 = suc x /\ nth n l2 = suc y /\ x, y e. R)} $; + +------------------- +-- peano_hex.mm0 -- +------------------- + + +-- The string preamble. This is used for interfacing with +-- the real world, making concrete inputs and outputs. + +--| The syntactic sort of hexadecimal digits. +--| This contains only the terms `x0..xf`. +strict free sort hex; + +--| Hexadecimal digit `0`. +term x0: hex; +--| Hexadecimal digit `1`. +term x1: hex; +--| Hexadecimal digit `2`. +term x2: hex; +--| Hexadecimal digit `3`. +term x3: hex; +--| Hexadecimal digit `4`. +term x4: hex; +--| Hexadecimal digit `5`. +term x5: hex; +--| Hexadecimal digit `6`. +term x6: hex; +--| Hexadecimal digit `7`. +term x7: hex; +--| Hexadecimal digit `8`. +term x8: hex; +--| Hexadecimal digit `9`. +term x9: hex; +--| Hexadecimal digit `a = 10`. +term xa: hex; +--| Hexadecimal digit `b = 11`. +term xb: hex; +--| Hexadecimal digit `c = 12`. +term xc: hex; +--| Hexadecimal digit `d = 13`. +term xd: hex; +--| Hexadecimal digit `e = 14`. +term xe: hex; +--| Hexadecimal digit `f = 15`. +term xf: hex; + +--| The syntactic sort of (8-bit) characters. +--| This contains only terms `ch a b` where `a` and `b` are hex digits, +--| for example `ch x4 x1`, denoting `\x41`, the ASCII character `A`. +strict free sort char; + +--| The only constructor for the sort `char`: +--| `ch a b` is the character with high nibble `a` and low nibble `b`. +term ch: hex > hex > char; + +--| The syntactic sort of byte strings. +--| The only constructors of this sort are: +--| * `s0`: the empty string +--| * `s1 c` where `c: char`: a one byte string +--| * `sadd s t`, or `s '+ t`: the concatenation of strings +--| +--| Because of this representation, there are multiple equivalent ways +--| to represent a string. (Formally, the function `s2n` is not injective.) +strict free sort string; + +--| The empty string. +term s0: string; +--| A singleton (length 1) string formed from a character. +term s1: char > string; +--| `sadd s t`, or `s '+ t`: A string formed by concatenating two smaller strings. +term sadd: string > string > string; infixr sadd: $'+$ prec 51; + +--| `c ': s` appends `c` to the front of string `s`. +def scons (c: char) (s: string): string = $ s1 c '+ s $; +infixr scons: $':$ prec 53; + +-- Peano translation functions. The sorts `hex`, `char`, `string` +-- are closed classes, but we can embed them in `nat` as lists +-- of numbers less than 256, and prove theorems on `nat` instead. +-- We have to introduce some axioms to deal with the coercion +-- functions though. + +def d11: nat = $suc 10$; prefix d11: $11$ prec max; +def d12: nat = $suc 11$; prefix d12: $12$ prec max; +def d13: nat = $suc 12$; prefix d13: $13$ prec max; +def d14: nat = $suc 13$; prefix d14: $14$ prec max; +def d15: nat = $suc 14$; prefix d15: $15$ prec max; +def d16: nat = $suc 15$; prefix d16: $16$ prec max; + +--| `h2n a`, the coercion `hex > nat`, embeds a hex digit to a natural number. +--| Because we cannot define functions by case distinction on `hex`, we must +--| axiomatize the value of this coercion on each digit. +--| This implies that all the elements of `hex` are distinct. +term h2n: hex > nat; coercion h2n: hex > nat; + +--| This allows us to prove facts about hex digits by case analysis. +--| It is not provable from the above axioms because the fact that the "hex" +--| sort has only the given 16 constructors is only observable from outside the theory. +axiom h2nlt (h: hex): $ h < 16 $; + +-- The theorems are to justify the admissibility of h2nlt +theorem d0lt16: $ 0 < 16 $; axiom h2n0: $ x0 = 0 $; +theorem d1lt16: $ 1 < 16 $; axiom h2n1: $ x1 = 1 $; +theorem d2lt16: $ 2 < 16 $; axiom h2n2: $ x2 = 2 $; +theorem d3lt16: $ 3 < 16 $; axiom h2n3: $ x3 = 3 $; +theorem d4lt16: $ 4 < 16 $; axiom h2n4: $ x4 = 4 $; +theorem d5lt16: $ 5 < 16 $; axiom h2n5: $ x5 = 5 $; +theorem d6lt16: $ 6 < 16 $; axiom h2n6: $ x6 = 6 $; +theorem d7lt16: $ 7 < 16 $; axiom h2n7: $ x7 = 7 $; +theorem d8lt16: $ 8 < 16 $; axiom h2n8: $ x8 = 8 $; +theorem d9lt16: $ 9 < 16 $; axiom h2n9: $ x9 = 9 $; +theorem d10lt16: $ 10 < 16 $; axiom h2na: $ xa = 10 $; +theorem d11lt16: $ 11 < 16 $; axiom h2nb: $ xb = 11 $; +theorem d12lt16: $ 12 < 16 $; axiom h2nc: $ xc = 12 $; +theorem d13lt16: $ 13 < 16 $; axiom h2nd: $ xd = 13 $; +theorem d14lt16: $ 14 < 16 $; axiom h2ne: $ xe = 14 $; +theorem d15lt16: $ 15 < 16 $; axiom h2nf: $ xf = 15 $; + +--| `h2n a`, the coercion `char > nat`, embeds a character +--| as a natural number less than 256. +term c2n: char > nat; coercion c2n: char > nat; +--| The `c2n` function is less than 256 for all elements of the type `char`. +--| This ensures that there are no other elements in the syntactic sort `char`. +axiom c2nlt (c: char): $ c < 16 * 16 $; +--| Justifies the use of c2nch and c2nlt +theorem chlt256 (hi lo: hex): $ hi * 16 + lo < 16 * 16 $; +--| The value of `c2n (ch hi lo) = h2n hi * 16 + h2n lo`. +axiom c2nch (hi lo: hex): $ ch hi lo = hi * 16 + lo $; + +--| `s2n s`, the coercion `string > nat`, +--| interprets a string as a `List u8` in the obvious way: +--| * `s2n s0 = 0` +--| * `s2n (s1 c) = c2n c : 0` +--| * `s2n (s '+ t) = s2n s ++ s2n t` +--| +--| Because `string` is a syntactic sort, it does not have quantifiers +--| so our ability to prove properties about it is limited; +--| but using this function we can obtain a `nat` which we can prove +--| theorems about. +term s2n: string > nat; coercion s2n: string > nat; +def isStr (s .c: nat): wff = $ all {c | c < 16 * 16} s $; +--| The `s2n` function returns a list all of whose elements +--| are numbers less than 256. +axiom s2nstr (s: string): $ isStr s $; +theorem s0str: $ isStr 0 $; +axiom s2ns0: $ s0 = 0 $; +theorem s1str (c: char): $ isStr (c : 0) $; +axiom s2ns1 (c: char): $ s1 c = c : 0 $; +theorem saddstr (s t: string): $ isStr (s ++ t) $; +axiom s2nsadd (s t: string): $ s '+ t = s ++ t $; + +------------- +-- x86.mm0 -- +------------- + + +def consBit (b: wff) (n: nat): nat = $ if b (b1 n) (b0 n) $; + +def bit (n i: nat): nat = $ nat (i e. n) $; +theorem bitT (n i: nat): $ bool (bit n i) $; + +def bitAnd (a b: nat): nat; +theorem bitAndEq (a b: nat): $ bitAnd a b == a i^i b $; + +def bitOr (a b: nat): nat; +theorem bitOrEq (a b: nat): $ bitOr a b == a u. b $; + +def bitDif (a b: nat): nat; +theorem bitDifEq (a b: nat): $ bitDif a b == a i^i Compl b $; + +def bitXor (a b: nat): nat; +theorem bitXor_mem (a b i: nat): $ i e. bitXor a b <-> ~(i e. a <-> i e. b) $; + +def d32: nat = $ 2 ^ 5 $; prefix d32: $32$ prec max; +def d64: nat = $ 2 ^ 6 $; prefix d64: $64$ prec max; +def d256: nat = $ 2 ^ 8 $; prefix d256: $256$ prec max; + +def Bits (k: nat): nat = $ upto (2 ^ k) $; +def u8: nat = $ Bits 8 $; +def u16: nat = $ Bits 16 $; +def u32: nat = $ Bits 32 $; +def u64: nat = $ Bits 64 $; + +--| Get the lower bits of a number +def chop (k n: nat): nat = $ n % 2 ^ k $; +theorem chopT (k n: nat): $ chop k n e. Bits k $; + +def bitsMSB (k n: nat): wff = $ 0 < k /\ k - 1 e. n $; + +--| Sign extend `(v: bitvec m)` to length `n` +def sExt (m n v: nat): nat = $ if (bitsMSB m v) (2 ^ n - 2 ^ m + v) v $; +def sExtq (n v: nat): nat = $ sExt n 64 v $; +theorem sExtT (m n v: nat): $ m <= n /\ v e. Bits m -> sExt m n v e. Bits n $; +theorem sExtqT (n v: nat): $ n <= 64 /\ v e. Bits n -> sExtq n v e. u64 $; + +--| Write `a e. Bits m` to bits `k` thru `k+m-1` of `n` +def bitsUpdate (k m a n: nat): nat = $ bitDif n (shl (upto m) k) + shl a k $; +theorem bitsUpdateT (k m l a n: nat): + $ k + m <= l /\ a e. Bits m /\ n e. Bits l -> bitsUpdate k m a n e. Bits l $; + +def bitsNot (k n: nat): nat = $ bitDif (upto k) n $; +theorem bitsNot_mem (k n i: nat): $ i e. bitsNot k n <-> i < k /\ ~i e. n $; +theorem bitsNotT (k n: nat): $ bitsNot k n e. Bits k $; + +def bitsAdd (k a b: nat): nat = $ chop k (a + b) $; +theorem bitsAddT (k a b: nat): $ bitsAdd k a b e. Bits k $; + +def bitsNeg (k n: nat): nat = $ bitsAdd k (bitsNot k n) 1 $; +theorem bitsNegT (k n: nat): $ bitsNeg k n e. Bits k $; + +def bitsSub (k a b: nat): nat = $ bitsAdd k a (bitsNeg k b) $; +theorem bitsSubT (k a b: nat): $ bitsSub k a b e. Bits k $; + +def bitsSar (k a b: nat): nat = +$ nat (bitsMSB k a) * (upto k - upto (k - b)) + shr a b $; +theorem bitsSarT (k a b: nat): + $ a e. Bits k /\ b <= k -> bitsSar k a b e. Bits k $; + +def add64 (a b: nat): nat = $ bitsAdd 64 a b $; infixl add64: $+_64$ prec 65; +theorem add64T (a b: nat): $ a +_64 b e. u64 $; +def sub64 (a b: nat): nat = $ bitsSub 64 a b $; infixl sub64: $-_64$ prec 65; +theorem sub64T (a b: nat): $ a -_64 b e. u64 $; + +--| Little endian encoding +def toBytes (k n: nat): nat; +theorem toBytes0 (n: nat): $ toBytes 0 n = 0 $; +theorem toBytesS (k n: nat): + $ toBytes (suc k) n = (n % 256) : toBytes k (n // 256) $; +theorem toBytesT (k n: nat): $ toBytes k n e. Array u8 k $; + +def u16Bytes (n: nat): nat = $ toBytes 2 n $; +def u32Bytes (n: nat): nat = $ toBytes 4 n $; +def u64Bytes (n: nat): nat = $ toBytes 8 n $; + +def Bitvec {.n: nat}: set = $ {n | snd n < 2 ^ fst n} $; + +def bvSize (bs: nat): nat; +theorem bvSize0: $ bvSize 0 = 0 $; +theorem bvSizeS (k n bs: nat): $ bvSize ((k, n) : bs) = k + bvSize bs $; + +def isBitvecs (bs k: nat): wff = $ bs e. List Bitvec /\ bvSize bs = k $; + +def ofBits (n: nat): nat; +theorem ofBits0: $ ofBits 0 = 0 $; +theorem ofBitsS (k n bs: nat): $ ofBits ((k, n) : bs) = n + shl (ofBits bs) k $; +theorem ofBits0T: $ ofBits 0 e. Bits 0 $; +theorem ofBitsST (k n bs m: nat): + $ n e. Bits k /\ ofBits bs e. Bits m -> + ofBits ((k, n) : bs) e. Bits (k + m) $; + +def splitBits (bs n: nat): wff = $ bs e. List Bitvec /\ ofBits bs = n $; +theorem splitBitsT (bs n k: nat): + $ isBitvecs bs k /\ splitBits bs n -> n e. Bits k $; + +---------------------------------------- +-- x86-64 machine code decoding +---------------------------------------- + +def Regs: nat = $ Bits 4 $; +def RAX: nat = $ 0 $; theorem RAX_T: $ RAX e. Regs $; +def RCX: nat = $ 1 $; theorem RCX_T: $ RCX e. Regs $; +def RDX: nat = $ 2 $; theorem RDX_T: $ RDX e. Regs $; +def RBX: nat = $ 3 $; theorem RBX_T: $ RBX e. Regs $; +def RSP: nat = $ 4 $; theorem RSP_T: $ RSP e. Regs $; +def RBP: nat = $ 5 $; theorem RBP_T: $ RBP e. Regs $; +def RSI: nat = $ 6 $; theorem RSI_T: $ RSI e. Regs $; +def RDI: nat = $ 7 $; theorem RDI_T: $ RDI e. Regs $; + +def REX: set = $ Option (Bits 4) $; +def REX_val (r: nat): nat = $ r - 1 $; +def REX_W (r: nat): nat = $ bit (REX_val r) 3 $; +def REX_R (r: nat): nat = $ bit (REX_val r) 2 $; +def REX_X (r: nat): nat = $ bit (REX_val r) 1 $; +def REX_B (r: nat): nat = $ bit (REX_val r) 0 $; +theorem REX_valT (r: nat): $ r e. REX -> REX_val r e. Bits 4 $; +theorem REX_W_T (r: nat): $ bool (REX_W r) $; +theorem REX_R_T (r: nat): $ bool (REX_R r) $; +theorem REX_X_T (r: nat): $ bool (REX_X r) $; +theorem REX_B_T (r: nat): $ bool (REX_B r) $; + +def rex_reg (b r: nat): nat = $ shl b 3 + r $; +theorem rex_regT (b r: nat): $ bool b /\ r e. Bits 3 -> rex_reg b r e. Regs $; + +def Base: set = $ Option (Option Regs) $; +def base_RIP: nat = $ suc 0 $; +def base_reg (r: nat): nat = $ suc (suc r) $; +theorem base0T: $ 0 e. Base $; +theorem base_RIP_T: $ base_RIP e. Base $; +theorem base_regT (r: nat): $ base_reg r e. Base <-> r e. Regs $; + +def ScaleIndex: set = $ Xp (Bits 2) Regs $; + +def RM: set = $ Sum Regs (Xp (Option ScaleIndex) (Xp Base u64)) $; +def RM_reg (r: nat): nat = $ b0 r $; +def RM_mem (si base q: nat): nat = $ b1 (si, base, q) $; +theorem RM_regT (r: nat): $ RM_reg r e. RM <-> r e. Regs $; +theorem RM_memT (si base q: nat): + $ RM_mem si base q e. RM <-> + si e. Option ScaleIndex /\ base e. Base /\ q e. u64 $; + +def RM_isMem (rm: nat): wff = $ odd rm $; + +def readDisplacement (mod q l .b .w: nat): wff = +$ mod = 0 /\ q = 0 /\ l = 0 \/ + E. b (b e. u8 /\ mod = 1 /\ q = sExtq 8 b /\ l = b : 0) \/ + E. w (w e. u32 /\ mod = 2 /\ q = sExtq 32 w /\ l = u32Bytes w) $; +theorem readDisplacementT (mod q l: nat): + $ readDisplacement mod q l -> + mod e. Bits 2 /\ mod != 3 /\ q e. u64 /\ l e. List u8 $; + +def readSIBDisplacement (mod bbase q base l .w: nat): wff = +$ ifp (bbase = RBP /\ mod = 0) + (E. w (w e. u32 /\ q = sExtq 32 w /\ base = 0 /\ l = u32Bytes w)) + (readDisplacement mod q l /\ base = base_reg bbase) $; +theorem readSIBDisplacementT (mod bbase q base l: nat): + $ bbase e. Regs /\ readSIBDisplacement mod bbase q base l -> + mod e. Bits 2 /\ mod != 3 /\ q e. u64 /\ base e. Base /\ l e. List u8 $; + +def readSIB (rex mod rm l .b .l2 .bs .ix .sc .disp .bbase .index: nat): wff = +$ E. b E. l2 E. bs E. ix E. sc E. disp E. bbase E. index ( + splitBits ((3, bs) : (3, ix) : (2, sc) : 0) b /\ + index = rex_reg (REX_X rex) ix /\ + readSIBDisplacement mod (rex_reg (REX_B rex) bs) disp bbase l2 /\ + rm = RM_mem (if (index = RSP) 0 (suc (sc, index))) bbase disp /\ + l = b : l2) $; +theorem readSIB_T (rex mod rm l: nat): + $ readSIB rex mod rm l -> + mod e. Bits 2 /\ mod != 3 /\ rm e. RM /\ l e. List u8 $; + +def readModRM (rex rn rm l .b .rm2 .opc .mod .i .l2 .disp: nat): wff = +$ E. b E. rm2 E. opc E. mod ( + splitBits ((3, rm2) : (3, opc) : (2, mod) : 0) b /\ + rn = rex_reg (REX_R rex) opc /\ + ifp (mod = 3) + (rm = RM_reg (rex_reg (REX_B rex) rm2) /\ + l = b : 0) + (ifp (rm2 = 5 /\ mod = 0) + (E. i (i e. u32 /\ + rm = RM_mem 0 base_RIP (sExtq 32 i) /\ + l = b : u32Bytes i)) + (E. l2 (l = b : l2 /\ + ifp (rm2 = 4) (readSIB rex mod rm l2) + (E. disp (readDisplacement mod disp l2 /\ + rm = RM_mem 0 (base_reg (rex_reg (REX_B rex) rm2)) disp)))))) $; +theorem readModRM_T (rex rn rm l: nat): + $ readModRM rex rn rm l -> rn e. Regs /\ rm e. RM /\ l e. List u8 $; + +def readOpcodeModRM (rex v rm l .rn: nat): wff = +$ E. rn (readModRM rex rn rm l /\ v = chop 3 rn) $; +theorem readOpcodeModRM_T (rex v rm l: nat): + $ readOpcodeModRM rex v rm l -> v e. Bits 3 /\ rm e. RM /\ l e. List u8 $; + +def readPrefixes (rex l .b .rex2: nat): wff = +$ rex = 0 /\ l = 0 \/ E. b E. rex2 ( + splitBits ((4, rex2) : (4, 4) : 0) b /\ + rex = suc rex2 /\ l = b : 0) $; +theorem readPrefixesT (rex l: nat): + $ readPrefixes rex l -> rex e. REX /\ l e. List u8 $; + +def readImmN (k q l .w: nat): wff = +$ 8 || k /\ E. w (w e. Bits k /\ q = sExtq k w /\ l = toBytes (k // 8) w) $; +theorem readImmN_T (k q l: nat): + $ k <= 64 /\ readImmN k q l -> q e. u64 /\ l e. List u8 $; + +def WSize (.n: nat): set = $ Xp (8 ; 16 ; 32 ; sn 64) Bool i^i {n | fst n = 8 \/ snd n = 0} $; +def wsizeBits (sz: nat): nat = $ fst sz $; +def wsizeBytes (sz: nat): nat = $ wsizeBits sz // 8 $; +def wSz8 (have_rex: wff): nat = $ 8, nat have_rex $; +def wSz16: nat = $ 16, 0 $; +def wSz32: nat = $ 32, 0 $; +def wSz64: nat = $ 64, 0 $; + +def readFullImm (sz q l: nat): wff = +$ readImmN (wsizeBits sz) q l $; +theorem readFullImmT (sz q l: nat): + $ sz e. WSize /\ readFullImm sz q l -> q e. u64 /\ l e. List u8 $; + +def readImm (sz q l: nat): wff = +$ readImmN (min (wsizeBits sz) 32) q l $; +theorem readImmT (sz q l: nat): + $ sz e. WSize /\ readImm sz q l -> q e. u64 /\ l e. List u8 $; + +def opSize (have_rex: wff) (w v: nat): nat = +$ if (true v) (if (true w) wSz64 wSz32) (wSz8 have_rex) $; +theorem opSizeT (have_rex: wff) (w v: nat): $ opSize have_rex w v e. WSize $; + +def opSizeW (rex v: nat): nat = $ opSize (rex != 0) (REX_W rex) v $; +theorem opSizeW_T (rex v: nat): $ opSizeW rex v e. WSize $; + +def DestSrc: set = $ Sum (Xp RM (Sum u64 Regs)) (Xp Regs RM) $; +def Rm_i (rm i: nat): nat = $ b0 (rm, b0 i) $; +def Rm_r (rm r: nat): nat = $ b0 (rm, b1 r) $; +def R_rm (r rm: nat): nat = $ b1 (r, rm) $; +theorem Rm_iT (rm i: nat): $ Rm_i rm i e. DestSrc <-> rm e. RM /\ i e. u64 $; +theorem Rm_rT (rm r: nat): $ Rm_r rm r e. DestSrc <-> rm e. RM /\ r e. Regs $; +theorem R_rmT (r rm: nat): $ R_rm r rm e. DestSrc <-> r e. Regs /\ rm e. RM $; + +def ImmRM: set = $ Sum RM u64 $; +def immRM_rm (rm: nat): nat = $ b0 rm $; +def immRM_imm (i: nat): nat = $ b1 i $; +theorem immRM_rmT (rm: nat): $ immRM_rm rm e. ImmRM <-> rm e. RM $; +theorem immRM_immT (i: nat): $ immRM_imm i e. ImmRM <-> i e. u64 $; + +def Unop: nat = $ upto 4 $; +def unopInc: nat = $ 0 $; +def unopDec: nat = $ 1 $; +def unopNot: nat = $ 2 $; +def unopNeg: nat = $ 3 $; + +def Binop: nat = $ Bits 4 $; +def binopAdd: nat = $ 0 $; +def binopOr: nat = $ 1 $; +def binopAdc: nat = $ 2 $; +def binopSbb: nat = $ 3 $; +def binopAnd: nat = $ 4 $; +def binopSub: nat = $ 5 $; +def binopXor: nat = $ 6 $; +def binopCmp: nat = $ 7 $; +def binopRol: nat = $ 8 $; +def binopRor: nat = $ 9 $; +def binopRcl: nat = $ 10 $; +def binopRcr: nat = $ 11 $; +def binopShl: nat = $ 12 $; +def binopShr: nat = $ 13 $; +def binopTst: nat = $ 14 $; +def binopSar: nat = $ 15 $; + +def BCond: nat = $ Bits 3 $; +def bcondO: nat = $ 0 $; +def bcondB: nat = $ 1 $; +def bcondE: nat = $ 2 $; +def bcondNA: nat = $ 3 $; +def bcondS: nat = $ 4 $; +def bcondL: nat = $ 6 $; +def bcondNG: nat = $ 7 $; + +def Cond: set = $ Option (Bits 4) $; +def condAlways: nat = $ 0 $; +def condPos (c: nat): nat = $ suc (b0 c) $; +def condNeg (c: nat): nat = $ suc (b1 c) $; +theorem condAlwaysT: $ condAlways e. Cond $; +theorem condPosT (c: nat): $ c e. BCond <-> condPos c e. Cond $; +theorem condNegT (c: nat): $ c e. BCond <-> condNeg c e. Cond $; + +def XASTArith: set = +$ Sum (Sum (Xp Unop (Xp WSize RM)) (Xp Binop (Xp WSize DestSrc))) + (Sum (Xp Bool (Xp WSize RM)) (Xp WSize (Option DestSrc))) $; +def xastUnop (unop sz rm: nat): nat = $ b0 (b0 (b0 (b0 (unop, sz, rm)))) $; +def xastBinop (binop sz ds: nat): nat = $ b0 (b0 (b0 (b1 (binop, sz, ds)))) $; +def xastMul (sz rm: nat): nat = $ b0 (b0 (b1 (b0 (0, sz, rm)))) $; +def xastDiv (sz rm: nat): nat = $ b0 (b0 (b1 (b0 (1, sz, rm)))) $; +def xastCDX (sz: nat): nat = $ b0 (b0 (b1 (b1 (sz, 0)))) $; +def xastLea (sz ds: nat): nat = $ b0 (b0 (b1 (b1 (sz, suc ds)))) $; + +def XASTData: set = +$ Sum (Xp WSize (Sum (Xp Bool (Xp DestSrc WSize)) (Xp (upto 3) (Xp RM Regs)))) + (Xp Cond (Sum (Xp WSize DestSrc) (Xp Bool RM))) $; +def xastMovX (b sz ds sz2: nat): nat = $ b0 (b1 (b0 (sz, b0 (b, ds, sz2)))) $; +def xastXchg (sz rm rn: nat): nat = $ b0 (b1 (b0 (sz, b1 (0, rm, rn)))) $; +def xastCmpXchg (sz rm rn: nat): nat = $ b0 (b1 (b0 (sz, b1 (1, rm, rn)))) $; +def xastXadd (sz rm rn: nat): nat = $ b0 (b1 (b0 (sz, b1 (2, rm, rn)))) $; +def xastCMov (c sz ds: nat): nat = $ b0 (b1 (b1 (c, b0 (sz, ds)))) $; +def xastSetCC (c b ds: nat): nat = $ b0 (b1 (b1 (c, b1 (b, ds)))) $; + +def xastMov (sz ds: nat): nat = $ xastCMov condAlways sz ds $; +def xastMovZX (sz ds sz2: nat): nat = $ xastMovX 0 sz ds sz2 $; +def xastMovSX (sz ds sz2: nat): nat = $ xastMovX 1 sz ds sz2 $; + +def XASTFlow: set = +$ Sum (Sum (Sum RM (Xp Cond u64)) (Sum ImmRM u64)) (Option (Sum ImmRM RM)) $; +def xastJump (rm: nat): nat = $ b1 (b0 (b0 (b0 (b0 rm)))) $; +def xastJCC (c q: nat): nat = $ b1 (b0 (b0 (b0 (b1 (c, q))))) $; +def xastCall (irm: nat): nat = $ b1 (b0 (b0 (b1 (b0 irm)))) $; +def xastRet (q: nat): nat = $ b1 (b0 (b0 (b1 (b1 q)))) $; +def xastLeave: nat = $ b1 (b0 (b1 0)) $; +def xastPush (irm: nat): nat = $ b1 (b0 (b1 (suc (b0 irm)))) $; +def xastPop (rm: nat): nat = $ b1 (b0 (b1 (suc (b1 rm)))) $; + +def XASTMisc: set = $ upto 5 $; +def xastCMC: nat = $ b1 (b1 0) $; +def xastCLC: nat = $ b1 (b1 1) $; +def xastSTC: nat = $ b1 (b1 2) $; +def xastUD2: nat = $ b1 (b1 3) $; +def xastSysCall: nat = $ b1 (b1 4) $; + +def XAST: set = $ Sum (Sum XASTArith XASTData) (Sum XASTFlow XASTMisc) $; + +-- some typechecking sanity checks +theorem xastUnopT (unop sz rm: nat): + $ xastUnop unop sz rm e. XAST <-> unop e. Unop /\ sz e. WSize /\ rm e. RM $; +theorem xastBinopT (bop sz ds: nat): + $ xastBinop bop sz ds e. XAST <-> bop e. Binop /\ sz e. WSize /\ ds e. DestSrc $; +theorem xastMulT (sz rm: nat): + $ xastMul sz rm e. XAST <-> sz e. WSize /\ rm e. RM $; +theorem xastDivT (sz rm: nat): + $ xastDiv sz rm e. XAST <-> sz e. WSize /\ rm e. RM $; +theorem xastCDX_T (sz: nat): + $ xastCDX sz e. XAST <-> sz e. WSize $; +theorem xastLeaT (sz ds: nat): + $ xastLea sz ds e. XAST <-> sz e. WSize /\ ds e. DestSrc $; + +theorem xastMovX_T (b sz ds sz2: nat): + $ xastMovX b sz ds sz2 e. XAST <-> + bool b /\ sz e. WSize /\ ds e. DestSrc /\ sz2 e. WSize $; +theorem xastXchgT (sz rm rn: nat): + $ xastXchg sz rm rn e. XAST <-> sz e. WSize /\ rm e. RM /\ rn e. Regs $; +theorem xastCmpXchgT (sz rm rn: nat): + $ xastCmpXchg sz rm rn e. XAST <-> sz e. WSize /\ rm e. RM /\ rn e. Regs $; +theorem xastXaddT (sz rm rn: nat): + $ xastXadd sz rm rn e. XAST <-> sz e. WSize /\ rm e. RM /\ rn e. Regs $; +theorem xastCMovT (c sz ds: nat): + $ xastCMov c sz ds e. XAST <-> c e. Cond /\ sz e. WSize /\ ds e. DestSrc $; +theorem xastSetCC_T (c b rm: nat): + $ xastSetCC c b rm e. XAST <-> c e. Cond /\ bool b /\ rm e. RM $; +theorem xastMovZX_T (sz ds sz2: nat): + $ xastMovZX sz ds sz2 e. XAST <-> sz e. WSize /\ ds e. DestSrc /\ sz2 e. WSize $; +theorem xastMovSX_T (sz ds sz2: nat): + $ xastMovSX sz ds sz2 e. XAST <-> sz e. WSize /\ ds e. DestSrc /\ sz2 e. WSize $; +theorem xastMovT (sz ds: nat): + $ xastMov sz ds e. XAST <-> sz e. WSize /\ ds e. DestSrc $; + +theorem xastJumpT (rm: nat): $ xastJump rm e. XAST <-> rm e. RM $; +theorem xastJCC_T (c q: nat): $ xastJCC c q e. XAST <-> c e. Cond /\ q e. u64 $; +theorem xastCallT (irm: nat): $ xastCall irm e. XAST <-> irm e. ImmRM $; +theorem xastRetT (q: nat): $ xastRet q e. XAST <-> q e. u64 $; +theorem xastLeaveT: $ xastLeave e. XAST $; +theorem xastPushT (irm: nat): $ xastPush irm e. XAST <-> irm e. ImmRM $; +theorem xastPopT (rm: nat): $ xastPop rm e. XAST <-> rm e. RM $; + +theorem xastCMC_T: $ xastCMC e. XAST $; +theorem xastCLC_T: $ xastCLC e. XAST $; +theorem xastSTC_T: $ xastSTC e. XAST $; +theorem xastUD2T: $ xastUD2 e. XAST $; +theorem xastSysCallT: $ xastSysCall e. XAST $; + +def decodeTwoCMov (rex ast b l .c .reg .r: nat): wff = +$ E. c E. reg E. r (splitBits ((4, c) : (4, 4) : 0) b /\ + readModRM rex reg r l /\ + ast = xastCMov (suc c) (opSize T. (REX_W rex) 1) (R_rm reg r)) $; +theorem decodeTwoCMovT (rex ast b l: nat): + $ decodeTwoCMov rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeTwoJCC (_rex ast b l .c .imm: nat): wff = +$ E. c E. imm (splitBits ((4, c) : (4, 8) : 0) b /\ + readImmN 32 imm l /\ + ast = xastJCC (suc c) imm) $; +theorem decodeTwoJCC_T (rex ast b l: nat): + $ decodeTwoJCC rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeTwoSetCC (rex ast b l .c .reg .r: nat): wff = +$ E. c E. reg E. r (splitBits ((4, c) : (4, 9) : 0) b /\ + readModRM rex reg r l /\ + ast = xastSetCC (suc c) (nat (rex != 0)) r) $; +theorem decodeTwoSetCC_T (rex ast b l: nat): + $ decodeTwoSetCC rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeTwoCmpXchg (rex ast b l .v .reg .r: nat): wff = +$ E. v E. reg E. r (splitBits ((1, v) : (3, 0) : (4, 11) : 0) b /\ + readModRM rex reg r l /\ + ast = xastCmpXchg (opSizeW rex v) r reg) $; +theorem decodeTwoCmpXchgT (rex ast b l: nat): + $ decodeTwoCmpXchg rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeTwoMovX (rex ast b l .v .s .reg .r: nat): wff = +$ E. v E. s E. reg E. r ( + splitBits ((1, v) : (2, 3) : (1, s) : (4, 11) : 0) b /\ + readModRM rex reg r l /\ + ast = xastMovX s (if (bool v) wSz16 (wSz8 (rex != 0))) + (R_rm reg r) (opSizeW rex 1)) $; +theorem decodeTwoMovX_T (rex ast b l: nat): + $ decodeTwoMovX rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeTwoXadd (rex ast b l .v .reg .r: nat): wff = +$ E. v E. reg E. r ( + splitBits ((1, v) : (3, 0) : (4, 12) : 0) b /\ + readModRM rex reg r l /\ + ast = xastXadd (opSizeW rex v) r reg) $; +theorem decodeTwoXaddT (rex ast b l: nat): + $ decodeTwoXadd rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeTwoUD2 (_rex ast b l: nat): wff = +$ b = ch x0 xb /\ l = 0 /\ ast = xastUD2 $; +theorem decodeTwoUD2T (rex ast b l: nat): + $ decodeTwoUD2 rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeTwoSysCall (_rex ast b l: nat): wff = +$ b = ch x0 x5 /\ l = 0 /\ ast = xastSysCall $; +theorem decodeTwoSysCallT (rex ast b l: nat): + $ decodeTwoSysCall rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeTwoAux (rex ast b l: nat): wff = +$ decodeTwoCMov rex ast b l \/ decodeTwoJCC rex ast b l \/ + decodeTwoSetCC rex ast b l \/ decodeTwoCmpXchg rex ast b l \/ + decodeTwoMovX rex ast b l \/ decodeTwoXadd rex ast b l \/ + decodeTwoUD2 rex ast b l \/ decodeTwoSysCall rex ast b l $; +theorem decodeTwoAuxT (rex ast b l: nat): + $ decodeTwoAux rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeTwo (rex ast b l .b2 .l2: nat): wff = +$ b = ch x0 xf /\ E. b2 E. l2 (l = b2 : l2 /\ decodeTwoAux rex ast b2 l2) $; +theorem decodeTwoT (rex ast b l: nat): + $ decodeTwo rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeBinopReg (rex ast b l .v .d .opc .reg .r: nat): wff = +$ E. v E. d E. opc E. reg E. r ( + splitBits ((1, v) : (1, d) : (1, 0) : (3, opc) : (2, 0) : 0) b /\ + readModRM rex reg r l /\ + ast = xastBinop opc (opSizeW rex v) + (if (true d) (R_rm reg r) (Rm_r r reg))) $; +theorem decodeBinopRegT (rex ast b l: nat): + $ decodeBinopReg rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeBinopRAX (rex ast b l .v .opc .imm: nat): wff = +$ E. v E. opc E. imm ( + splitBits ((1, v) : (2, 2) : (3, opc) : (2, 0) : 0) b /\ + readImm (opSizeW rex v) imm l /\ + ast = xastBinop opc (opSizeW rex v) (Rm_i (RM_reg RAX) imm)) $; +theorem decodeBinopRAX_T (rex ast b l: nat): + $ decodeBinopRAX rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeBinopImm (rex ast b l .v .opc .r .l1 .imm .l2: nat): wff = +$ E. v E. opc E. r E. l1 E. imm E. l2 (l = l1 ++ l2 /\ + splitBits ((1, v) : (3, 0) : (4, 8) : 0) b /\ + readOpcodeModRM rex opc r l1 /\ + readImm (opSizeW rex v) imm l2 /\ + ast = xastBinop opc (opSizeW rex v) (Rm_i r imm)) $; +theorem decodeBinopImmT (rex ast b l: nat): + $ decodeBinopImm rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeBinopImm8 (rex ast b l .opc .r .l1 .imm .l2: nat): wff = +$ E. opc E. r E. imm E. l1 E. l2 (l = l1 ++ l2 /\ b = ch x8 x3 /\ + readOpcodeModRM rex opc r l1 /\ + readImmN 8 imm l2 /\ + ast = xastBinop opc (opSizeW rex 1) (Rm_i r imm)) $; +theorem decodeBinopImm8T (rex ast b l: nat): + $ decodeBinopImm8 rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeBinopHi (rex ast b l .v .opc .r .imm .l1 .l2: nat): wff = +$ E. v E. opc E. r E. imm E. l1 E. l2 (l = l1 ++ l2 /\ + splitBits ((1, v) : (3, 0) : (4, 12) : 0) b /\ + readOpcodeModRM rex opc r l1 /\ opc != 6 /\ + readImmN 8 imm l2 /\ + ast = xastBinop (rex_reg 1 opc) (opSizeW rex v) (Rm_i r imm)) $; +theorem decodeBinopHiT (rex ast b l: nat): + $ decodeBinopHi rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeBinopHiReg (rex ast b l .v .x .opc .r: nat): wff = +$ E. v E. x E. opc E. r ( + splitBits ((1, v) : (1, x) : (2, 0) : (4, 13) : 0) b /\ + readOpcodeModRM rex opc r l /\ opc != 6 /\ + ast = xastBinop (rex_reg 1 opc) (opSizeW rex v) + (if (true x) (Rm_r r RCX) (Rm_i r 1))) $; +theorem decodeBinopHiRegT (rex ast b l: nat): + $ decodeBinopHiReg rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeBinop (rex ast b l: nat): wff = +$ decodeBinopReg rex ast b l \/ decodeBinopRAX rex ast b l \/ + decodeBinopImm rex ast b l \/ decodeBinopImm8 rex ast b l \/ + decodeBinopHi rex ast b l \/ decodeBinopHiReg rex ast b l $; +theorem decodeBinopT (rex ast b l: nat): + $ decodeBinop rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeMovSX (rex ast b l .reg .r: nat): wff = +$ E. reg E. r (b = ch x6 x3 /\ + readModRM rex reg r l /\ ast = xastMovSX wSz32 (R_rm reg r) (opSizeW rex 1)) $; +theorem decodeMovSX_T (rex ast b l: nat): + $ decodeMovSX rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeMovReg (rex ast b l .v .d .reg .r: nat): wff = +$ E. v E. d E. reg E. r ( + splitBits ((1, v) : (1, d) : (2, 2) : (4, 8) : 0) b /\ + readModRM rex reg r l /\ + ast = xastMov (opSizeW rex v) (if (true d) (R_rm reg r) (Rm_r r reg))) $; +theorem decodeMovRegT (rex ast b l: nat): + $ decodeMovReg rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeMov64 (rex ast b l .r .v .imm: nat): wff = +$ E. r E. v E. imm ( + splitBits ((3, r) : (1, v) : (4, 11) : 0) b /\ + readFullImm (opSizeW rex v) imm l /\ + ast = xastMov (opSizeW rex v) (Rm_i (RM_reg (rex_reg (REX_B rex) r)) imm)) $; +theorem decodeMov64T (rex ast b l: nat): + $ decodeMov64 rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeMovImm (rex ast b l .v .opc .r .imm .l1 .l2: nat): wff = +$ E. v E. r E. imm E. l1 E. l2 (l = l1 ++ l2 /\ + splitBits ((1, v) : (3, 3) : (4, 12) : 0) b /\ + readOpcodeModRM rex 0 r l1 /\ + readImm (opSizeW rex v) imm l2 /\ + ast = xastMov (opSizeW rex v) (Rm_i r imm)) $; +theorem decodeMovImmT (rex ast b l: nat): + $ decodeMovImm rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeMov (rex ast b l: nat): wff = +$ decodeMovSX rex ast b l \/ decodeMovReg rex ast b l \/ + decodeMov64 rex ast b l \/ decodeMovImm rex ast b l $; +theorem decodeMovT (rex ast b l: nat): + $ decodeMov rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodePushImm (_rex ast b l .x .imm .r: nat): wff = +$ E. x E. imm ( + splitBits ((1, 0) : (1, x) : (2, 2) : (4, 6) : 0) b /\ + readImmN (if (true x) 8 32) imm l /\ + ast = xastPush (immRM_imm imm)) $; +theorem decodePushImmT (rex ast b l: nat): + $ decodePushImm rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodePushReg (rex ast b l .x .imm .r: nat): wff = +$ l = 0 /\ E. r ( + splitBits ((3, r) : (1, 0) : (4, 5) : 0) b /\ + ast = xastPush (immRM_rm (RM_reg (rex_reg (REX_B rex) r)))) $; +theorem decodePushRegT (rex ast b l: nat): + $ decodePushReg rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodePopReg (rex ast b l .r: nat): wff = +$ l = 0 /\ E. r ( + splitBits ((3, r) : (1, 1) : (4, 5) : 0) b /\ + ast = xastPop (RM_reg (rex_reg (REX_B rex) r))) $; +theorem decodePopRegT (rex ast b l: nat): + $ decodePopReg rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodePop0 (rex ast b l .r: nat): wff = +$ E. r (b = ch x8 xf /\ readOpcodeModRM rex 0 r l /\ ast = xastPop r) $; +theorem decodePop0T (rex ast b l: nat): + $ decodePop0 rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeStack (rex ast b l .r: nat): wff = +$ decodePushImm rex ast b l \/ decodePushReg rex ast b l \/ + decodePopReg rex ast b l \/ decodePop0 rex ast b l $; +theorem decodeStackT (rex ast b l: nat): + $ decodeStack rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeJump (_rex ast b l .x .imm: nat): wff = +$ E. x E. imm ( + splitBits ((1, 1) : (1, x) : (2, 2) : (4, 14) : 0) b /\ + readImmN (if (true x) 8 32) imm l /\ + ast = xastJCC condAlways imm) $; +theorem decodeJumpT (rex ast b l: nat): + $ decodeJump rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeJCC8 (_rex ast b l .c .imm: nat): wff = +$ E. c E. imm (splitBits ((4, c) : (4, 7) : 0) b /\ + readImmN 8 imm l /\ ast = xastJCC (suc c) imm) $; +theorem decodeJCC8T (rex ast b l: nat): + $ decodeJCC8 rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeCall (_rex ast b l .imm: nat): wff = +$ E. imm (b = ch xe x8 /\ + readImmN 32 imm l /\ ast = xastCall (immRM_imm imm)) $; +theorem decodeCallT (rex ast b l: nat): + $ decodeCall rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeRet (_rex ast b l .v .imm: nat): wff = +$ E. v E. imm ( + splitBits ((1, v) : (3, 1) : (4, 12) : 0) b /\ + ifp (true v) (imm = 0 /\ l = 0) (readImmN 16 imm l) /\ + ast = xastRet imm) $; +theorem decodeRetT (rex ast b l: nat): + $ decodeRet rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeLeave (_rex ast b l: nat): wff = +$ b = ch xc x9 /\ l = 0 /\ ast = xastLeave $; +theorem decodeLeaveT (rex ast b l: nat): + $ decodeLeave rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeFlow (rex ast b l: nat): wff = +$ decodeJump rex ast b l \/ decodeJCC8 rex ast b l \/ + decodeCall rex ast b l \/ decodeRet rex ast b l \/ decodeLeave rex ast b l $; +theorem decodeFlowT (rex ast b l: nat): + $ decodeFlow rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeXchg (rex ast b l .v .reg .r: nat): wff = +$ E. v E. reg E. r ( + splitBits ((1, v) : (3, 3) : (4, 8) : 0) b /\ + readModRM rex reg r l /\ + ast = xastXchg (opSizeW rex v) r reg) $; +theorem decodeXchgT (rex ast b l: nat): + $ decodeXchg rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeXchgRAX (rex ast b l .v .reg .r: nat): wff = +$ l = 0 /\ E. r ( + splitBits ((3, r) : (1, 0) : (4, 9) : 0) b /\ + ast = xastXchg (opSizeW rex 1) (RM_reg RAX) (rex_reg (REX_B rex) r)) $; +theorem decodeXchgRAX_T (rex ast b l: nat): + $ decodeXchgRAX rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeCDX (rex ast b l .reg .r: nat): wff = +$ E. reg E. r (b = ch x9 x9 /\ l = 0 /\ ast = xastCDX (opSize T. (REX_W rex) 1)) $; +theorem decodeCDX_T (rex ast b l: nat): + $ decodeCDX rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeLea (rex ast b l .reg .r: nat): wff = +$ E. reg E. r (b = ch x8 xd /\ + readModRM rex reg r l /\ RM_isMem r /\ + ast = xastLea (opSize T. (REX_W rex) 1) (R_rm reg r)) $; +theorem decodeLeaT (rex ast b l: nat): + $ decodeLea rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeTest (rex ast b l .v .reg .r: nat): wff = +$ E. v E. reg E. r ( + splitBits ((1, v) : (3, 2) : (4, 8) : 0) b /\ + readModRM rex reg r l /\ + ast = xastBinop binopTst (opSizeW rex v) (Rm_r r reg)) $; +theorem decodeTestT (rex ast b l: nat): + $ decodeTest rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeTestRAX (rex ast b l .v .imm .sz: nat): wff = +$ E. v E. imm E. sz ( + splitBits ((1, v) : (3, 4) : (4, 10) : 0) b /\ + sz = opSize T. (REX_W rex) v /\ + readImm sz imm l /\ + ast = xastBinop binopTst sz (Rm_i (RM_reg RAX) imm)) $; +theorem decodeTestRAX_T (rex ast b l: nat): + $ decodeTestRAX rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeCMC (_rex ast b l: nat): wff = $ b = ch xf x5 /\ l = 0 /\ ast = xastCMC $; +theorem decodeCMC_T (rex ast b l: nat): $ decodeCMC rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; +def decodeCLC (_rex ast b l: nat): wff = $ b = ch xf x8 /\ l = 0 /\ ast = xastCLC $; +theorem decodeCLC_T (rex ast b l: nat): $ decodeCLC rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; +def decodeSTC (_rex ast b l: nat): wff = $ b = ch xf x9 /\ l = 0 /\ ast = xastSTC $; +theorem decodeSTC_T (rex ast b l: nat): $ decodeSTC rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeFlag (rex ast b l: nat): wff = +$ decodeCMC rex ast b l \/ decodeCLC rex ast b l \/ decodeSTC rex ast b l $; +theorem decodeFlagT (rex ast b l: nat): + $ decodeFlag rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeMisc (rex ast b l: nat): wff = +$ decodeXchg rex ast b l \/ decodeXchgRAX rex ast b l \/ + decodeTest rex ast b l \/ decodeTestRAX rex ast b l \/ + decodeCDX rex ast b l \/ decodeLea rex ast b l \/ decodeFlag rex ast b l $; +theorem decodeMiscT (rex ast b l: nat): + $ decodeMisc rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeHiAux (v sz r hi n ast l .imm: nat): wff = +$ ifp (true hi) + (l = 0 /\ ( + n = 0 /\ ast = xastUnop unopInc sz r \/ + n = 1 /\ ast = xastUnop unopDec sz r \/ + true v /\ ( + n = 2 /\ ast = xastCall (immRM_rm r) \/ + n = 4 /\ ast = xastJump r \/ + n = 6 /\ ast = xastPush (immRM_rm r)))) + (n = 0 /\ E. imm (readImm sz imm l /\ + ast = xastBinop binopTst sz (Rm_i r imm)) \/ + l = 0 /\ ( + n = 2 /\ ast = xastUnop unopNot sz r \/ + n = 3 /\ ast = xastUnop unopNeg sz r \/ + n = 4 /\ ast = xastMul sz r \/ + n = 6 /\ ast = xastDiv sz r)) $; +theorem decodeHiAuxT (v sz r hi n ast l: nat): + $ sz e. WSize /\ r e. RM /\ + decodeHiAux v sz r hi n ast l -> ast e. XAST /\ l e. List u8 $; + +def decodeHi (rex ast b l .v .x .opc .r .l1 .l2: nat): wff = +$ E. v E. x E. opc E. r E. l1 E. l2 (l = l1 ++ l2 /\ + splitBits ((1, v) : (2, 3) : (1, x) : (4, 15) : 0) b /\ + readOpcodeModRM rex opc r l1 /\ + decodeHiAux v (opSizeW rex v) r x opc ast l2) $; +theorem decodeHiT (rex ast b l: nat): + $ decodeHi rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decodeAux (rex ast b l: nat): wff = +$ decodeBinop rex ast b l \/ decodeMov rex ast b l \/ + decodeStack rex ast b l \/ decodeFlow rex ast b l \/ + decodeMisc rex ast b l \/ decodeHi rex ast b l \/ decodeTwo rex ast b l $; +theorem decodeAuxT (rex ast b l: nat): + $ decodeAux rex ast b l -> ast e. XAST /\ b e. u8 /\ l e. List u8 $; + +def decode (ast l .rex .l1 .opc .l2: nat): wff = +$ E. rex E. l1 E. opc E. l2 (l = l1 ++ opc : l2 /\ + readPrefixes rex l1 /\ decodeAux rex ast opc l2) /\ + len l <= 15 $; +theorem decodeT (ast l: nat): + $ decode ast l -> ast e. XAST /\ l e. List u8 $; + +---------------------------------------- +-- Dynamic semantics +---------------------------------------- + +def Flags: nat = $ u64 $; +def CF (flags: nat): wff = $ 0 e. flags $; +def ZF (flags: nat): wff = $ 6 e. flags $; +def SF (flags: nat): wff = $ 7 e. flags $; +def OF (flags: nat): wff = $ 11 e. flags $; + +def setCF (f: nat) (p: wff): nat = $ bitsUpdate 0 1 (nat p) f $; +def setZF (f: nat) (p: wff): nat = $ bitsUpdate 6 1 (nat p) f $; +def setSF (f: nat) (p: wff): nat = $ bitsUpdate 7 1 (nat p) f $; +def setOF (f: nat) (p: wff): nat = $ bitsUpdate 11 1 (nat p) f $; +theorem setCF_T (f: nat) (p: wff): $ f e. Flags -> setCF f p e. Flags $; +theorem setZF_T (f: nat) (p: wff): $ f e. Flags -> setZF f p e. Flags $; +theorem setSF_T (f: nat) (p: wff): $ f e. Flags -> setSF f p e. Flags $; +theorem setOF_T (f: nat) (p: wff): $ f e. Flags -> setOF f p e. Flags $; + +def readBCond (f c: nat): wff; +theorem readBCondO (f: nat): $ readBCond f bcondO <-> OF f $; +theorem readBCondB (f: nat): $ readBCond f bcondB <-> CF f $; +theorem readBCondE (f: nat): $ readBCond f bcondE <-> ZF f $; +theorem readBCondNA (f: nat): $ readBCond f bcondNA <-> CF f \/ ZF f $; +theorem readBCondS (f: nat): $ readBCond f bcondS <-> SF f $; +theorem readBCondL (f: nat): $ readBCond f bcondL <-> ~(SF f <-> OF f) $; +theorem readBCondNG (f: nat): $ readBCond f bcondNG <-> ZF f \/ ~(SF f <-> OF f) $; + +def readCondF (f c: nat): wff; +theorem readCondFAlways (f: nat): $ readCondF f condAlways $; +theorem readCondFPos (f c: nat): $ readCondF f (condPos c) <-> readBCond f c $; +theorem readCondFNeg (f c: nat): $ readCondF f (condNeg c) <-> ~readBCond f c $; + +def Prot: set = $ Bits 3 $; +theorem finiteProt: $ finite Prot $; +def PROT_READ: nat = $ 1 $; +def PROT_WRITE: nat = $ 2 $; +def PROT_EXEC: nat = $ 4 $; +theorem PROT_READ_T: $ PROT_READ e. Prot $; +theorem PROT_WRITE_T: $ PROT_WRITE e. Prot $; +theorem PROT_EXEC_T: $ PROT_EXEC e. Prot $; + +def Memory: set = $ Arrow u64 (Xp Prot u8) $; +theorem finiteMemory: $ finite Memory $; + +def Exception: set = $ upto 3 $; +theorem finiteException: $ finite Exception $; +--| Represents the 'syscall' function +def exSysCall: nat = $ 0 $; +--| General protection fault, issued on invalid read/write +def exGPF: nat = $ 1 $; +--| Undefined instruction, issued on ud2 instruction +def exUD: nat = $ 2 $; +theorem exSysCallT: $ exSysCall e. Exception $; +theorem exGPF_T: $ exGPF e. Exception $; +theorem exUD_T: $ exUD e. Exception $; + +--| ``` +--| data Config = { +--| ex: Option Exception, -- nonnull if we are going to do IO on the next step +--| rip: u64, -- the intruction pointer +--| regs: Regs -> u64, -- the 16 general purpose registers +--| flags: Flags, -- the flags CF, ZF, SF, OF +--| mem: u64 -> Prot * u8 } -- the virtual memory +--| ``` +def Config: set = $ Xp (Xp (Option Exception) u64) (Xp (Arrow Regs u64) (Xp Flags Memory)) $; +theorem finiteConfig: $ finite Config $; +def mkCfg (ex rip regs flags mem: nat): nat = $ (ex, rip), regs, flags, mem $; +theorem mkCfgT (ex rip regs flags mem: nat): + $ mkCfg ex rip regs flags mem e. Config <-> + ex e. Option Exception /\ rip e. u64 /\ regs e. Arrow Regs u64 /\ + flags e. Flags /\ mem e. Memory $; + +def readException (k: nat): nat = $ pi11 k $; +def readRIP (k: nat): nat = $ pi12 k $; +def readReg (k r: nat): nat = $ pi21 k @ r $; +def readFlags (k: nat): nat = $ pi221 k $; +def getMemory (k: nat): nat = $ pi222 k $; +def readCond (k c: nat): wff = $ readCondF (readFlags k) c $; + +theorem readExceptionT (k: nat): $ k e. Config -> readException k e. Option Exception $; +theorem readRIP_T (k: nat): $ k e. Config -> readRIP k e. u64 $; +theorem readRegT (k r: nat): $ k e. Config /\ r e. Regs -> readReg k r e. u64 $; +theorem readFlagsT (k: nat): $ k e. Config -> readFlags k e. Flags $; +theorem getMemoryT (k: nat): $ k e. Config -> getMemory k e. Memory $; + +def readMemory1 (ps m a b .prot: nat): wff = +$ m e. Memory /\ a e. u64 /\ E. prot (m @ a = prot, b /\ ps C_ prot) $; +theorem readMemory1T (ps m a b: nat): + $ readMemory1 ps m a b -> ps e. Prot /\ m e. Memory /\ a e. u64 /\ b e. u8 $; + +def readMemory (ps m a l: nat): wff; +theorem readMemory0 (ps m a: nat): + $ readMemory ps m a 0 <-> ps e. Prot /\ m e. Memory /\ a e. u64 $; +theorem readMemoryS (ps m a b l: nat): + $ readMemory ps m a (b : l) <-> + readMemory1 ps m a b /\ readMemory ps m (a +_64 1) l $; +theorem readMemoryT (ps m a l: nat): + $ readMemory ps m a l -> ps e. Prot /\ m e. Memory /\ a e. u64 /\ l e. List u8 $; + +def readMem (k a l: nat): wff = $ k e. Config /\ readMemory PROT_READ (getMemory k) a l $; +theorem readMemT (k a l: nat): + $ readMem k a l -> k e. Config /\ a e. u64 /\ l e. List u8 $; + +def readMemX (k a l: nat): wff = +$ k e. Config /\ readMemory (PROT_READ + PROT_EXEC) (getMemory k) a l $; +theorem readMemX_T (k a l: nat): + $ readMemX k a l -> k e. Config /\ a e. u64 /\ l e. List u8 $; + +def writeMemory1 (m a b m2 e .prot .b2: nat): wff = +$ m e. Memory /\ a e. u64 /\ b e. u8 /\ + E. prot E. b2 (m @ a = prot, b2 /\ + ifp (PROT_READ + PROT_WRITE C_ prot) + (m2 == write m a (prot, b) /\ e = 0) + (m2 == m /\ e = suc exGPF)) $; +theorem writeMemory1T (m a b m2 e: nat): + $ writeMemory1 m a b m2 e -> + m e. Memory /\ a e. u64 /\ b e. u8 /\ + m2 e. Memory /\ e e. Option Exception $; + +def writeMemory (m a l m2 e: nat): wff; +theorem writeMemory0 (m a m2 e: nat): + $ m e. Memory /\ a e. u64 -> + (writeMemory m a 0 m2 e <-> m2 = m /\ e = 0) $; +theorem writeMemoryS {m2 e1: nat} (m a b l m3 e: nat): + $ m e. Memory /\ a e. u64 /\ b e. u8 /\ l e. List u8 -> + (writeMemory m a (b : l) m3 e <-> + E. m2 E. e1 (writeMemory1 m a b m2 e1 /\ + ifp (e1 = 0) + (writeMemory m2 (a +_64 1) l m3 e) + (m3 = m2 /\ e = e1))) $; +theorem writeMemoryT (m a l m2 e: nat): + $ writeMemory m a l m2 e -> + m e. Memory /\ a e. u64 /\ l e. List u8 /\ + m2 e. Memory /\ e e. Option Exception $; + +def writeMem (k a l k2 .ip .r .f .m .m2 .e: nat): wff = +$ k e. Config /\ a e. u64 /\ l e. List u8 /\ + E. ip E. r E. f E. m E. m2 E. e (writeMemory m a l m2 e /\ + k = mkCfg 0 ip r f m /\ k2 = mkCfg e ip r f m2) $; +theorem writeMemT (k a l k2: nat): + $ writeMem k a l k2 -> k e. Config /\ a e. u64 /\ l e. List u8 /\ k2 e. Config $; + +def EA: set = $ Sum u64 (Sum Regs u64) $; +def EA_i (q: nat): nat = $ b0 q $; +def EA_r (r: nat): nat = $ b1 (b0 r) $; +def EA_m (q: nat): nat = $ b1 (b1 q) $; +theorem EA_iT (q: nat): $ EA_i q e. EA <-> q e. u64 $; +theorem EA_rT (r: nat): $ EA_r r e. EA <-> r e. Regs $; +theorem EA_mT (q: nat): $ EA_m q e. EA <-> q e. u64 $; + +def EA_addr (ea: nat): nat; +theorem EA_addrm (a: nat): $ EA_addr (EA_m a) = a $; +theorem EA_addr0 {a: nat} (ea: nat): $ ~(E. a ea = EA_m a) -> EA_addr ea = 0 $; +theorem EA_addrT (ea: nat): $ ea e. EA -> EA_addr ea e. u64 $; + +def readIndex (k si: nat): nat; +theorem readIndex0 (k: nat): $ readIndex k 0 = 0 $; +theorem readIndexS (k sc r: nat): + $ readIndex k (suc (sc, r)) = chop 64 (shl (readReg k r) sc) $; +theorem readIndexT (k si: nat): + $ k e. Config /\ si e. Option ScaleIndex -> readIndex k si e. u64 $; + +def readBase (k b: nat): nat; +theorem readBase0 (k: nat): $ readBase k 0 = 0 $; +theorem readBaseRIP (k: nat): $ readBase k base_RIP = readRIP k $; +theorem readBaseReg (k r: nat): $ readBase k (base_reg r) = readReg k r $; +theorem readBaseT (k b: nat): + $ k e. Config /\ b e. Base -> readBase k b e. u64 $; + +def RM_EA (k rm: nat): nat; +theorem RM_EAreg (k r: nat): $ RM_EA k (RM_reg r) = EA_r r $; +theorem RM_EAmem (k si base q: nat): $ RM_EA k (RM_mem si base q) = + EA_m (readIndex k si +_64 readBase k base +_64 q) $; +theorem RM_EA_T (k rm: nat): + $ k e. Config /\ rm e. RM -> RM_EA k rm e. EA $; + +def immRM_EA (k irm: nat): nat; +theorem immRM_EArm (k rm: nat): $ immRM_EA k (immRM_rm rm) = RM_EA k rm $; +theorem immRM_EAimm (k q: nat): $ immRM_EA k (immRM_imm q) = EA_i q $; +theorem immRM_EA_T (k irm: nat): + $ k e. Config /\ irm e. ImmRM -> immRM_EA k irm e. EA $; + +def destEA (k ds: nat): nat; +theorem destEAm_i (k v q: nat): $ destEA k (Rm_i v q) = RM_EA k v $; +theorem destEAm_r (k v r: nat): $ destEA k (Rm_r v r) = RM_EA k v $; +theorem destEA_rm (k r rm: nat): $ destEA k (R_rm r rm) = EA_r r $; +theorem destEA_T (k ds: nat): + $ k e. Config /\ ds e. DestSrc -> destEA k ds e. EA $; + +def srcEA (k ds: nat): nat; +theorem srcEAm_i (k v q: nat): $ srcEA k (Rm_i v q) = EA_i q $; +theorem srcEAm_r (k v r: nat): $ srcEA k (Rm_r v r) = EA_r r $; +theorem srcEA_rm (k r rm: nat): $ srcEA k (R_rm r rm) = RM_EA k rm $; +theorem srcEA_T (k ds: nat): + $ k e. Config /\ ds e. DestSrc -> srcEA k ds e. EA $; + +def readRegSz (k sz r: nat): nat = +$ chop (wsizeBits sz) + (if (sz = wSz8 F. /\ 2 e. r) (shr (readReg k (r - 4)) 8) (readReg k r)) $; +theorem readRegSzT (k sz r: nat): + $ k e. Config /\ sz e. WSize /\ r e. Regs -> + readRegSz k sz r e. Bits (wsizeBits sz) $; + +def readEA (k sz ea v: nat): wff; +theorem readEA_i (k q sz v: nat): + $ k e. Config /\ q e. u64 /\ sz e. WSize -> + (readEA k sz (EA_i q) v <-> v = chop (wsizeBits sz) q) $; +theorem readEA_r (k sz r v: nat): + $ k e. Config /\ r e. Regs /\ sz e. WSize -> + (readEA k sz (EA_r r) v <-> v = readRegSz k sz r) $; +theorem readEA_m (k a sz v: nat): + $ k e. Config /\ a e. u64 /\ sz e. WSize -> + (readEA k sz (EA_m a) v <-> + v e. Bits (wsizeBits sz) /\ readMem k a (toBytes (wsizeBytes sz) v)) $; +theorem readEA_T (k sz ea v: nat): $ readEA k sz ea v -> + k e. Config /\ ea e. EA /\ sz e. WSize /\ v e. Bits (wsizeBits sz) $; + +def readEA64 (k ea v: nat): wff = $ readEA k wSz64 ea v $; +theorem readEA64T (k ea v: nat): $ readEA64 k ea v -> + k e. Config /\ ea e. EA /\ v e. u64 $; + +def setException (k e: nat): nat; +theorem setExceptionVal (ex ip rs f m e: nat): + $ setException (mkCfg ex ip rs f m) e = mkCfg e ip rs f m $; +theorem setExceptionT (k e: nat): + $ k e. Config /\ e e. Option Exception -> setException k e e. Config $; + +def setReg (k r q: nat): nat; +theorem setRegVal (ex ip rs f m r q: nat): + $ setReg (mkCfg ex ip rs f m) r q = mkCfg ex ip (lower (write rs r q)) f m $; +theorem setRegT (k r q: nat): + $ k e. Config /\ r e. Regs /\ q e. u64 -> setReg k r q e. Config $; + +def writeReg (k sz r v: nat): nat; +theorem writeReg8 (k r v: nat) (have_rex: wff): + $ writeReg k (wSz8 have_rex) r v = if (~have_rex /\ 2 e. r) + (setReg k (r - 4) (bitsUpdate 8 8 v (readReg k (r - 4)))) + (setReg k r (bitsUpdate 0 8 v (readReg k r))) $; +theorem writeReg16 (k r v: nat): + $ writeReg k wSz16 r v = setReg k r (bitsUpdate 0 16 v (readReg k r)) $; +theorem writeReg32 (k r v: nat): $ writeReg k wSz32 r v = setReg k r v $; +theorem writeReg64 (k r v: nat): $ writeReg k wSz64 r v = setReg k r v $; +theorem writeRegT (k sz r v: nat): $ k e. Config /\ sz e. WSize /\ + r e. Regs /\ v e. Bits (wsizeBits sz) -> writeReg k sz r v e. Config $; + +def writeEASz (k sz ea v k2: nat): wff; +theorem writeEASz_i (k sz i v k2: nat): $ ~ writeEASz k sz (EA_i i) v k2 $; +theorem writeEASz_r (k sz r v k2: nat): + $ k e. Config /\ sz e. WSize /\ r e. Regs /\ v e. Bits (wsizeBits sz) -> + (writeEASz k sz (EA_r r) v k2 <-> k2 = writeReg k sz r v) $; +theorem writeEASz_m (k sz a v k2: nat): + $ k e. Config /\ sz e. WSize /\ a e. u64 /\ v e. Bits (wsizeBits sz) -> + (writeEASz k sz (EA_m a) v k2 <-> + writeMem k a (toBytes (wsizeBits sz) v) k2) $; +theorem writeEASzT (k sz ea v k2: nat): + $ writeEASz k sz ea v k2 -> + k e. Config /\ sz e. WSize /\ ea e. EA /\ v e. Bits (wsizeBits sz) /\ + k2 e. Config $; + +def writeEA (k sz ea v k2: nat): wff = +$ v e. u64 /\ writeEASz k sz ea (chop (wsizeBits sz) v) k2 $; +theorem writeEA_T (k sz ea v k2: nat): + $ writeEA k sz ea v k2 -> + k e. Config /\ sz e. WSize /\ ea e. EA /\ v e. u64 /\ + k2 e. Config $; + +def writeRIP (k q: nat): nat; +theorem writeRIPVal (ex ip rs f m q: nat): + $ writeRIP (mkCfg ex ip rs f m) q = mkCfg ex q rs f m $; +theorem writeRIP_T (k q: nat): + $ k e. Config /\ q e. u64 -> writeRIP k q e. Config $; + +def EA_callDest (k ea v: nat): wff; +theorem EA_callDest_i (k i v: nat): + $ k e. Config /\ i e. u64 -> + (EA_callDest k (EA_i i) v <-> v = readRIP k +_64 i) $; +theorem EA_callDest_r (k r v: nat): + $ k e. Config /\ r e. Regs -> + (EA_callDest k (EA_r r) v <-> v = readReg k r) $; +theorem EA_callDest_m (k a v: nat): + $ k e. Config /\ a e. u64 -> + (EA_callDest k (EA_m a) v <-> v e. u64 /\ readMem k a (u64Bytes v)) $; +theorem EA_callDestT (k ea v: nat): + $ EA_callDest k ea v -> k e. Config /\ ea e. EA /\ v e. u64 $; + +def EA_jump (k ea k2 .v: nat): wff = +$ E. v (EA_callDest k ea v /\ k2 = writeRIP k v) $; +theorem EA_jumpT (k ea k2: nat): + $ EA_jump k ea k2 -> k e. Config /\ ea e. EA /\ k2 e. Config $; + +def writeFlags (k f: nat): nat; +theorem writeFlagsVal (ex ip rs f m f2: nat): + $ writeFlags (mkCfg ex ip rs f m) f2 = mkCfg ex ip rs f2 m $; +theorem writeFlagsT (k f: nat): + $ k e. Config /\ f e. Flags -> writeFlags k f e. Config $; + +def setCZSO (k: nat) (c z s o: wff): nat; +theorem setCZSOVal (ex ip rs f m: nat) (c z s o: wff): + $ setCZSO (mkCfg ex ip rs f m) c z s o = + mkCfg ex ip rs (setOF (setSF (setZF (setCF f c) z) s) o) m $; +theorem setCZSO_T (k: nat) (c z s o: wff): + $ k e. Config -> setCZSO k c z s o e. Config $; + +def MSB (sz w: nat): wff = $ bitsMSB (wsizeBits sz) w $; + +def writeResultFlags (k sz w: nat) (c o: wff): nat = +$ setCZSO k c (chop (wsizeBits sz) w = 0) (MSB sz w) o $; +theorem writeResultFlagsT (k sz w: nat) (c o: wff): + $ k e. Config /\ sz e. WSize /\ w e. u64 -> + writeResultFlags k sz w c o e. Config $; + +def eraseFlags (k k2 .f2: nat): wff = +$ k e. Config /\ E. f2 (f2 e. Flags /\ k2 = writeFlags k f2) $; +theorem eraseFlagsT (k k2: nat): + $ eraseFlags k k2 -> k e. Config /\ k2 e. Config $; + +def addCarry (sz a b w c o: nat): wff = +$ sz e. WSize /\ a e. u64 /\ b e. u64 /\ + w = a +_64 b /\ c = nat (2 ^ wsizeBits sz <= a + b) /\ + o = nat ((MSB sz a <-> MSB sz b) /\ ~(MSB sz (a +_64 b) <-> MSB sz a)) $; +theorem addCarryT (sz a b w c o: nat): + $ addCarry sz a b w c o -> + sz e. WSize /\ a e. u64 /\ b e. u64 /\ + w e. u64 /\ bool c /\ bool o $; + +def subBorrow (sz a b w c o: nat): wff = +$ sz e. WSize /\ a e. u64 /\ b e. u64 /\ + w = a -_64 b /\ c = nat (a < b) /\ + o = nat (~(MSB sz a <-> MSB sz b) /\ ~(MSB sz (a -_64 b) <-> MSB sz a)) $; +theorem subBorrowT (sz a b w c o: nat): + $ subBorrow sz a b w c o -> + sz e. WSize /\ a e. u64 /\ b e. u64 /\ + w e. u64 /\ bool c /\ bool o $; + +def writeCFOFResult (k sz ea w: nat) (c o: wff) (k2: nat): wff = +$ k e. Config /\ writeEA (writeResultFlags k sz w c o) sz ea w k2 $; +theorem writeCFOFResultT (k sz ea w: nat) (c o: wff) (k2: nat): + $ writeCFOFResult k sz ea w c o k2 -> + k e. Config /\ sz e. WSize /\ ea e. EA /\ w e. u64 /\ + k2 e. Config $; + +def maskShift (sz w: nat): nat = $ chop (if (wsizeBits sz = 64) 6 5) w $; + +def writeBinop (k op sz ea a b k2: nat): wff; +theorem writeBinopAdd {w c o: nat} (k sz ea a b k2: nat): + $ writeBinop k binopAdd sz ea a b k2 <-> E. w E. c E. o ( + addCarry sz a b w c o /\ + writeCFOFResult k sz ea w (true c) (true o) k2) $; +theorem writeBinopSub {w c o: nat} (k sz ea a b k2: nat): + $ writeBinop k binopSub sz ea a b k2 <-> E. w E. c E. o ( + subBorrow sz a b w c o /\ + writeCFOFResult k sz ea w (true c) (true o) k2) $; +theorem writeBinopCmp {w c o: nat} (k sz ea a b k2: nat): + $ writeBinop k binopCmp sz ea a b k2 <-> E. w E. c E. o ( + subBorrow sz a b w c o /\ + k2 = writeResultFlags k sz w (true c) (true o)) $; +theorem writeBinopOr (k sz ea a b k2: nat): + $ writeBinop k binopOr sz ea a b k2 <-> + writeCFOFResult k sz ea (bitOr a b) F. F. k2 $; +theorem writeBinopAnd (k sz ea a b k2: nat): + $ writeBinop k binopAnd sz ea a b k2 <-> + writeCFOFResult k sz ea (bitAnd a b) F. F. k2 $; +theorem writeBinopXor (k sz ea a b k2: nat): + $ writeBinop k binopXor sz ea a b k2 <-> + writeCFOFResult k sz ea (bitXor a b) F. F. k2 $; +theorem writeBinopTst (k sz ea a b k2: nat): + $ writeBinop k binopTst sz ea a b k2 <-> + k2 = writeResultFlags k sz (bitAnd a b) F. F. $; +theorem writeBinopShl {k3: nat} (k sz ea a b k2: nat): + $ writeBinop k binopShl sz ea a b k2 <-> + E. k3 (eraseFlags k k3 /\ writeEA k3 sz ea (shl a (maskShift sz b)) k2) $; +theorem writeBinopShr {k3: nat} (k sz ea a b k2: nat): + $ writeBinop k binopShr sz ea a b k2 <-> + E. k3 (eraseFlags k k3 /\ writeEA k3 sz ea (shr a (maskShift sz b)) k2) $; +theorem writeBinopSar {k3: nat} (k sz ea a b k2: nat): + $ writeBinop k binopSar sz ea a b k2 <-> + E. k3 (eraseFlags k k3 /\ + writeEA k3 sz ea (bitsSar (wsizeBits sz) a (maskShift sz b)) k2) $; +theorem writeBinopAdc (k sz ea a b k2: nat): $ ~ writeBinop k binopAdc sz ea a b k2 $; +theorem writeBinopSbb (k sz ea a b k2: nat): $ ~ writeBinop k binopSbb sz ea a b k2 $; +theorem writeBinopRol (k sz ea a b k2: nat): $ ~ writeBinop k binopRol sz ea a b k2 $; +theorem writeBinopRor (k sz ea a b k2: nat): $ ~ writeBinop k binopRor sz ea a b k2 $; +theorem writeBinopRcl (k sz ea a b k2: nat): $ ~ writeBinop k binopRcl sz ea a b k2 $; +theorem writeBinopRcr (k sz ea a b k2: nat): $ ~ writeBinop k binopRcr sz ea a b k2 $; +theorem writeBinopT (k op sz ea a b k2: nat): + $ k e. Config /\ op e. Binop /\ sz e. WSize /\ a e. u64 /\ b e. u64 /\ + ea e. EA /\ writeBinop k op sz ea a b k2 -> k2 e. Config $; + +def writeUnop (k op sz ea a k2: nat): wff; +theorem writeUnopInc {w c o: nat} (k sz ea a k2: nat): + $ writeUnop k unopInc sz ea a k2 <-> E. w E. c E. o ( + addCarry sz a 1 w c o /\ + writeCFOFResult k sz ea w (CF (readFlags k)) (true o) k2) $; +theorem writeUnopDec {w c o: nat} (k sz ea a k2: nat): + $ writeUnop k unopDec sz ea a k2 <-> E. w E. c E. o ( + subBorrow sz a 1 w c o /\ + writeCFOFResult k sz ea w (CF (readFlags k)) (true o) k2) $; +theorem writeUnopNot (k sz ea a k2: nat): + $ writeUnop k unopNot sz ea a k2 <-> + writeEA k sz ea (bitsNot (wsizeBits sz) a) k2 $; +theorem writeUnopNeg {b: nat} (k sz ea a k2: nat): + $ writeUnop k unopNeg sz ea a k2 <-> + E. b (b = bitsNeg (wsizeBits sz) a /\ + writeCFOFResult k sz ea b (a != 0) (MSB sz a /\ ~MSB sz b) k2) $; +theorem writeUnopT (k op sz ea a k2: nat): + $ k e. Config /\ op e. Unop /\ sz e. WSize /\ a e. u64 /\ + ea e. EA /\ writeUnop k op sz ea a k2 -> k2 e. Config $; + +def popAux (k q k2: nat): wff = +$ readEA64 k (EA_m (readReg k RSP)) q /\ + k2 = setReg k RSP (readReg k RSP +_64 8) $; +theorem popAuxT (k q k2: nat): + $ popAux k q k2 -> k e. Config /\ q e. u64 /\ k2 e. Config $; + +def popWrite (k rm k3 .q .k2: nat): wff = +$ rm e. RM /\ E. k2 E. q (popAux k q k2 /\ writeEA k2 wSz64 (RM_EA k2 rm) q k3) $; +theorem popWriteT (k rm k2: nat): + $ popWrite k rm k2 -> k e. Config /\ rm e. RM /\ k2 e. Config $; + +def popRIP (k k3 .q .k2: nat): wff = +$ E. k2 E. q (popAux k q k2 /\ k3 = writeRIP k2 q) $; +theorem popRIP_T (k k2: nat): + $ popRIP k k2 -> k e. Config /\ k2 e. Config $; + +def pushAux (k q k2 .sp: nat): wff = +$ k e. Config /\ + E. sp (sp = readReg k RSP -_64 8 /\ + writeEA (setReg k RSP sp) (EA_m sp) wSz64 q k2) $; +theorem pushAuxT (k q k2: nat): + $ pushAux k q k2 -> k e. Config /\ q e. u64 /\ k2 e. Config $; + +def pushImmRM (k irm k2 .q: nat): wff = +$ irm e. ImmRM /\ E. q (readEA64 k (immRM_EA k irm) q /\ pushAux k q k2) $; +theorem pushImmRM_T (k irm k2: nat): + $ pushImmRM k irm k2 -> k e. Config /\ irm e. ImmRM /\ k2 e. Config $; + +def pushRIP (k k2: nat): wff = $ pushAux k (readRIP k) k2 $; +theorem pushRIP_T (k k2: nat): + $ pushRIP k k2 -> k e. Config /\ k2 e. Config $; + +def divModSz (sz a b d m: nat): wff = +$ b != 0 /\ d e. Bits (wsizeBits sz) /\ d = a // b /\ m = a % b $; + +def execXAST (k ast k2: nat): wff; +theorem execXASTUnop {q: nat} (k op sz rm k2: nat): + $ execXAST k (xastUnop op sz rm) k2 <-> E. q ( + readEA k sz (RM_EA k rm) q /\ + writeUnop k op sz (RM_EA k rm) q k2) $; +theorem execXASTBinop {d s: nat} (k op sz ds k2: nat): + $ execXAST k (xastBinop op sz ds) k2 <-> E. d E. s ( + readEA k sz (destEA k ds) d /\ + readEA k sz (srcEA k ds) s /\ + writeBinop k op sz (destEA k ds) d s k2) $; +theorem execXASTMul {n src res lo hi: nat} (k sz rm k2: nat): + $ execXAST k (xastMul sz rm) k2 <-> E. n E. src E. res ( + n = wsizeBits sz /\ + readEA k sz (RM_EA k rm) src /\ + res = readRegSz k sz RAX * src /\ + ifp (n = 8) + (k2 = writeReg k wSz16 RAX res) + (E. lo E. hi ( + splitBits ((n, lo) : (n, hi) : 0) res /\ + k2 = writeReg (writeReg k sz RAX lo) sz RDX hi))) $; +theorem execXASTDiv {n a b d m: nat} (k sz rm k2: nat): + $ execXAST k (xastDiv sz rm) k2 <-> E. n E. a E. b E. d E. m ( + n = wsizeBits sz /\ + readEA k sz (RM_EA k rm) b /\ + divModSz sz a b d m /\ + ifp (n = 8) + (a = readRegSz k wSz16 RAX /\ + eraseFlags (writeReg k sz RAX (shl m 8 + d)) k2) + (splitBits ((n, readRegSz k sz RAX) : + (n, readRegSz k sz RDX) : 0) a /\ + eraseFlags (writeReg (writeReg k sz RAX d) sz RDX m) k2)) $; +theorem execXASTCDX {n src lo hi: nat} (k sz k2: nat): + $ execXAST k (xastCDX sz) k2 <-> E. n E. src E. lo E. hi ( + n = wsizeBits sz /\ n != 8 /\ + lo = readRegSz k sz RAX /\ + splitBits ((n, lo) : (n, hi) : 0) (sExt n (2 * n) lo) /\ + k2 = writeReg k sz RDX hi) $; +theorem execXASTLea (k sz ds k2: nat): + $ execXAST k (xastLea sz ds) k2 <-> + writeEA k sz (destEA k ds) (EA_addr (srcEA k ds)) k2 $; +theorem execXASTMovZX {src: nat} (k sz ds sz2 k2: nat): + $ execXAST k (xastMovZX sz ds sz2) k2 <-> E. src ( + readEA k sz (srcEA k ds) src /\ + writeEA k sz2 (destEA k ds) src k2) $; +theorem execXASTMovSX {src: nat} (k sz ds sz2 k2: nat): + $ execXAST k (xastMovSX sz ds sz2) k2 <-> E. src ( + readEA k sz (srcEA k ds) src /\ + writeEA k sz2 (destEA k ds) + (sExt (wsizeBits sz) (wsizeBits sz2) src) k2) $; +theorem execXASTXchg {v: nat} (k sz rm r k2: nat): + $ execXAST k (xastXchg sz rm r) k2 <-> E. v ( + readEA k sz (RM_EA k rm) v /\ + writeEA (writeReg k sz r v) sz (RM_EA k rm) (readRegSz k sz r) k2) $; +theorem execXASTCmpXchg {src acc dst ki: nat} (k sz rm r k2: nat): + $ execXAST k (xastCmpXchg sz rm r) k2 <-> E. src E. acc E. dst E. ki ( + acc = readRegSz k sz RAX /\ + readEA k sz (RM_EA k rm) dst /\ + writeBinop k binopCmp sz (EA_r r) acc dst ki /\ + ifp (acc = dst) + (writeEA ki sz (RM_EA k rm) (readRegSz k sz r) k2) + (writeEA ki sz (EA_r RAX) dst k2)) $; +theorem execXASTXadd {v: nat} (k sz rm r k2: nat): + $ execXAST k (xastXadd sz rm r) k2 <-> E. v ( + readEA k sz (RM_EA k rm) v /\ + writeBinop k binopAdd sz (RM_EA k rm) (readRegSz k sz r) v k2) $; +theorem execXASTCMov {v: nat} (k c sz ds k2: nat): + $ execXAST k (xastCMov c sz ds) k2 <-> E. v ( + readEA k sz (if (readCond k c) (srcEA k ds) (destEA k ds)) v /\ + writeEA k sz (destEA k ds) v k2) $; +theorem execXASTSetCC (k c b rm k2: nat): + $ execXAST k (xastSetCC c b rm) k2 <-> + writeEA k (wSz8 (true b)) (RM_EA k rm) (nat (readCond k c)) k2 $; +theorem execXASTJump {v: nat} (k rm k2: nat): + $ execXAST k (xastJump rm) k2 <-> E. v ( + readEA k wSz64 (RM_EA k rm) v /\ k2 = writeRIP k v) $; +theorem execXASTJCC (k c q k2: nat): + $ execXAST k (xastJCC c q) k2 <-> + k2 = if (readCond k c) (writeRIP k (readRIP k +_64 q)) k $; +theorem execXASTCall {ki: nat} (k irm k2: nat): + $ execXAST k (xastCall irm) k2 <-> E. ki ( + pushRIP k ki /\ EA_jump ki (immRM_EA k irm) k2) $; +theorem execXASTRet {ki: nat} (k q k2: nat): + $ execXAST k (xastRet q) k2 <-> E. ki ( + popRIP k ki /\ k2 = setReg ki RSP (readReg ki RSP +_64 q)) $; +theorem execXASTLeave (k k2: nat): + $ execXAST k xastLeave k2 <-> + popWrite (setReg k RSP (readReg k RBP)) (RM_reg RBP) k2 $; +theorem execXASTPush (k irm k2: nat): + $ execXAST k (xastPush irm) k2 <-> pushImmRM k irm k2 $; +theorem execXASTPop (k rm k2: nat): + $ execXAST k (xastPop rm) k2 <-> popWrite k rm k2 $; +theorem execXASTCMC (k k2: nat): + $ execXAST k xastCMC k2 <-> + k2 = writeFlags k (setCF (readFlags k) (~ (CF (readFlags k)))) $; +theorem execXASTCLC (k k2: nat): + $ execXAST k xastCLC k2 <-> k2 = writeFlags k (setCF (readFlags k) F.) $; +theorem execXASTSTC (k k2: nat): + $ execXAST k xastSTC k2 <-> k2 = writeFlags k (setCF (readFlags k) T.) $; +theorem execXASTUD2 (k k2: nat): + $ execXAST k xastUD2 k2 <-> k2 = setException k (suc exUD) $; +theorem execXASTSysCall {r11: nat} (k k2: nat): + $ execXAST k xastSysCall k2 <-> E. r11 (r11 e. u64 /\ + k2 = setException (setReg (setReg k RCX (readRIP k)) 11 r11) (suc exSysCall)) $; + +theorem execXAST_T (k ast k2: nat): + $ k e. Config /\ ast e. XAST /\ execXAST k ast k2 -> k2 e. Config $; + +--| This is the step relation for the x86 semantic model, excluding IO. +--| `step k k2` means that k2 is a possible next state after k. Multiple +--| next states may exist in the case of undefined/nondeterministic behavior, +--| and no next states means the state is either invalid or an IO call. +def step (k k2 .l .ast: nat): wff = +$ k e. Config /\ readException k = 0 /\ E. l E. ast ( + readMemX k (readRIP k) l /\ + decode ast l /\ + execXAST (writeRIP k (readRIP k +_64 len l)) ast k2) $; +theorem stepT (k k2: nat): $ step k k2 -> k e. Config /\ k2 e. Config $; + +---------------------------------------- +-- IO semantics +---------------------------------------- + +def PageMapping (M .m .a .p .v: nat): set = +$ {m | m e. Arrow u64 (Option Prot) /\ + A. a A. p (a, suc p e. m -> E. v M @ a = p, v)} $; + +-- Now we model enough of the Linux kernel to interpret a few IO system calls. + +def KernelState {.k: nat}: set = +$ Xp (Xp (List u8) (List u8)) (X\ k e. Config, PageMapping (getMemory k)) $; +def mkKS (i o k m: nat): nat = $ (i, o), k, m $; +theorem mkKS_T (i o k m: nat): + $ mkKS i o k m e. KernelState <-> + i e. List u8 /\ o e. List u8 /\ k e. Config /\ m e. PageMapping (getMemory k) $; + +def ksIn (k: nat): nat = $ pi11 k $; +def ksOut (k: nat): nat = $ pi12 k $; +def ksCfg (k: nat): nat = $ pi21 k $; +def ksMapping (k: nat): nat = $ pi22 k $; +theorem ksInT (k: nat): $ k e. KernelState -> ksIn k e. List u8 $; +theorem ksOutT (k: nat): $ k e. KernelState -> ksOut k e. List u8 $; +theorem ksCfgT (k: nat): $ k e. KernelState -> ksCfg k e. Config $; +theorem ksMappingT (k: nat): + $ k e. KernelState -> ksMapping k e. PageMapping (getMemory (ksCfg k)) $; + +def writeMapping (ks k2 m2 ks2: nat): wff = +$ ks e. KernelState /\ k2 e. Config /\ m2 e. PageMapping (getMemory k2) /\ + ks2 = mkKS (ksIn ks) (ksOut ks) k2 m2 $; +theorem writeMappingT (ks m k ks2: nat): + $ writeMapping ks k m ks2 -> + ks e. KernelState /\ k e. Config /\ + m e. PageMapping (getMemory k) /\ ks2 e. KernelState $; + +def writeCfg (ks k2 ks2: nat): wff = +$ writeMapping ks k2 (ksMapping ks) ks2 $; +theorem writeCfgT (ks k ks2: nat): + $ writeCfg ks k ks2 -> ks e. KernelState /\ k e. Config /\ ks2 e. KernelState $; + +def stdin: nat = $ 0 $; +def stdout: nat = $ 1 $; + +def isIOError (n: nat): wff = $ n e. u64 /\ bitsNeg 64 (2 ^ 12) < n $; +theorem isIOErrorT (n: nat): $ isIOError n -> n e. u64 $; + +def toCStr (s l .c: nat): wff = $ all {c | c != 0} s /\ l = s |> 0 $; +theorem toCStrT (s l: nat): + $ toCStr s l -> (s e. List u8 <-> l e. List u8) $; + +def readCStr (k a s .l: nat): wff = $ E. l (toCStr s l /\ readMem k a l) $; +theorem readCStrT (k a s: nat): + $ readCStr k a s -> k e. Config /\ a e. u64 /\ s e. List u8 $; + +def O_RDONLY: nat = $ 0 $; +def O_WRONLY: nat = $ 1 $; +def O_CREAT: nat = $ shl 1 6 $; +def O_TRUNC: nat = $ shl 1 9 $; + +def sys_open: nat = $ 2 $; +def execOpen (k ret .filename .flags: nat): wff = +$ k e. Config /\ readReg k RAX = sys_open /\ + E. filename E. flags ( + readCStr k (readReg k RDI) filename /\ + flags = readReg k RSI /\ readReg k RDX = 0 /\ + (flags = O_RDONLY \/ flags = O_WRONLY + O_CREAT + O_TRUNC) /\ + ret e. u64) $; +theorem execOpenT (k ret: nat): + $ execOpen k ret -> k e. Config /\ ret e. u64 $; + +--| If `fd` is the tracked file descriptor, reading/writing `l1` from `fd` +--| results in the accumulated input.output `l2`. +def extendIfFD (tgt fd l l1 l2: nat): wff = +$ l e. List u8 /\ l1 e. List u8 /\ l2 = if (fd = tgt) (l ++ l1) l $; +theorem extendIfFD_T (tgt fd l l1 l2: nat): + $ extendIfFD tgt fd l l1 l2 -> l e. List u8 /\ l1 e. List u8 /\ l2 e. List u8 $; + +def sys_read: nat = $ 0 $; +def execRead (l k l2 k2 ret .fd .buf .count .l1: nat): wff = +$ l e. List u8 /\ readReg k RAX = sys_read /\ + E. fd E. buf E. count (readReg k RDI = fd /\ + readMem k (readReg k RSI) buf /\ buf e. Array u8 count /\ + count = readReg k RDX /\ + ifp (isIOError ret) + (l2 = l /\ k2 = k) + (ret <= count /\ E. l1 (extendIfFD stdin fd l l1 l2 /\ + writeMem k (readReg k RSI) l1 k2))) $; +theorem execReadT (l k l2 k2 ret: nat): + $ execRead l k l2 k2 ret -> + l e. List u8 /\ k e. Config /\ + l2 e. List u8 /\ k2 e. Config /\ ret e. u64 $; +theorem execReadPM (l k l2 k2 ret: nat): + $ execRead l k l2 k2 ret -> + PageMapping (getMemory k) C_ PageMapping (getMemory k2) $; + +def sys_write: nat = $ 1 $; +def execWrite (l k l2 ret .fd .buf .count .l1: nat): wff = +$ l e. List u8 /\ readReg k RAX = sys_write /\ + E. fd E. buf E. count ( + fd = readReg k RDI /\ count = readReg k RDX /\ + readMem k (readReg k RSI) buf /\ buf e. Array u8 count /\ + ifp (isIOError ret) (l2 = l) + (ret <= count /\ E. l1 (extendIfFD stdout fd l l1 l2 /\ + readMem k (readReg k RSI) l1))) $; +theorem execWriteT (l k l2 ret: nat): + $ execWrite l k l2 ret -> + l e. List u8 /\ k e. Config /\ + l2 e. List u8 /\ ret e. u64 $; + +def Stat: set = $ Array u8 (8 * 10) $; +def sys_fstat: nat = $ 5 $; +def execFStat (k k2 ret .fd .stat .stat2: nat): wff = +$ readReg k RAX = sys_fstat /\ E. fd E. stat E. stat2 ( + fd = readReg k RDI /\ fd e. u32 /\ + readMem k (readReg k RSI) stat /\ + stat e. Stat /\ stat2 e. Stat /\ + ret e. u64 /\ writeMem k (readReg k RSI) stat2 k2) $; +theorem execFStatT (k k2 ret: nat): + $ execFStat k k2 ret -> k2 e. Config /\ ret e. u64 $; +theorem execFStatPM (k k2 ret: nat): + $ execFStat k k2 ret -> + PageMapping (getMemory k) C_ PageMapping (getMemory k2) $; + +def mapMemory1 (prot m a b: nat): nat = +$ lower (write (fst m) a (prot, b)), lower (write (snd m) a (suc prot)) $; +theorem mapMemory1T {x: nat} (prot m a b: nat): + $ prot e. Prot /\ m e. X\ x e. Memory, PageMapping x /\ a e. u64 /\ b e. u8 -> + mapMemory1 prot m a b e. X\ x e. Memory, PageMapping x $; + +def mapMemory (prot m a l: nat): nat; +theorem mapMemory0 {x: nat} (prot m a: nat): + $ prot e. Prot /\ m e. X\ x e. Memory, PageMapping x /\ a e. u64 -> + mapMemory prot m a 0 = m $; +theorem mapMemoryS {x: nat} (prot m a b l: nat): + $ prot e. Prot /\ m e. X\ x e. Memory, PageMapping x /\ a e. u64 /\ b e. u8 /\ l e. List u8 -> + mapMemory prot m a (b : l) = + mapMemory prot (mapMemory1 prot m a b) (a +_64 1) l $; +theorem mapMemoryT {x: nat} (prot m a l: nat): + $ prot e. Prot /\ m e. X\ x e. Memory, PageMapping x /\ a e. u64 /\ l e. List u8 -> + mapMemory prot m a l e. X\ x e. Memory, PageMapping x $; + +def mapMem (prot k km a l k2 km2 .e .ip .r .f .m .m2: nat): wff = +$ prot e. Prot /\ k e. Config /\ km e. PageMapping (getMemory k) /\ a e. u64 /\ l e. List u8 /\ + E. e E. ip E. r E. f E. m E. m2 ( + k = mkCfg e ip r f m /\ + mapMemory prot (m, km) a l = m2, km2 /\ + k2 = mkCfg e ip r f m2) $; +theorem mapMemT (prot k km a l k2 km2: nat): + $ mapMem prot k km a l k2 km2 -> + prot e. Prot /\ k e. Config /\ km e. PageMapping (getMemory k) /\ a e. u64 /\ l e. List u8 /\ + k2 e. Config /\ km2 e. PageMapping (getMemory k2) $; + +def sys_mmap: nat = $ 9 $; +def MAP_PRIVATE: nat = $ 2 $; +def MAP_ANONYMOUS: nat = $ 32 $; +def MAP_FAILED: nat = $ bitsNeg 64 1 $; +def execMMap (k m k2 m2 ret .len .prot .flags .fd .off .buf .i: nat): wff = +$ k e. Config /\ m e. PageMapping (getMemory k) /\ + readReg k RAX = sys_mmap /\ E. len E. prot E. flags E. fd E. off ( + readReg k RDI = 0 /\ len = readReg k RSI /\ + prot = readReg k RDX /\ flags = readReg k 10 /\ + fd = readReg k 8 /\ off = readReg k 9 /\ + flags = MAP_PRIVATE + nat (fd = bitsNeg 32 1) * MAP_ANONYMOUS /\ + prot e. Prot /\ off = 0 /\ ret e. u64 /\ + ifp (isIOError ret) (k2 = k /\ m2 = m /\ ret = MAP_FAILED) + (E. buf (buf e. Array u8 len /\ (fd = bitsNeg 32 1 -> all (sn 0) buf) /\ + A. i (i < len -> m @ (ret +_64 i) = 0) /\ + mapMem prot k m ret buf k2 m2))) $; +theorem execMMapT (k m k2 m2 ret: nat): + $ execMMap k m k2 m2 ret -> + k e. Config /\ m e. PageMapping (getMemory k) /\ + k2 e. Config /\ m2 e. PageMapping (getMemory k2) /\ ret e. u64 $; + +def execIO (ks ks2 .i .o .k .m .ret .k2 .k3 .i2 .o2 .m2: nat): wff = +$ E. i E. o E. k E. m E. ret (ks = mkKS i o k m /\ readException k = suc exSysCall /\ + E. k2 E. k3 (k3 = setException (setReg k2 RAX ret) 0 /\ ( + execOpen k ret /\ k2 = k /\ ks2 = mkKS i o k3 m \/ + E. i2 (execRead i k i2 k2 ret /\ ks2 = mkKS i2 o k3 m) \/ + E. o2 (execWrite o k o2 ret /\ k2 = k /\ ks2 = mkKS i o2 k3 m) \/ + execFStat k k2 ret /\ ks2 = mkKS i o k3 m \/ + E. m2 (execMMap k m k2 m2 ret /\ ks2 = mkKS i o k3 m2)))) $; +theorem execIO_T (ks ks2: nat): + $ ks e. KernelState /\ execIO ks ks2 -> ks2 e. KernelState $; + +def sys_exit: nat = $ ch x3 xc $; +--| We consider protection faults as a valid way to exit with a nonzero exit code +--| (usually `0xD` or `0xE` but often reported as `0x8D` and `0x8E` by shells). +def execExit (k ret: nat): wff = +$ k e. Config /\ ret e. u32 /\ ( + readException k = suc exGPF /\ ret != 0 \/ + readException k = suc exSysCall /\ readReg k RAX = sys_exit /\ ret = readReg k RDI) $; +theorem execExitT (k ret: nat): + $ execExit k ret -> k e. Config /\ ret e. u32 $; + +--| This is the composite step relation for the extended state. +--| This mixes regular steps of the machine with IO steps where +--| we hand control to the (POSIX-compliant) Linux kernel and axiomatize +--| the behavior. (We could avoid this, but if we go any lower level than +--| this we won't be able to run the result as a normal program - we will have +--| to replace the bootloader and so on to make a single program OS.) +def ksStep (ks ks2 .k2: nat): wff = +$ ks e. KernelState /\ ( + E. k2 (step (ksCfg ks) k2 /\ writeCfg ks k2 ks2) \/ + execIO ks ks2) $; +theorem ksStepT (ks ks2: nat): + $ ksStep ks ks2 -> ks e. KernelState /\ ks2 e. KernelState $; + +def ksReachable (ks ks2: nat): wff; +theorem ksReachable0 (ks: nat): $ ks e. KernelState -> ksReachable ks ks $; +theorem ksReachableS (ks ks2 ks3: nat): + $ ksStep ks ks2 -> ksReachable ks2 ks3 -> ksReachable ks ks3 $; +theorem ksReachableInd {ks1 ks2: nat} (ks ks3: nat) (A: set): + $ ks e. A /\ A. ks1 A. ks2 (ksStep ks1 ks2 -> ks1 e. A -> ks2 e. A) /\ + ksReachable ks ks3 -> ks3 e. A $; +theorem ksReachableT (ks ks2: nat): + $ ksReachable ks ks2 -> ks e. KernelState /\ ks2 e. KernelState $; + +--| `terminates_ensuring k P` asserts that starting from initial configuration `k` +--| containing the value on input, with the ability to read more files as +--| necessary, the program always reaches the exit point and returns a value, +--| and moreover, if it returns `0`, then the relation `P` holds of the final +--| input and output. +def terminates_ensuring (k .k2 .k3 .exit_code: nat) (P: set): wff = +$ k e. KernelState /\ + A. k2 (ksReachable k k2 -> + E. k3 E. exit_code (ksReachable k2 k3 /\ + execExit (ksCfg k3) exit_code /\ + (exit_code = 0 -> ksIn k3, ksOut k3 e. P))) $; +theorem terminates_ensuringT (k: nat) (P: set): + $ terminates_ensuring k P -> k e. KernelState $; + +--| `succeeds k i o` asserts that starting from initial configuration `k`, +--| the program reaches the exit point and returns success (exit code 0), and +--| puts `o` on standard out and leaves `i` on standard in. +def succeeds (k i o .k2: nat): wff = +$ E. k2 (ksReachable k k2 /\ + ksIn k2 = i /\ ksOut k2 = o /\ execExit (ksCfg k2) 0) $; +theorem succeedsT (k i o: nat): + $ succeeds k i o -> k e. KernelState /\ i e. List u8 /\ o e. List u8 $; + +--| The basic relation between `terminates_ensuring k P` and `succeeds k i o`: +--| together they imply that the property `P` is satisfied. +theorem terminates_ensuring_succeeds (k i o: nat) (P: set): + $ terminates_ensuring k P /\ succeeds k i o -> i, o e. P $; + +---------------------------------------- +-- ELF file format and the initial state +---------------------------------------- + +def ELF_MAGIC: nat = $ ch x7 xf : ch x4 x5 : ch x4 xc : ch x4 x6 : 0 $; +def ELF_CLASS_64: nat = $ 2 $; +def ELF_DATA_2LSB: nat = $ 1 $; +def ELF_VERSION: nat = $ 1 $; +def ELF_IDENT: nat = +$ ELF_MAGIC ++ ELF_CLASS_64 : ELF_DATA_2LSB : ELF_VERSION : repeat 0 9 $; +theorem ELF_IDENT_T: $ ELF_IDENT e. Array u8 16 $; + +def ET_EXEC: nat = $ u16Bytes 2 $; +def EM_X86_64: nat = $ u16Bytes (ch x3 xe) $; +def E_VERSION: nat = $ u32Bytes 1 $; +def E_FLAGS: nat = $ u32Bytes 0 $; +def EH_SIZE: nat = $ 64 $; +def PH_SIZE: nat = $ ch x3 x8 $; +def SH_SIZE: nat = $ 64 $; +--| This checks the ELF header assuming x86 architecture. +def elfHeader (l entry phoff shoff phnum shnum .shstrndx: nat): wff = +$ entry e. u64 /\ phoff e. u64 /\ shoff e. u64 /\ + phnum e. u16 /\ phnum < bitsNeg 16 1 /\ + shnum e. u16 /\ shnum < bitsNeg 16 1 /\ + E. shstrndx (shstrndx e. u16 /\ + l = ELF_IDENT ++ ET_EXEC ++ EM_X86_64 ++ E_VERSION ++ + u64Bytes entry ++ u64Bytes phoff ++ u64Bytes shoff ++ + E_FLAGS ++ u16Bytes EH_SIZE ++ u16Bytes PH_SIZE ++ u16Bytes phnum ++ + u16Bytes SH_SIZE ++ u16Bytes shnum ++ u16Bytes shstrndx) $; +theorem elfHeaderT (l entry phoff shoff phnum shnum: nat): + $ elfHeader l entry phoff shoff phnum shnum -> + l e. Array u8 EH_SIZE /\ entry e. u64 /\ phoff e. u64 /\ shoff e. u64 /\ + phnum e. u16 /\ shnum e. u16 $; + +-- sadly the protection flag bits for ELF are different than the memory page +-- protection flags: R=4, W=2, X=1 for ELF; R=1, W=2, X=4 for the syscall +def protToFlags (prot: nat): nat = +$ consBit (PROT_EXEC C_ prot) ( + consBit (PROT_WRITE C_ prot) (nat (PROT_READ C_ prot))) $; + +def PT_LOAD: nat = $ 1 $; +def pHeader (l type prot off vaddr filesz memsz .i: nat): wff = +$ type e. u32 /\ prot e. Prot /\ off e. u64 /\ vaddr e. u64 /\ + filesz e. u64 /\ memsz e. u64 /\ filesz <= memsz /\ + E. i (i < 64 /\ 2 ^ i || bitsSub 64 vaddr off /\ + l = u32Bytes type ++ u32Bytes (protToFlags prot) ++ + u64Bytes off ++ u64Bytes vaddr ++ u64Bytes 0 ++ + u64Bytes filesz ++ u64Bytes memsz ++ u64Bytes (2 ^ i)) $; +theorem pHeaderT (l type prot off vaddr filesz memsz: nat): + $ pHeader l type prot off vaddr filesz memsz -> + l e. Array u8 PH_SIZE /\ type e. u32 /\ prot e. Prot /\ off e. u64 /\ + vaddr e. u64 /\ filesz e. u64 /\ memsz e. u64 $; + +def basicElfEH (file entry phoff .eh: nat): wff = +$ file e. List u8 /\ + E. eh (sublistAt 0 file eh /\ elfHeader eh entry phoff 0 1 0) $; +theorem basicElfEH_T (file entry phoff: nat): + $ basicElfEH file entry phoff -> + file e. List u8 /\ entry e. u64 /\ phoff e. u64 $; + +def basicElf (entry prot off seg: nat): wff = +$ entry e. u64 /\ prot e. Prot /\ seg e. List u8 /\ off + len seg e. u64 /\ + off <= entry /\ entry < off + len seg $; +theorem BasicElfT (entry prot off seg: nat): + $ basicElf entry prot off seg -> + entry e. u64 /\ prot e. Prot /\ off e. u64 /\ seg e. List u8 $; + +--| This defines a basic ELF file (only one program segment, no sections) +--| and extracts the program segment and its protection and location. +def parseBasicElf (file entry prot vaddr seg: nat) + (.off .eh .ph .phoff .fseg .memsz: nat): wff = +$ file e. List u8 /\ + E. eh E. ph E. phoff E. off E. fseg E. memsz ( + sublistAt 0 file eh /\ elfHeader eh entry phoff 0 1 0 /\ + sublistAt phoff file ph /\ + pHeader ph PT_LOAD prot off vaddr (len fseg) memsz /\ + sublistAt off file fseg /\ + vaddr + memsz e. u64 /\ vaddr <= entry /\ entry < vaddr + memsz /\ + seg = fseg ++ repeat 0 (memsz - len fseg)) $; +theorem parseBasicElfT (file entry prot vaddr seg: nat): + $ parseBasicElf file entry prot vaddr seg -> file e. List u8 /\ + basicElf entry prot vaddr seg $; + +--| `isBasicElf elf` means that `elf` is a string that satisfies the +--| ELF specification. +def isBasicElf (elf: string) (.entry .prot .off .seg: nat): wff = +$ E. entry E. prot E. off E. seg parseBasicElf elf entry prot off seg $; + +def blankConfig (entry k .f .m .r: nat): wff = +$ E. f E. m (f e. Flags /\ m e. Memory /\ + k = mkCfg 0 entry (\. r e. Regs, 0) f m) $; +theorem blankConfigT (entry k: nat): + $ entry e. u64 /\ blankConfig entry k -> k e. Config $; + +def allocStack (k m k3 km3 + .sp .base .guard .low .stack .argc .k2 .km2 .x .arg .cstr .str: nat): wff = +$ k e. Config /\ E. sp E. low E. stack E. argc E. k2 E. km2 ( + low e. List u8 /\ 2 ^ 12 + len low <= sp /\ sp + len stack e. u64 /\ + mapMem (PROT_READ + PROT_WRITE) (setReg k RSP sp) m + (sp - len low) (low ++ stack) k2 km2 /\ + E. guard (guard e. Array u8 (2 ^ 12) /\ + mapMem 0 k2 km2 (sp - len low - 2 ^ 12) guard k3 km3) /\ + argc e. u64 /\ sublistAt 0 stack (u64Bytes argc) /\ + A. x (x < argc -> E. arg E. cstr ( + sublistAt (8 * suc x) stack (u64Bytes (sp + arg)) /\ + sublistAt arg stack cstr /\ E. str toCStr str cstr))) $; +theorem allocStackT (k m k3 km3: nat): + $ allocStack k m k3 km3 -> + k e. Config /\ m e. PageMapping (getMemory k) /\ + k3 e. Config /\ km3 e. PageMapping (getMemory k3) $; + +--| This defines the initial state set up from a basic ELF file (only one +--| program segment, no sections). +def initialConfig (elf: string) (ks: nat) + (.entry .prot .off .seg .k0 .k1 .km1 .k2 .km2 .a: nat): wff = +$ E. entry E. prot E. off E. seg E. k0 E. k1 E. km1 E. k2 E. km2 ( + parseBasicElf elf entry prot off seg /\ + blankConfig entry k0 /\ allocStack k0 (\. a e. u64, 0) k1 km1 /\ + mapMem prot k1 km1 off seg k2 km2 /\ + ks = mkKS 0 0 k2 km2) $; +theorem initialConfigT (elf: string) (ks: nat): + $ initialConfig elf ks -> ks e. KernelState $; + +------------------ +-- compiler.mm0 -- +------------------ + + +-- It should suffice to use x86.mm0 directly for compiler.mm1, +-- because it (should) add no new axioms, +-- but in the interim we are using this to keep the partial proofs checked in CI: +axiom sorry (p: wff): $ p $; +term sorry_nat: nat; +term sorry_set: set; +term sorry_wff: wff; + +-- Search for theorem ... = 'sorry; to find the incomplete proofs +-- (or delete the sorry axiom and see what breaks). Proofs depending on this axiom +-- also show up in the doc-gen tool in the "Axiom use" section. + +------------------- +-- hello_mmc.mm0 -- +------------------- + + +def test: string; + +theorem test_isBasicElf: $ isBasicElf test $; +theorem test_ok {k vs x: nat}: + $ A. k (initialConfig test k -> terminates_ensuring k (S\ vs, S\ x, sn 0)) $; + +-- output string: $ test $;