diff --git a/examples/assembler-new.mm1 b/examples/assembler-new.mm1
index 57903eca..526ef1e2 100644
--- a/examples/assembler-new.mm1
+++ b/examples/assembler-new.mm1
@@ -194,6 +194,18 @@ $ n e. Bits (8 * suc k) /\ s = toBytes (suc k) n $;
 @mmc-th theorem parseUBytes01: $ parseUBytes 0 a0 (s1 (ch x0 a0)) $ =
 '(iani xelBits81 xtoBytes11);
 
+theorem parseUBytes_x00xN (h1: $ s = repeat 0 x $) (h2: $ x = suc k $): $ parseUBytes k x0 s $ =
+'(iani xelBits81 @ eqtr h1 @ eqtr4 (repeateq2 h2) @ eqtr (toByteseq2 h2n0) toBytes02);
+do {
+  --| (parseUBytes_x00xn i) proves `|- parseUBytes {i-1} x0 _x00x{i}`
+  (def (parseUBytes_x00xn i) (atom-app 'parseUBytes_x00x i))
+  (scan (range 1 8) @ fn (i)
+    (add-tac-thm! (parseUBytes_x00xn i) () ()
+        $ parseUBytes ,(sucs {i - 1}) x0 ,(_x00xn i) $ () @ fn ()
+      @ refine '(parseUBytes_x00xN (,(_x00xn_eq i)) (,(h2nn i))))
+    (mmc-th (parseUBytes_x00xn i)))
+};
+
 @mmc-th local def parseIBytesPos (k n: nat) (s: string): wff =
 $ n e. Bits (8 * k + 7) /\ s = toBytes (suc k) n $;
 
@@ -808,7 +820,7 @@ $ S\ p, S\ s, {x | E. ds (mkRMI2 dst src ds /\ decode (xastCMov (suc c) sz ds) s
 --------------------------------------------
 
 @mmc-th local def asmProc (n: nat) (A: set): set =
-$ S\ s, {p | p = n /\ E. t1 E. t2 E. z (s = t1 ++ t2 /\ t1 != 0 /\ p, t1, 0 e. A)} $;
+$ S\ s, {p | p = n /\ E. t1 E. t2 (s = t1 ++ t2 /\ t1 != 0 /\ p, t1, 0 e. A)} $;
 
 @mmc-th theorem asmProcI (s x n y A)
   (h1: $ localAssemble x s x0 n A $)
@@ -838,7 +850,11 @@ do (ignore @ on-hexstrings @ fn (n)
 
 --| Global context. In lean:
 --| ```lean
---| structure gctx := (content: string) (filesz memsz: nat) (result: prop)
+--| structure GCtx where
+--|   content : String
+--|   fileSz : UInt64
+--|   memSz : UInt64
+--|   result : SProp
 --| ```
 @mmc-th local def mkGCtx (content: string) (filesz memsz: nat) (result: set): set =
 $ Sum (Sum (content, filesz, memsz) result) 0 $;
diff --git a/examples/compiler-new.mm1 b/examples/compiler-new.mm1
index 29964061..3f7f92de 100644
--- a/examples/compiler-new.mm1
+++ b/examples/compiler-new.mm1
@@ -2,6 +2,11 @@ import "compiler-old.mm1";
 
 do (warn-unused-vars #f);
 
+-- `Valuation := Nat -> Nat` (finitely supported)
+-- `VProp := Valuation -> SProp`
+-- `Ty := Valuation -> Nat -> SProp`
+-- `Expr := Valuation -> Nat`
+
 --| `tyUnit: Ty`:
 --| The type `()`, the unit type.
 @_ @mmc-th local def tyUnit: set = $ S\ vs, S\ x, emp $;
@@ -10,15 +15,15 @@ do (warn-unused-vars #f);
 --| The type `F.`, the empty type.
 @_ @mmc-th local def tyFalse: set = $ 0 $;
 
---| `isTyped: Expr -> Ty -> SProp`:
+--| `isTyped: Expr -> Ty -> VProp`:
 --| The assertion `[e: ty]`, which asserts that expression `e` has type `ty`.
 @_ @mmc-th local def isTyped (e ty: set): set = $ S\ vs, ty @' vs @' (e @ vs) $;
 
---| `isHyp: Ty -> SProp`:
+--| `isHyp: Ty -> VProp`:
 --| The assertion `[(): ty]`, which asserts that type `ty` is inhabited.
 @_ @mmc-th local def isHyp (ty: set): set = $ S\ vs, ty @' vs @' 0 $;
 
---| `asTy: SProp -> Ty`: Convert a SProp to a Ty by ignoring the value argument.
+--| `asTy: VProp -> Ty`: Convert a VProp to a Ty by ignoring the value argument.
 @_ @mmc-th local def asTy (P: set): set = $ S\ vs, S\ x, P @' vs $;
 
 --| `tyTyped: Expr -> Ty -> Ty`:
@@ -34,10 +39,10 @@ do (warn-unused-vars #f);
 --| A return ABI saying you can't return
 @_ @mmc-th local def noRet: set = $ sorry_set $; -- TODO
 
--- inductive epilogue
--- | free : nat -> epilogue -> epilogue
--- | pop : regnum -> epilogue -> epilogue
--- | ret : epilogue
+-- inductive Epilogue
+--   | free : Nat → Epilogue → Epilogue
+--   | pop : RegNum → Epilogue → Epilogue
+--   | ret : Epilogue
 
 @_ local def epi_ok (epi: nat): wff = $ epi != 0 $;
 @_ local def epi_regs (epi: nat): nat = $ fst (epi - 1) $;
@@ -49,16 +54,16 @@ $ if (epi_ok epi /\ n != 0 /\ epi_sp epi = 0) (suc (epi_regs epi, n)) 0 $;
 $ if (epi_ok epi /\ epi_sp epi = 0) (suc (reg : epi_regs epi, 0)) 0 $;
 @mmc-th local def epiRet: nat = $ suc (0, 0) $;
 
---| Procedure-global context, constructor for `pctx1` type.
---| * `ret`: the return ABI
---| * `epi: epilogue`: the epilogue sequence
+--| Procedure-global context, constructor for `PCtx1` type.
+--| * `ret: ReturnABI`: the return ABI
+--| * `epi: Epilogue`: the epilogue sequence
 --| * `se: bool`: true if this procedure is allowed to perform side effects
 @mmc-th local def mkPCtx1 (ret: set) (epi: nat) (se: wff): set =
 $ Sum ret (epi, nat se) $;
 
---| Procedure-global context, constructor for `pctx := gctx * pctx1` type.
---| We write it in such a way that `pctx` extends `gctx`,
---| so `gctx` extraction functions also work on `pctx`.
+--| Procedure-global context, constructor for `PCtx := GCtx * PCtx1` type.
+--| We write it in such a way that `PCtx` extends `GCtx`,
+--| so `GCtx` extraction functions also work on `PCtx`.
 @mmc-th local def mkPCtx (gctx pctx1: set): set =
 $ Sum (Fst gctx) (Sum pctx1 0) $;
 
@@ -77,14 +82,19 @@ theorem pctx_se_PI: $ pctx_se (mkPCtx gctx (mkPCtx1 ret epi se)) <-> se $ =
 
 @_ local def soReturnType (ret: set): set = $ sorry_set $; -- TODO
 
-@_ local def okPCtx (pctx: set): wff = $ epi_ok (pctx_epi pctx) $;
+@_ local def okGCtx (gctx: set): wff =
+$ len (gctx_content gctx) = gctx_filesz gctx /\ gctx_filesz gctx <= gctx_memsz gctx /\
+  text_start + gctx_memsz gctx e. u64 $;
+
+@_ local def okPCtx (pctx: set): wff = $ okGCtx pctx /\ epi_ok (pctx_epi pctx) $;
 
 --| Block-local context. In lean:
 --| ```lean
---| structure bctx := (G : pctx) (labs : list label_group)
+--| structure BCtx extends PCtx where
+--|   labelGroups : List (Expr × LabelGroup)
 --| ```
---| We write it in such a way that `bctx` extends `pctx`,
---| so `pctx` extraction functions also work on `bctx`.
+--| We write it in such a way that `BCtx` extends `PCtx`,
+--| so `PCtx` extraction functions also work on `BCtx`.
 @mmc-th local def mkBCtx (pctx labs: set): set = $ Sum (Fst pctx) (Sum (Fst (Snd pctx)) labs) $;
 
 theorem pctx_ret_BI: $ pctx_ret (mkBCtx (mkPCtx gctx (mkPCtx1 ret epi se)) labs) == ret $ =
@@ -100,37 +110,145 @@ theorem pctx_se_BI: $ pctx_se (mkBCtx (mkPCtx gctx (mkPCtx1 ret epi se)) labs) <
 
 @_ local def okBCtx (bctx: set): wff = $ okPCtx bctx $; -- TODO
 
-@_ local def soLayout (tctx: set): set = $ sorry_set $; -- TODO
-@_ local def soType (tctx: set): set = $ sorry_set $; -- TODO
+--| Run time values which are fixed during execution of a function. In lean:
+--| ```lean
+--| structure Frame where
+--|   frame : Heap
+--|   retAddr : UInt64
+--|   pushed : List UInt64
+--|   lo : Nat
+--|   top : Nat
+--| ```
+local def mkFrame (fr ret pushed lo top: nat): nat = $ fr, (ret, pushed), lo, top $;
+
+@_ local def fr_heap (fr: nat): nat = $ fst fr $;
+@_ local def fr_retAddr (fr: nat): nat = $ fst (pi21 fr) $;
+@_ local def fr_pushed (fr: nat): nat = $ snd (pi21 fr) $;
+@_ local def fr_lo (fr: nat): nat = $ pi221 fr $;
+@_ local def fr_top (fr: nat): nat = $ pi222 fr $;
+
+@_ local def okFrame (fr: nat): wff =
+$ isfun (fr_heap fr) /\ (fr_retAddr fr : fr_pushed fr) e. List u64 /\
+  fr_lo fr <= fr_top fr /\ fr_top fr e. u64 $;
+
+@_ local def okFramePCtx (fr: nat) (pctx: set): wff =
+$ len (fr_pushed fr) = len (epi_regs (pctx_epi pctx)) $;
+
+@_ local def fr_frame (fr: nat): set =
+$ ^s okFrame fr /\s sn (fr_heap fr) $;
+
+@_ local def stackLayoutG (fr n sz pushed: nat) (L: set): set =
+$ S[fr_top fr - len pushed / sp1] S[sp1 - sz / sp] (
+  ^s (fr_lo fr + 2 ^ 12 + n + sz + len pushed <= fr_top fr) /\s
+  RSP >->r sp *s fr_lo fr >=>.[fr_lo fr] sp *s sp1 >=> pushed *s
+  L @' fr_lo fr @' sp) $;
+
+@_ local def stackLayout (fr n sz: nat) (L: set): set =
+$ stackLayoutG fr n sz (ljoin (map (\ x, u64Bytes x) (fr_pushed fr |> fr_retAddr fr))) L $;
+
+@_ local def mainLayout (content ip: nat): set =
+$ text_start >=>c content *s RIP>-> ip *s s_OK *s flags>->. $;
+
+local def SL_0: set = $ S\ lo, S\ sp, emp $;
+
+@_ local def SL_pad (off n: nat): set = $ S\ lo, S\ sp, ((sp + off) >=>.[lo] n) $;
+
+@_ local def SL_A (A B: set): set = $ S\ lo, S\ sp, (A @' lo @' sp *s B @' lo @' sp) $;
+
+--| `mctx0: MCtx`: the empty machine context.
+@mmc-th local def mctx0: set = $ S\ vs, Sum emp SL_0 $;
+
+--| `FREE: RegNum -> MCtx`: indicates that the named register is available for use
+@mmc-th local def FREE (r: hex): set = $ S\ vs, Sum (E.s v e. u64, r >->r v) SL_0 $;
+
+--| `stkFREE (off n: nat): MCtx`: This represents
+--| a piece of free stack space at `[RSP+off..RSP+off+n]`.
+@mmc-th local def stkFREE (off n: nat): set = $ S\ vs, Sum emp (SL_pad off n) $;
+
+@_ local def REG_N (r: nat) (val: set): set = $ S\ vs, Sum (r >->r val @ vs) SL_0 $;
+
+--| `REG (r: RegNum) (val: Expr): MCtx`: This represents
+--| a register which holds the given expression.
+@mmc-th local def REG (r: hex) (val: set): set = $ REG_N r val $;
+notation REG (r val): nat = ($r[$:20) r ($]:$:0) val;
+
+@_ @mmc-th local def mctxA (A B: set): set =
+$ S\ vs, Sum (Fst (A @' vs) *s Fst (B @' vs)) (SL_A (Snd (A @' vs)) (Snd (B @' vs))) $;
+infixl mctxA: $+M$ prec 20;
+
+theorem mctxA_com: $ (A +M B) == (B +M A) $ = 'sorry;
+theorem mctxA_01: $ (mctx0 +M A) == A $ = 'sorry;
+theorem mctxA_02: $ (A +M mctx0) == A $ = '(eqstr mctxA_com mctxA_01);
+theorem mctxA_ass: $ ((A +M B) +M C) == (A +M (B +M C)) $ = 'sorry;
+
+@_ local def bddMCtxN (mctx: set) (lo hi: nat): wff =
+$ A. vs (Snd (mctx @' vs) == SL_0 /\
+    E. f (f e. Arrow {r | r e. Regs /\ lo <= r /\ r <= hi} u64 /\
+      Fst (mctx @' vs) C_ |*|s r e. Dom f, r >->r f @ r)) $;
+
+@mmc-th local def bddMCtx (mctx: set) (lo hi: hex): wff = $ bddMCtxN mctx lo hi $;
+theorem bddMCtx_0: $ bddMCtxN mctx0 0 0 $ = 'sorry;
+@mmc-th theorem bddMCtx_FREE: $ bddMCtx (FREE r) r r $ = 'sorry;
+@mmc-th theorem bddMCtx_REG: $ bddMCtx (r[r]: v) r r $ = 'sorry;
+@mmc-th theorem bddMCtx_A (h1: $ bddMCtx A a b $) (h2: $ bddMCtx B c d $) (h3: $ b < c $):
+  $ bddMCtx (A +M B) a d $ = 'sorry;
+
+@mmc-th local def okMCtx (mctx: set): wff = $ E. a E. b bddMCtxN mctx a b $;
+theorem okMCtxI (h: $ bddMCtxN mctx a b $): $ okMCtx mctx $ = '(iexie @ iexde @ mpbiri h ,eqtac);
+@mmc-th theorem okMCtx0: $ okMCtx mctx0 $ = '(okMCtxI bddMCtx_0);
+@mmc-th theorem okMCtxS (h: $ bddMCtx mctx a b $): $ okMCtx mctx $ = '(okMCtxI h);
+
+@_ @mmc-th local def pushMCtx (mctx1 val mctx2: set): wff = $ mctx2 == (mctx1 +M val) $;
+
+@mmc-th theorem pushMCtx0: $ pushMCtx mctx0 val val $ = '(eqscom mctxA_01);
+
+@mmc-th theorem pushMCtx1L: $ pushMCtx A val (val +M A) $ = 'mctxA_com;
+
+@mmc-th theorem pushMCtx1R: $ pushMCtx A val (A +M val) $ = 'eqsid;
+
+@mmc-th theorem pushMCtxR (h: $ pushMCtx B val C $): $ pushMCtx (A +M B) val (A +M C) $ =
+'(eqstr4 (mctxAeq2 h) mctxA_ass);
+
+@mmc-th theorem pushMCtxL (h: $ pushMCtx A val B $): $ pushMCtx (A +M C) val (B +M C) $ =
+'(mpbi (pushMCtxeq mctxA_com eqsid mctxA_com) @ pushMCtxR h);
+
+@mmc-th theorem pushMCtxRotL
+  (h: $ pushMCtx mctx val (A +M (B +M C)) $):
+  $ pushMCtx mctx val ((A +M B) +M C) $ = '(mpbir (pushMCtxeq3 mctxA_ass) h);
+@mmc-th theorem pushMCtxRotR
+  (h: $ pushMCtx mctx val ((A +M B) +M C) $):
+  $ pushMCtx mctx val (A +M (B +M C)) $ = '(mpbi (pushMCtxeq3 mctxA_ass) h);
+
+--| Type context, or type state.
+--| The first part is the logical context, where variables and their types are stored,
+--| and the second part is the machine context where variables are assigned to memory locations.
+@mmc-th local def mkTCtx (vctx: set) (vctx_sz: nat) (mctx: set): set =
+$ Sum vctx_sz (S\ vs, Sum (vctx @' vs *s Fst (mctx @' vs)) (Snd (mctx @' vs))) $;
 
-@_ local def frFrame (fr: nat): nat = $ fst fr $;
-@_ local def frRetAddr (fr: nat): nat = $ pi21 fr $;
-@_ local def frPushed (fr: nat): nat = $ pi22 fr $;
-@_ local def frHeaderLayout (fr: nat): set =
-$ L_1 (map (\ x, u64Bytes x) (frRetAddr fr : rev (frPushed fr))) $;
+@_ local def tctx_sz (tctx: set): nat = $ lower (Fst tctx) $;
+@_ local def tctx_type (tctx: set) (vs: nat): set = $ Fst (Snd tctx @' vs) $;
+@_ local def tctx_layout (tctx: set) (vs: nat): set = $ Snd (Snd tctx @' vs) $;
 
-@_ local def okReturnN (pctx: set) (fr: nat): wff =
+@_ local def okReturn (pctx: set) (fr: nat): wff =
 $ s_ok
-  (sn (frFrame fr) *s (
-    main_layout (gctx_content pctx) 0 (frRetAddr fr) 8 L_emp *s
+  (fr_frame fr *s (
+    mainLayout (gctx_content pctx) (fr_retAddr fr) *s
+    stackLayoutG fr 8 0 0 SL_0 *s
     soReturnType (pctx_ret pctx)))
   (gctx_result pctx) $;
 
-@_ local def okCodeN (bctx tctx: set) (fr ip) =
+@_ local def okCodeN (bctx tctx: set) (fr ip: nat) =
 $ s_ok
-  (sn (frFrame fr) *s (
-    main_layout
-      (gctx_content bctx)
-      (epi_sp (pctx_epi bctx) + 8)
-      (text_start + ip)
-      8
-      (L_seq (frHeaderLayout fr) (soLayout tctx)) *s
-    soType tctx))
+  (fr_frame fr *s (
+    mainLayout (gctx_content bctx) (text_start + ip) *s
+    E.s vs e. _V, (
+      stackLayout fr 8 (epi_sp (pctx_epi bctx)) (tctx_layout tctx vs) *s
+      tctx_type tctx vs)))
   (gctx_result bctx) $;
 
 @mmc-th local def labelGroup0: set = $ 0 $;
 prefix labelGroup0: $LG0$ prec max;
-local def labelGroup1 (var ls: set): set = $ E.s v e. var, ls @' v $;
+local def labelGroup1 (var ls: set): set = $ E.s vs e. _V, ls @' vs @' (var @ vs) $;
 @mmc-th local def labelGroup (var ls labs: set): set = $ labs \/s labelGroup1 var ls $;
 notation labelGroup (var ls labs: set): set = ($LG($:85) var ($,$:55) ls ($);$:0) labs;
 
@@ -139,21 +257,18 @@ notation labelGroup (var ls labs: set): set = ($LG($:85) var ($,$:55) ls ($);$:0
 @mmc-th theorem findLabelsS (h: $ findLabels labs var ls $):
   $ findLabels (LG(var, ls1); labs) var ls $ = 'sorry;
 
---| `labels.and : labels -> labels -> labels`
+--| `Labels.and : Labels -> Labels -> Labels`
 @mmc-th local def labelA (A B: set): set = $ A \/s B $;
 infixl labelA: $+L$ prec 20;
---| `labels.one : block_loc -> expr -> tctx -> labels`
+--| `Labels.one : BlockLoc -> Expr -> TCtx -> Labels`
 @mmc-th local def label1 (x: nat) (var tctx: set): set =
-$ S\ v, S\ c, S\ epi, S\ fr, S\ p, (sn (frFrame fr) *s (
-    If (x = 0)
-      (E.s ip e. u64, main_layout c (epi_sp epi + 8) ip 8
-        (L_seq (frHeaderLayout fr) (soLayout tctx)))
-      (main_layout c (epi_sp epi + 8) (text_start + p + (x - 1)) 8
-        (L_seq (frHeaderLayout fr) (soLayout tctx))) *s
-    ^s (v e. var) *s -- TODO, this is incorrect
-    soType tctx)) $;
-
-@mmc-th local def findLabel (ls: set) (x: nat) (var A: set): wff = $ label1 x var A C_ ls $; -- TODO
+$ S\ vs, S\ v, S\ c, S\ epi, S\ fr, S\ p, (fr_frame fr *s (
+    If (x = 0) (E.s ip e. u64, mainLayout c ip) (mainLayout c (text_start + p + (x - 1))) *s
+    ^s (vs, v e. var) *s
+    stackLayout fr 8 (epi_sp epi) (tctx_layout tctx vs) *s
+    tctx_type tctx vs)) $;
+
+@mmc-th local def findLabel (ls: set) (x: nat) (var A: set): wff = $ label1 x var A C_ ls $;
 @mmc-th theorem findLabel_l (h: $ findLabel A x var P $): $ findLabel (A +L B) x var P $ = 'sorry;
 @mmc-th theorem findLabel_r (h: $ findLabel B x var P $): $ findLabel (A +L B) x var P $ = 'sorry;
 @mmc-th theorem findLabel1: $ findLabel (label1 x var P) x var P $ = 'sorry;
@@ -164,11 +279,11 @@ $ S\ v, S\ c, S\ epi, S\ fr, S\ p, (sn (frFrame fr) *s (
 @_ @mmc-th local def vctxA (A B: set): set = $ S\ vs, (A @' vs *s B @' vs) $;
 infixl vctxA: $*V$ prec 20;
 
---| `vVar: nat -> ty -> vctx`:
+--| `vVar: nat -> Ty -> VCtx`:
 --| A variable record in a variable context. This asserts that `v_n: ty`.
 @_ @mmc-th local def vVar (n: nat) (ty: set): set = $ isTyped (eVar n) ty $;
 
---| `vHyp: ty -> vctx`:
+--| `vHyp: Ty -> VCtx`:
 --| A hypothesis, or unnamed variable. This asserts that `(): ty`.
 @_ @mmc-th local def vHyp (ty: set): set = $ isHyp ty $;
 
@@ -188,12 +303,10 @@ infixl vctxA: $*V$ prec 20;
   $ okVCtxGet vctx2 A $ = 'sorry;
 
 @mmc-th theorem okVCtxGet_R
-  (h: $ okVCtxGet ((A *V B) *V C) ty $):
-  $ okVCtxGet (A *V (B *V C)) ty $ = 'sorry;
+  (h: $ okVCtxGet ((A *V B) *V C) ty $): $ okVCtxGet (A *V (B *V C)) ty $ = 'sorry;
 @mmc-th theorem okVCtxGet_l (h: $ okVCtxGet A ty $): $ okVCtxGet (A *V B) ty $ = 'sorry;
 @mmc-th theorem okVCtxGet_r (h: $ okVCtxGet B ty $): $ okVCtxGet (A *V B) ty $ = 'sorry;
 
-
 @_ @mmc-th local def okVCtxTake (vctx A vctx2: set): wff =
 $ A. vs vctx @' vs =>*s A @' vs *s vctx2 @' vs $;
 
@@ -211,83 +324,9 @@ $ A. vs vctx @' vs =>*s A @' vs *s vctx2 @' vs $;
 @mmc-th theorem okVCtxTake_r (h: $ okVCtxTake B ty B2 $):
   $ okVCtxTake (A *V B) ty (A *V B2) $ = 'sorry;
 
---| `mctx0: mctx`: the empty machine context.
-@mmc-th local def mctx0: set = $ S\ vs, Sum emp L_emp $;
-
---| `FREE: reg -> mctx`: indicates that the named register is available for use
-@mmc-th local def FREE (r: hex): set = $ S\ vs, Sum (E.s v e. u64, r >->r v) L_emp $;
-
---| `stkFREE (off n: nat): mctx`: This represents
---| a piece of free stack space at `[RSP+off..RSP+off+n]`.
-@mmc-th local def stkFREE (off n: nat): set =
--- TODO: `L_at off` is not right here, it should be RSP-relative not an absolute addr
-$ S\ vs, Sum emp (L_at off (L_padn n)) $;
-
-@_ local def REG_N (r: nat) (val: set): set = $ S\ vs, Sum (r >->r val @ vs) L_emp $;
-
---| `REG (r: reg) (val: expr): mctx`: This represents a register which holds the given expression.
-@mmc-th local def REG (r: hex) (val: set): set = $ REG_N r val $;
-notation REG (r val): nat = ($r[$:20) r ($]:$:0) val;
-
-@_ @mmc-th local def mctxA (A B: set): set =
-$ S\ vs, Sum (Fst A @' vs *s Fst B @' vs) (L_seq (Snd A @' vs) (Snd B @' vs)) $;
-infixl mctxA: $+M$ prec 20;
-
-theorem mctxA_com: $ (A +M B) == (B +M A) $ = 'sorry;
-theorem mctxA_01: $ (mctx0 +M A) == A $ = 'sorry;
-theorem mctxA_02: $ (A +M mctx0) == A $ = '(eqstr mctxA_com mctxA_01);
-theorem mctxA_ass: $ ((A +M B) +M C) == (A +M (B +M C)) $ = 'sorry;
-
-@_ local def bddMCtx_N (mctx: set) (lo hi: nat): wff =
-$ Snd mctx == (S\ vs, L_emp) /\
-  sorry_wff $; -- TODO: "Fst mctx is inhabitable and contained in r[lo..hi]"
-
-@mmc-th local def bddMCtx (mctx: set) (lo hi: hex): wff = $ bddMCtx_N mctx lo hi $;
-theorem bddMCtx_0: $ bddMCtx_N mctx0 0 0 $ = 'sorry;
-@mmc-th theorem bddMCtx_FREE: $ bddMCtx (FREE r) r r $ = 'sorry;
-@mmc-th theorem bddMCtx_REG: $ bddMCtx (r[r]: v) r r $ = 'sorry;
-@mmc-th theorem bddMCtx_A (h1: $ bddMCtx A a b $) (h2: $ bddMCtx B c d $) (h3: $ b < c $):
-  $ bddMCtx (A +M B) a d $ = 'sorry;
-
-@mmc-th local def okMCtx (mctx: set): wff = $ E. a E. b bddMCtx_N mctx a b $;
-theorem okMCtx_I (h: $ bddMCtx_N mctx a b $): $ okMCtx mctx $ = '(iexie @ iexde @ mpbiri h ,eqtac);
-@mmc-th theorem okMCtx0: $ okMCtx mctx0 $ = '(okMCtx_I bddMCtx_0);
-@mmc-th theorem okMCtxS (h: $ bddMCtx mctx a b $): $ okMCtx mctx $ = '(okMCtx_I h);
-
-@_ @mmc-th local def pushMCtx (mctx1 val mctx2: set): wff = $ mctx2 == (mctx1 +M val) $;
-
-@mmc-th theorem pushMCtx0: $ pushMCtx mctx0 val val $ = '(eqscom mctxA_01);
-
-@mmc-th theorem pushMCtx1L: $ pushMCtx A val (val +M A) $ = 'mctxA_com;
-
-@mmc-th theorem pushMCtx1R: $ pushMCtx A val (A +M val) $ = 'eqsid;
-
-@mmc-th theorem pushMCtxR (h: $ pushMCtx B val C $): $ pushMCtx (A +M B) val (A +M C) $ =
-'(eqstr4 (mctxAeq2 h) mctxA_ass);
-
-@mmc-th theorem pushMCtxL (h: $ pushMCtx A val B $): $ pushMCtx (A +M C) val (B +M C) $ =
-'(mpbi (pushMCtxeq mctxA_com eqsid mctxA_com) @ pushMCtxR h);
-
-@mmc-th theorem pushMCtxRotL
-  (h: $ pushMCtx mctx val (A +M (B +M C)) $):
-  $ pushMCtx mctx val ((A +M B) +M C) $ = '(mpbir (pushMCtxeq3 mctxA_ass) h);
-@mmc-th theorem pushMCtxRotR
-  (h: $ pushMCtx mctx val ((A +M B) +M C) $):
-  $ pushMCtx mctx val (A +M (B +M C)) $ = '(mpbi (pushMCtxeq3 mctxA_ass) h);
-
---| Type context, or type state.
---| The first part is the logical context, where variables and their types are stored,
---| and the second part is the machine context where variables are assigned to memory locations.
-@mmc-th local def mkTCtx (vctx: set) (vctx_sz: nat) (mctx: set): set =
-$ Sum vctx_sz (S\ vs, Sum (vctx @' vs *s Fst mctx @' vs) (Snd mctx @' vs)) $;
-
-@_ local def tctx_sz (tctx: set): nat = $ lower (Fst tctx) $;
-@_ local def tctx_P (tctx: set) (vs: nat): set = $ Fst (Snd tctx @' vs) $;
-@_ local def tctx_L (tctx: set) (vs: nat): set = $ Snd (Snd tctx @' vs) $;
-
 @_ @mmc-th local def okPushVar (tctx ty tctx2: set): wff =
 $ tctx2 == Sum (suc (tctx_sz tctx))
-    (S\ vs, Sum (tctx_P tctx vs *s ty @' vs @' (vs @ tctx_sz tctx)) (tctx_L tctx vs)) $;
+    (S\ vs, Sum (tctx_type tctx vs *s ty @' vs @' (vs @ tctx_sz tctx)) (tctx_layout tctx vs)) $;
 
 @mmc-th theorem okPushVarI
   (h1: $ okVCtxPush vctx (vVar n ty) vctx2 $)
@@ -295,27 +334,22 @@ $ tctx2 == Sum (suc (tctx_sz tctx))
   $ okPushVar (mkTCtx vctx n mctx) ty (mkTCtx vctx2 n2 mctx) $ = 'sorry;
 
 @mmc-th local def okPushHyp (tctx ty tctx2: set): wff =
-$ tctx2 == Sum (tctx_sz tctx) (S\ vs, Sum (tctx_P tctx vs *s ty @' vs @' 0) (tctx_L tctx vs)) $;
+$ tctx2 == Sum (tctx_sz tctx)
+    (S\ vs, Sum (tctx_type tctx vs *s ty @' vs @' 0) (tctx_layout tctx vs)) $;
 
 @mmc-th theorem okPushHypI
   (h1: $ okVCtxPush vctx (vHyp ty) vctx2 $):
   $ okPushHyp (mkTCtx vctx n mctx) ty (mkTCtx vctx2 n mctx) $ = 'sorry;
 
-@_ @mmc-th local def okReadHypVCtx (vctx ty: set): wff =
-$ A. vs E. n vctx @' vs =>*s ty @' vs @' n $;
+@_ @mmc-th local def okReadHyp (tctx ty: set): wff =
+$ A. vs E. n tctx_type tctx vs =>*s ty @' vs @' n $;
 
-@mmc-th theorem okReadHypVCtxI
+@mmc-th theorem okReadHypHyp
   (h1: $ okVCtxGet vctx (vHyp ty) $):
-  $ okReadHypVCtx vctx ty $ = 'sorry;
+  $ okReadHyp (mkTCtx vctx n mctx) ty $ = 'sorry;
 
 @mmc-th theorem okReadHypVar
   (h1: $ okVCtxGet vctx (vVar v ty) $):
-  $ okReadHypVCtx vctx ty $ = 'sorry;
-
-@_ @mmc-th local def okReadHyp (tctx ty: set): wff = $ okReadHypVCtx (S\ vs, tctx_P tctx vs) ty $;
-
-@mmc-th theorem okReadHypI
-  (h1: $ okVCtxTake vctx ty vctx2 $):
   $ okReadHyp (mkTCtx vctx n mctx) ty $ = 'sorry;
 
 @mmc-th theorem okReadHyp_unit:
@@ -323,18 +357,19 @@ $ A. vs E. n vctx @' vs =>*s ty @' vs @' n $;
 
 @mmc-th local def ok0: set = $ 0 $;
 
-@_ local def okScopeN (bctx: set) (fr p: nat): wff =
-$ okReturnN bctx fr /\ s_ok
+@_ local def okScope (bctx: set) (fr p: nat): wff =
+$ okReturn bctx fr /\ len (epi_regs (pctx_epi bctx)) = len (fr_pushed fr) /\
+  s_ok
     (bctx_labelGroups bctx @' gctx_content bctx @' pctx_epi bctx @' fr @' p)
-    (gctx_result bctx) $; -- TODO
+    (gctx_result bctx) $;
 
 @_ local def okAsmd (bctx code: set) (p x y: nat): wff =
 $ okBCtx bctx /\
   E. s (y = x + len s /\ text_start + p + y e. u64 /\
-  sublistAt (p + x) (gctx_content bctx) s /\ p, s, x e. code) $;
+    sublistAt (p + x) (gctx_content bctx) s /\ p, s, x e. code) $;
 
 @_ @mmc-th local def okCode (bctx tctx1 code tctx2: set): wff =
-$ A. p A. x A. y A. fr (okAsmd bctx code p x y -> okScopeN bctx fr p ->
+$ A. p A. x A. y A. fr (okAsmd bctx code p x y -> okScope bctx fr p ->
   okCodeN bctx tctx2 fr (p + y) -> okCodeN bctx tctx1 fr (p + x)) $;
 
 theorem okCode_rev:
@@ -542,7 +577,7 @@ $ epi_ok epi -> instEpilogue epi == code $;
   (h2: $ checkRet bctx tctx ret $)
   (h3: $ okEpilogue epi code $):
   $ okCode bctx tctx code ok0 $ =
-'(okCode_rev @ mpbid (okCodeeq3d @ mpbir (okEpilogueeq1 @ anr h1) h3) @ a1i @ h2 (anl h1));
+'(okCode_rev @ mpbid (anwr @ okCodeeq3d @ mpbir (okEpilogueeq1 @ anr h1) h3) @ a1i @ h2 (anl h1));
 
 @mmc-th theorem okEpilogue_free
   (h: $ okEpilogue epi code $):
diff --git a/examples/compiler-old.mm1 b/examples/compiler-old.mm1
index a4b48350..54b33733 100644
--- a/examples/compiler-old.mm1
+++ b/examples/compiler-old.mm1
@@ -1853,20 +1853,20 @@ theorem L_or_sstop: $ L_or L1 L2 C_ L_top $ =
     sylc s_eor ,(f 'lemax1) ,(f 'lemax2)));
 
 --| An overlapping composition of layouts.
-@_ local def stack_layout (sp n: nat) (L: set): set =
+@_ local def stack_layoutOLD (sp n: nat) (L: set): set =
 $ E.s lo e. _V, E.s sz e. _V, (
     ^s (lo + sz e. u64 /\ lo + 2 ^ 12 + n <= lo + sz) /\s
     RSP >->r (lo + sz -_64 sp) *s L_seq L_pad L @' lo @' lo @' sz) $;
 
 --| The portion of the layout that we always want to know in any hoare triple.
---| `main_layout c sp ip` means that the code `c` is at `text_start`,
+--| `main_layoutOLD c sp ip` means that the code `c` is at `text_start`,
 --| the instruction pointer at `ip`, and the flags are assigned to an arbitrary value
 --| (i.e. we are permitted to clobber them).
 --| Additionally, the stack is laid out according to stack layout `L`
 --| (see the `L_*` functions) with at least `n` spare bytes left in the stack frame;
 --| `sp` is the value of the stack pointer relative to the stack layout.
-@_ local def main_layout (c sp ip n L): set =
-$ text_start >=>c c *s RIP>-> ip *s s_OK *s flags>->. *s stack_layout sp n L $;
+@_ local def main_layoutOLD (c sp ip n L): set =
+$ text_start >=>c c *s RIP>-> ip *s s_OK *s flags>->. *s stack_layoutOLD sp n L $;
 
 --| The correctness predicate for a function call.
 --| * `T`: A global parameter, the correctness predicate on final IO
@@ -1882,8 +1882,8 @@ $ text_start >=>c c *s RIP>-> ip *s s_OK *s flags>->. *s stack_layout sp n L $;
 --| Both `P` and `Q` are allowed to depend on common logical variables `vs`.
 @_ local def func_ok (T c ip P Q): wff =
 $ A. vs A. ret (ret e. u64 -> hoare T
-    (main_layout c 8 ip (2 ^ 12) (L_1 (u64Bytes ret)) *s P @' vs)
-    (main_layout c 0 ret 8 L_emp *s Q @' vs)) $;
+    (main_layoutOLD c 8 ip (2 ^ 12) (L_1 (u64Bytes ret)) *s P @' vs)
+    (main_layoutOLD c 0 ret 8 L_emp *s Q @' vs)) $;
 
 --| The correctness predicate for a jump target.
 --| * `T, c`: Global parameters
@@ -1900,7 +1900,7 @@ $ A. vs A. ret (ret e. u64 -> hoare T
 --|
 --| Both `L` and `P` are allowed to depend on common logical variables `vs`.
 @_ local def jump_ok (T c sp fr ip L P): wff =
-$ s_ok (sn fr *s (main_layout c sp ip 8 L *s P)) T $;
+$ s_ok (sn fr *s (main_layoutOLD c sp ip 8 L *s P)) T $;
 
 theorem stack_dealloc
   (h2: $ G -> jump_ok T c sp fr ip L2 P $)
@@ -1916,7 +1916,7 @@ theorem hoareCfg_jump_ok {k}
   (ha: $ G -> decode ast l $)
   (hj: $ G -> jump_ok T c sp2 fr ip3 L2 P2 $)
   (h4: $ G -> hoareCfg k {k2 | execXAST k ast k2}
-    (main_layout c sp ip2 8 L *s P) (main_layout c sp2 ip3 8 L2 *s P2) $):
+    (main_layoutOLD c sp ip2 8 L *s P) (main_layoutOLD c sp2 ip3 8 L2 *s P2) $):
   $ G -> jump_ok T c sp fr ip L P $ =
 (focus
   (have 'H '(s_code_assembledOLD hc))
@@ -2012,7 +2012,7 @@ theorem sub_rsp_ok
 --   (ip: nat) -- the current location of the instruction pointer
 --   (L: set) -- the stack layout at this point
 --   (P: set) = -- the precondition for flow into this point
--- $ s_ok (sn fr *s (main_layout c sp ip 8 L *s P)) T $;
+-- $ s_ok (sn fr *s (main_layoutOLD c sp ip 8 L *s P)) T $;
 
 -- A type ty consists of:
 -- * a separating proposition [v : ty] which gives truth conditions for "v has type ty",
@@ -2121,7 +2121,7 @@ $ S\ vs, (E.s a e. _V, (has_ty a (ty @' vs) *s
 --       vs) $):
 --   $ G -> s_ok
 --     (sn fr *s
---       (main_layout prog 8 adder (2 ^ 12) (L_1 (toBytes 8 ret)) *s
+--       (main_layoutOLD prog 8 adder (2 ^ 12) (L_1 (toBytes 8 ret)) *s
 --         v_sep (v_reg x7 (vn x0) v_ty_u32) (v_reg x6 (vn x1) v_ty_u32) @' vs))
 --     progT $ =
 -- (focus
diff --git a/examples/test3.mm1 b/examples/test3.mm1
new file mode 100644
index 00000000..ab0d865b
--- /dev/null
+++ b/examples/test3.mm1
@@ -0,0 +1 @@
+import "test.mm1";
diff --git a/examples/x86.mm1 b/examples/x86.mm1
index 3ddf72ef..2eb4afe0 100644
--- a/examples/x86.mm1
+++ b/examples/x86.mm1
@@ -4332,7 +4332,7 @@ do (mk-cases-eqns execXAST_clauses @ match-fn* @ (rvars ((name . dummies) stmt)
     '((k nat ())) (map (fn (x) '(,x nat ())) vars) '((k2 nat ())))
   (def stmt $ execXAST k ,'(,name . ,vars) k2 <-> ,stmt $)
   (add-tac-thm! thname bis () stmt 'pub @ fn ()
-    (named '(trud ,(ctx ,eqtac)))));
+    (named '(trud ,(ctx eqtac)))));
 
 theorem splitSum
   (h0: $ G /\ a // 2 e. A -> a = b0 (a // 2) -> p $)
@@ -4419,7 +4419,7 @@ pub theorem execXAST_T (k ast k2: nat):
     '(iand _ @ sylan destEA_T an4l anlr)
     '(iand _ @ anwr @ rsyl anlr @ anrd readEA_T64)
     '(iand _ @ anwr @ anwll @ anrd readEA_T64)
-    '(iand an3l @ anllr))
+    '(iand an3l anllr))
   (focus -- Mul
     '(eexd @ eexd @ eexd @ impd @ exp @ eord _ _)
     (focus
diff --git a/mm0-lean4/.gitignore b/mm0-lean4/.gitignore
new file mode 100644
index 00000000..bfb30ec8
--- /dev/null
+++ b/mm0-lean4/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/mm0-lean4/MM0.lean b/mm0-lean4/MM0.lean
new file mode 100644
index 00000000..9648f7d9
--- /dev/null
+++ b/mm0-lean4/MM0.lean
@@ -0,0 +1 @@
+import MM0.Basic
diff --git a/mm0-lean4/MM0/Basic.lean b/mm0-lean4/MM0/Basic.lean
new file mode 100644
index 00000000..89fd52a4
--- /dev/null
+++ b/mm0-lean4/MM0/Basic.lean
@@ -0,0 +1,318 @@
+noncomputable section
+namespace MMCC
+
+def Var := Nat
+
+def RegNum := Fin 16 deriving LT
+def RSP : RegNum := (4 : Fin 16)
+def Int.toUInt64 (n : Int) : UInt64 :=
+  (n.emod UInt64.size).toNat.toUInt64
+
+def textStart : UInt64 := 0x400078
+
+instance : Coe String (List UInt8) := ⟨fun s => s.toUTF8.toList⟩
+
+axiom Heap : Type
+
+axiom SProp : Type
+
+axiom Result : Type
+
+axiom UInt64.bytes : UInt64 → List UInt8
+
+axiom Result.ok : SProp → Result → Prop
+axiom SProp.false : SProp
+axiom SProp.emp : SProp
+axiom SProp.heap : Heap → SProp
+axiom SProp.sep : SProp → SProp → SProp
+axiom SProp.and : SProp → SProp → SProp
+axiom SProp.or : SProp → SProp → SProp
+axiom SProp.lift : Prop → SProp
+
+instance : Coe Prop SProp := ⟨SProp.lift⟩
+infixl:72 " ∗ " => SProp.sep
+infixl:70 " ∧ₛ " => SProp.and
+infixl:70 " ∨ₛ " => SProp.or
+
+axiom SProp.exists : ∀ {α}, (α → SProp) → SProp
+notation:75 "∃ₛ " x ", " p => SProp.exists fun x => p
+
+axiom SProp.reg : RegNum → Nat → SProp
+infix:80 " ↦ᵣ " => SProp.reg
+
+axiom SProp.code : UInt64 → List UInt8 → SProp
+infix:80 " ↦ᶜ " => SProp.code
+
+axiom SProp.block : UInt64 → List UInt8 → SProp
+infix:80 " ↦ " => SProp.block
+
+axiom SProp.ip : UInt64 → SProp
+prefix:80 "RIP ↦ " => SProp.ip
+axiom SProp.flagsNone : SProp
+notation "flags ↦ -" => SProp.flagsNone
+
+axiom SProp.blockS (lo a n : Nat) : SProp
+notation:80 a " ↦[" lo "] -×" n:80 => SProp.blockS lo a n
+
+axiom SProp.OK : SProp
+
+def Valuation := Var → Nat
+def VProp := Valuation → SProp
+def VProp.emp : VProp := fun _ => .emp
+def Ty := Valuation → Nat → SProp
+def Expr := Valuation → Nat
+def Ty.unit : Ty := fun _ _ => .emp
+def Ty.false : Ty := fun _ _ => .false
+def asTy (P : VProp) : Ty := fun vs _ => P vs
+def isTyped (e : Expr) (ty : Ty) : VProp := fun vs => ty vs (e vs)
+def isHyp (ty : Ty) : VProp := fun vs => ty vs 0
+def Ty.typed (e : Expr) (ty : Ty) : Ty := asTy (isTyped e ty)
+def eVar (v : Var) : Expr := fun vs => vs v
+axiom Ty.moved : Ty → Ty
+
+inductive ReturnABI
+  | noRet
+
+axiom ReturnABI.returnType : ReturnABI → SProp
+
+inductive Epilogue
+  | free : Nat → Epilogue → Epilogue
+  | pop : RegNum → Epilogue → Epilogue
+  | ret : Epilogue
+
+def Epilogue.value : Epilogue → Option (List RegNum × Nat)
+  | .ret => some ([], 0)
+  | .free n epi => do
+    let (regs, 0) ← epi.value | none
+    unless n != 0 do none
+    some (regs, n)
+  | .pop reg epi => do
+    let (regs, 0) ← epi.value | none
+    some (reg :: regs, 0)
+
+structure Epilogue' where
+  val : Epilogue
+  regs : List RegNum
+  sp : Nat
+  ok : val.value = some (regs, sp)
+
+structure GCtx where
+  content : List UInt8
+  fileSz : UInt64
+  memSz : UInt64
+  result : Result
+  len_eq : content.length = fileSz.toNat
+  le : fileSz ≤ memSz
+  lt : textStart.toNat + memSz.toNat < UInt64.size
+
+structure PCtx1 where
+  ret : ReturnABI
+  epi : Epilogue'
+  se : Bool
+
+structure PCtx extends GCtx, PCtx1
+
+def BlockLoc := Option UInt64
+
+structure Frame where
+  frame : Heap
+  retAddr : UInt64
+  pushed : List UInt64
+  lo : Nat
+  top : Nat
+  le : lo ≤ top
+  lt : top < UInt64.size
+
+def Frame.stackBot (fr : Frame) (sp n : Nat) : SProp :=
+  (fr.lo + 2^12 + n ≤ sp) ∧ₛ
+  fr.lo ↦[fr.lo] -×(sp - fr.lo)
+
+def Frame.stackLayout'
+    (fr : Frame) (n sz : Nat) (pushed : List UInt8) (L : Nat → Nat → SProp) : SProp :=
+  let sp := fr.top - pushed.length - sz
+  RSP ↦ᵣ sp ∗ fr.stackBot sp n ∗ L fr.lo sp ∗ (sp + sz).toUInt64 ↦ pushed
+
+def Frame.stackLayout (fr : Frame) (n sz : Nat) (L : Nat → Nat → SProp) : SProp :=
+  fr.stackLayout' n sz ((fr.pushed ++ [fr.retAddr]).bind UInt64.bytes) L
+
+def mainLayout (content : List UInt8) (ip : UInt64) : SProp :=
+  textStart ↦ᶜ content ∗ RIP ↦ ip ∗ SProp.OK ∗ flags ↦ -
+
+def okReturn (pctx : PCtx) (fr : Frame) : Prop :=
+  pctx.result.ok <| SProp.heap fr.frame ∗
+    (mainLayout pctx.content fr.retAddr ∗
+      fr.stackLayout' 8 0 [] (fun _ _ => .emp) ∗
+      pctx.ret.returnType)
+
+inductive VCtx where
+  | emp
+  | var (n : Option Nat) (ty : Ty)
+  | and (A B : VCtx)
+
+def VCtx.eval : VCtx → VProp
+  | .emp => .emp
+  | .var (some n) ty => isTyped (eVar n) ty
+  | .var none ty => isHyp ty
+  | .and A B => fun vs => A.eval vs ∗ B.eval vs
+
+inductive VCtx.OK1 : VCtx → Prop where
+  | var : VCtx.OK1 (.var n ty)
+  | and : VCtx.OK1 A → VCtx.OK1 B → VCtx.OK1 (.and A B)
+
+inductive VCtx.OK : VCtx → Prop where
+  | emp : VCtx.OK .emp
+  | nonempty : VCtx.OK1 A → VCtx.OK A
+
+inductive VCtx.push : VCtx → VCtx → VCtx → Prop where
+  | one : VCtx.push .emp A A
+  | suc : VCtx.push vctx A (.and vctx A)
+  | rot : VCtx.push vctx ty (.and (.and A B) C) → VCtx.push vctx ty (.and A (.and B C))
+
+inductive VCtx.get : VCtx → VCtx → Prop where
+  | push : VCtx.push A ty A' → VCtx.get A' ty
+  | l : VCtx.get A ty → VCtx.get (.and A B) ty
+  | r : VCtx.get B ty → VCtx.get (.and A B) ty
+  | rot : VCtx.get (.and (.and A B) C) ty → VCtx.get (.and A (.and B C)) ty
+
+inductive isMoved : Ty → Ty → Prop where
+
+inductive VCtx.take : VCtx → VCtx → VCtx → Prop where
+  | move : isMoved ty moved → VCtx.take (.var n ty) (.var n ty) (.var n moved)
+  | ref : isMoved ty moved → VCtx.take (.var n ty) (.var n moved) (.var n ty)
+  | l : VCtx.take A ty A' → VCtx.take (.and A B) ty (.and A' B)
+  | r : VCtx.take B ty B' → VCtx.take (.and A B) ty (.and A B')
+
+inductive StackLayout where
+  | emp
+  | pad (off n : Nat)
+  | and (A B : StackLayout)
+
+def StackLayout.eval : StackLayout → Valuation → Nat → Nat → SProp
+  | .emp, _, _, _ => .emp
+  | .pad off n, _, lo, sp => (sp + off) ↦[lo] -×n
+  | .and A B, vs, lo, sp => A.eval vs lo sp ∗ B.eval vs lo sp
+
+inductive MCtx where
+  | emp
+  | free (r : RegNum)
+  | stkFree (off n : Nat)
+  | reg (reg : RegNum) (val : Expr)
+  | and (A B : MCtx)
+
+def MCtx.lctx : MCtx → Valuation → SProp
+  | .emp, _ => .emp
+  | .free r, _ => ∃ₛ v, r ↦ᵣ v
+  | .stkFree _ _, _ => .emp
+  | .reg r val, vs => r ↦ᵣ val vs
+  | .and A B, vs => A.lctx vs ∗ B.lctx vs
+
+def MCtx.mctx : MCtx → StackLayout
+  | .emp => .emp
+  | .free _ => .emp
+  | .stkFree off n => .pad off n
+  | .reg _ _ => .emp
+  | .and A B => .and A.mctx B.mctx
+
+inductive MCtx.OKReg : MCtx → RegNum → RegNum → Prop where
+  | emp : MCtx.OKReg .emp (0:Fin _) (0:Fin _)
+  | free : MCtx.OKReg (.free r) r r
+  | reg : MCtx.OKReg (.reg r v) r r
+  | and : MCtx.OKReg A a b → b < c → MCtx.OKReg A c d → MCtx.OKReg (A.and B) a d
+
+inductive MCtx.OKStack : MCtx → Prop where
+
+inductive MCtx.OK : MCtx → Prop where
+  | nostack : MCtx.OKReg A a b → OK A
+  | stack : MCtx.OKReg A a b → MCtx.OKStack B → OK (.and A B)
+
+structure TCtx where
+  vctx : VCtx
+  vctxSz : Nat
+  mctx : MCtx
+
+def TCtx.type (tctx : TCtx) : VProp :=
+  fun vs => tctx.vctx.eval vs ∗ tctx.mctx.lctx vs
+
+def TCtx.layout (tctx : TCtx) : StackLayout := tctx.mctx.mctx
+
+inductive TCtx.pushVar : TCtx → Ty → TCtx → Prop where
+  | mk {vctx mctx} : VCtx.push vctx (.var (some sz) ty) vctx' →
+    TCtx.pushVar ⟨vctx, sz, mctx⟩ ty ⟨vctx', sz + 1, mctx⟩
+
+inductive TCtx.pushHyp : TCtx → Ty → TCtx → Prop where
+  | mk {vctx mctx} : VCtx.push vctx (.var none ty) vctx' →
+    TCtx.pushHyp ⟨vctx, sz, mctx⟩ ty ⟨vctx', sz, mctx⟩
+
+inductive TCtx.readHyp : TCtx → Ty → Prop where
+  | unit : TCtx.readHyp tctx .unit
+  | var {vctx} : vctx.get (.var n ty) → TCtx.readHyp ⟨vctx, n, tctx⟩ ty
+
+axiom Variant : Type
+axiom Variant.eval : Variant → Valuation → Nat → Prop
+
+inductive LabelGroup
+  | and : LabelGroup → LabelGroup → LabelGroup
+  | one : BlockLoc → Variant → TCtx → LabelGroup
+
+def LabelGroup.eval : LabelGroup → Valuation → Nat → List UInt8 → Epilogue' → Frame → Nat → SProp
+  | .one x var tctx, vs, v, c, epi, fr, p => (SProp.heap fr.frame ∗
+    (match x with
+    | some x => mainLayout c (textStart + p.toUInt64 + x)
+    | none => ∃ₛ ip, mainLayout c ip) ∗
+    var.eval vs v ∗
+    fr.stackLayout 8 epi.sp (tctx.layout.eval vs) ∗ tctx.type vs)
+  | .and a b, vs, v, c, epi, fr, p => a.eval vs v c epi fr p ∨ₛ b.eval vs v c epi fr p
+
+inductive findLabel : LabelGroup → BlockLoc → Variant → TCtx → Prop
+  | one : findLabel (.one x var tctx) x var tctx
+  | l : findLabel A x var tctx → findLabel (.and A B) x var tctx
+  | r : findLabel B x var tctx → findLabel (.and A B) x var tctx
+
+def LabelGroups := List (Expr × LabelGroup)
+
+def LabelGroups.eval : LabelGroups → List UInt8 → Epilogue' → Frame → Nat → SProp
+  | [], _, _, _, _ => .false
+  | (var, ls) :: labs, c, epi, fr, p =>
+    (∃ₛ vs, ls.eval vs (var vs) c epi fr p) ∨ₛ eval labs c epi fr p
+
+structure BCtx extends PCtx where
+  labelGroups : LabelGroups
+
+def okCodeN (bctx : BCtx) (tctx : TCtx) (fr : Frame) (ip : Nat) : Prop :=
+  bctx.result.ok <| SProp.heap fr.frame ∗ (
+    mainLayout bctx.content (textStart + ip.toUInt64) ∗
+    ∃ₛ vs, fr.stackLayout 8 bctx.epi.sp (tctx.layout.eval vs) ∗ tctx.type vs)
+
+inductive LAsm where
+  | nil
+  | at (x : Nat) (A : LAsm)
+  | entry (p : Nat) (A : LAsm)
+  | seq (A B : LAsm)
+
+inductive LAsm.eval : LAsm → Nat → List UInt8 → Nat → Prop
+  | nil : eval .nil p [] x
+  | at : eval A p s x → eval (.at x A) p s x
+  | entry : eval A p s x → eval (.entry p A) p s x
+  | seq : eval A p t₁ x → eval B p t₂ (x + t₁.length) → eval (.seq A B) p (t₁ ++ t₂) x
+
+inductive GAsm where
+  | proc (p : Nat) (A : LAsm)
+  | seq (A B : GAsm)
+
+inductive GAsm.eval : GAsm → List UInt8 → Nat → Prop
+  | proc : A.eval p t₁ 0 → t₁ ≠ [] → eval (.proc p A) (t₁ ++ t₂) x
+  | seq : eval A t₁ x → eval B t₂ (x + t₁.length) → eval (.seq A B) (t₁ ++ t₂) x
+
+def sublistAt (n : Nat) (L₁ L₂ : List α) : Prop := ∃ l r, L₁ = l ++ L₂ ++ r ∧ l.length = n
+
+def okScope (bctx : BCtx) (fr : Frame) (p : Nat) : Prop :=
+  okReturn bctx.toPCtx fr ∧ bctx.epi.regs.length = fr.pushed.length ∧
+  bctx.result.ok (bctx.labelGroups.eval bctx.content bctx.epi fr p)
+
+def okAsmd (bctx : BCtx) (code : LAsm) (p x y : Nat) : Prop :=
+  ∃ s, y = x + s.length ∧ textStart.toNat + p + y < UInt64.size ∧
+    sublistAt (p + x) bctx.content s ∧ code.eval p s x
+
+def okCode (bctx : BCtx) (tctx : TCtx) (code : LAsm) (tctx' : TCtx) : Prop :=
+  ∀ p x y fr, okAsmd bctx code p x y → okScope bctx fr p →
+    okCodeN bctx tctx' fr (p + y) → okCodeN bctx tctx fr (p + x)
diff --git a/mm0-lean4/README.md b/mm0-lean4/README.md
new file mode 100644
index 00000000..4edda2fd
--- /dev/null
+++ b/mm0-lean4/README.md
@@ -0,0 +1,3 @@
+# mm0-lean4
+
+Scratch files written in Lean 4
diff --git a/mm0-lean4/lake-manifest.json b/mm0-lean4/lake-manifest.json
new file mode 100644
index 00000000..1a6df810
--- /dev/null
+++ b/mm0-lean4/lake-manifest.json
@@ -0,0 +1,5 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages": [],
+ "name": "mm0",
+ "lakeDir": ".lake"}
diff --git a/mm0-lean4/lakefile.toml b/mm0-lean4/lakefile.toml
new file mode 100644
index 00000000..66707fac
--- /dev/null
+++ b/mm0-lean4/lakefile.toml
@@ -0,0 +1,6 @@
+name = "mm0"
+version = "0.1.0"
+defaultTargets = ["MM0"]
+
+[[lean_lib]]
+name = "MM0"
diff --git a/mm0-lean4/lean-toolchain b/mm0-lean4/lean-toolchain
new file mode 100644
index 00000000..4f86f953
--- /dev/null
+++ b/mm0-lean4/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.13.0
diff --git a/mm0-rs/src/joiner.rs b/mm0-rs/src/joiner.rs
index 08b8b01d..6a1444b5 100644
--- a/mm0-rs/src/joiner.rs
+++ b/mm0-rs/src/joiner.rs
@@ -87,8 +87,8 @@ impl<W: Write> Joiner<W> {
 }
 
 fn join_with_header(comments: bool, header: bool, mut w: impl Write, file: FileRef) -> io::Result<()> {
-  let mut buf = vec![];
   if comments && header {
+    let mut buf = vec![];
     let mut joiner = Joiner::new(comments, &mut buf);
     joiner.write(file.clone())?;
     writeln!(w, "\
diff --git a/mm0-rs/src/mmc/proof/compiler.rs b/mm0-rs/src/mmc/proof/compiler.rs
index 03df875c..963b2511 100644
--- a/mm0-rs/src/mmc/proof/compiler.rs
+++ b/mm0-rs/src/mmc/proof/compiler.rs
@@ -938,7 +938,7 @@ impl ProcProver<'_> {
   /// Given `ty`, `|- okReadHypVCtx vctx ty`, returns `|- okReadHyp tctx ty`
   fn read_hyp_from_vctx(&mut self, tctx: ProofId, ty: ProofId, th: ProofId) -> ProofId {
     app_match!(self.thm, let (mkTCtx vctx n mctx) = tctx);
-    thm!(self.thm, okReadHypI(mctx, n, ty, vctx, th): okReadHyp[tctx, ty])
+    thm!(self.thm, okReadHypI(mctx, n, ty, vctx, th): okReadHyp[tctx, ty]) // TODO
   }
 
   /// Returns `(ty, |- okReadHyp tctx ty)`
diff --git a/mm0-rs/src/mmc/proof/mod.rs b/mm0-rs/src/mmc/proof/mod.rs
index 205f64f8..65e00200 100644
--- a/mm0-rs/src/mmc/proof/mod.rs
+++ b/mm0-rs/src/mmc/proof/mod.rs
@@ -452,7 +452,7 @@ impl Mangler {
         and satisfy the global exit proposition (or fail).",
         ProcName(None), self.mangle(Name::GCtx)),
 
-      Name::ProgOkThm => format!("The main correctness theorem for {}. \
+      Name::ProgOkThm => format!("The main correctness theorem for `{}`. \
         This theorem has the form `okProg elf prop`, where:\n\
         \n\
         * `elf` is the program binary\n\
@@ -482,8 +482,8 @@ pub(crate) fn render_proof(
     let mut thm = ProofDedup::new(pd, &[]);
     let u_gctx = thm.get_def0(elab, gctx);
     app_match!(thm, let (mkGCtx c fs ms ty) = u_gctx);
-    let [_, fss, hfs] = thm.parse_ubytes(7, fs);
-    let [_, mss, hms] = thm.parse_ubytes(7, ms);
+    let [_, fss, hfs] = thm.parse_ubytes(8, fs);
+    let [_, mss, hms] = thm.parse_ubytes(8, ms);
 
     let u_elf = app!(thm, (ELF_lit fss mss c));
     let (elf, _) = elab.env.add_term({
diff --git a/mm0-rs/src/mmc/proof/norm_num.rs b/mm0-rs/src/mmc/proof/norm_num.rs
index 3ab1a091..9b521f74 100644
--- a/mm0-rs/src/mmc/proof/norm_num.rs
+++ b/mm0-rs/src/mmc/proof/norm_num.rs
@@ -308,9 +308,21 @@ norm_split_bits! {
 }
 
 impl ProofDedup<'_> {
-  /// Proves `[k, s, |- parseUBytes k n s]`.
+  pub(super) fn sucs(&mut self, mut n: u8) -> ProofId {
+    let mut out = app!(self, (d0));
+    for _ in 0..n { out = app!(self, (suc out)) }
+    out
+  }
+
+  /// Proves `[k-1, s, |- parseUBytes (k-1) n s]`.
   pub(super) fn parse_ubytes(&mut self, k: u8, n: ProofId) -> [ProofId; 3] {
-    if k == 0 {
+    if k <= 8 && app_match!(self, n => { (h2n ((xn[0u8]))) => true, _ => false, }) {
+      let ek = self.sucs(k-1);
+      let s = app!(self, (padn[k]));
+      return [ek, s, thm!(self, parseUBytes_x00xn[k](): (parseUBytes ek n s))]
+    }
+    if k <= 1 {
+      debug_assert!(k == 1);
       let ek = app!(self, (dn[0u8]));
       app_match!(self, n => {
         (h2n a0) => {
diff --git a/mm0-rs/src/mmc/proof/predefs.rs b/mm0-rs/src/mmc/proof/predefs.rs
index a90cf8e4..0cb302cb 100644
--- a/mm0-rs/src/mmc/proof/predefs.rs
+++ b/mm0-rs/src/mmc/proof/predefs.rs
@@ -303,6 +303,8 @@ make_predefs! {
   parseUBytes01: ThmId => "parseUBytes01";
   parseUBytes02: ThmId => "parseUBytes02";
 
+  parseUBytes_x00xn[i: 8]: ThmId if i != 0 => format!("parseUBytes_x00x{i:x}");
+
   /// `parseIBytesPos (k n: nat) (s: string): wff`
   parseIBytesPos: TermId => "parseIBytesPos";
   parseIBytesPosS: ThmId => "parseIBytesPosS";