From 799b102cfe4e9e142d0039df4f63dbd8b203b4d0 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Mon, 25 Nov 2024 02:53:23 +0100
Subject: [PATCH] random acts of progress

---
 examples/compiler-new.mm1        | 149 ++++++++-------
 mm0-lean4/MM0/Basic.lean         | 305 +++++++++++++++++++++++++------
 mm0-rs/src/mmc/proof/compiler.rs |  71 ++++---
 mm0-rs/src/mmc/proof/predefs.rs  |   2 +
 4 files changed, 360 insertions(+), 167 deletions(-)

diff --git a/examples/compiler-new.mm1 b/examples/compiler-new.mm1
index 3f7f92de..af795f51 100644
--- a/examples/compiler-new.mm1
+++ b/examples/compiler-new.mm1
@@ -46,12 +46,13 @@ do (warn-unused-vars #f);
 
 @_ local def epi_ok (epi: nat): wff = $ epi != 0 $;
 @_ local def epi_regs (epi: nat): nat = $ fst (epi - 1) $;
-@_ local def epi_sp (epi: nat): nat = $ snd (epi - 1) $;
+@_ local def epi_sp_opt (epi: nat): nat = $ snd (epi - 1) $;
+@_ local def epi_sp (epi: nat): nat = $ epi_sp_opt epi - 1 $;
 
 @_ @mmc-th local def epiFree (n: nat) (epi: nat): nat =
-$ if (epi_ok epi /\ n != 0 /\ epi_sp epi = 0) (suc (epi_regs epi, n)) 0 $;
+$ if (epi_ok epi /\ epi_sp_opt epi = 0) (suc (epi_regs epi, suc n)) 0 $;
 @mmc-th local def epiPop (reg: hex) (epi: nat): nat =
-$ if (epi_ok epi /\ epi_sp epi = 0) (suc (reg : epi_regs epi, 0)) 0 $;
+$ if (epi_ok epi /\ epi_sp_opt 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.
@@ -131,7 +132,7 @@ local def mkFrame (fr ret pushed lo top: nat): nat = $ fr, (ret, pushed), lo, to
 $ 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 =
+@_ local def okFramePCtx (pctx: set) (fr: nat): wff =
 $ len (fr_pushed fr) = len (epi_regs (pctx_epi pctx)) $;
 
 @_ local def fr_frame (fr: nat): set =
@@ -237,36 +238,36 @@ $ s_ok
     soReturnType (pctx_ret pctx)))
   (gctx_result pctx) $;
 
-@_ local def okCodeN (bctx tctx: set) (fr ip: nat) =
+@_ local def okCodeP (c epi: nat) (tctx: set) (fr p ip vs: nat): set =
+$ fr_frame fr *s (
+    If (ip = 0)
+      (E.s y e. u64, mainLayout c y)
+      (mainLayout c (text_start + (p + (ip - 1)))) *s
+    stackLayout fr 8 (epi_sp epi) (tctx_layout tctx vs) *s
+    tctx_type tctx vs) $;
+
+@_ local def okCodeN (bctx tctx: set) (fr p ip: nat) =
 $ s_ok
-  (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)))
+  (E.s vs e. _V, okCodeP (gctx_content bctx) (pctx_epi bctx) tctx fr p ip 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 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;
+local def labelGroup1 (val ls: set): set = $ E.s vs e. _V, ls @' vs @' (val @ vs) $;
+@mmc-th local def labelGroup (val ls labs: set): set = $ labs \/s labelGroup1 val ls $;
+notation labelGroup (val ls labs: set): set = ($LG($:85) val ($,$:55) ls ($);$:0) labs;
 
-@mmc-th local def findLabels (labs: set) (var ls: set): wff = $ labelGroup1 var ls C_ labs $;
-@mmc-th theorem findLabels1: $ findLabels (LG(var, ls); labs) var ls $ = 'sorry;
-@mmc-th theorem findLabelsS (h: $ findLabels labs var ls $):
-  $ findLabels (LG(var, ls1); labs) var ls $ = 'sorry;
+@mmc-th local def findLabels (labs: set) (val ls: set): wff = $ labelGroup1 val ls C_ labs $;
+@mmc-th theorem findLabels1: $ findLabels (LG(val, ls); labs) val ls $ = 'sorry;
+@mmc-th theorem findLabelsS (h: $ findLabels labs val ls $):
+  $ findLabels (LG(val1, ls1); labs) val ls $ = 'sorry;
 
 --| `Labels.and : Labels -> Labels -> Labels`
 @mmc-th local def labelA (A B: set): set = $ A \/s B $;
 infixl labelA: $+L$ prec 20;
---| `Labels.one : BlockLoc -> Expr -> TCtx -> Labels`
-@mmc-th local def label1 (x: nat) (var tctx: set): set =
-$ 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)) $;
+--| `Labels.one : BlockLoc -> Variant -> TCtx -> Labels`
+@mmc-th local def label1 (ip: nat) (var tctx: set): set =
+$ S\ vs, S\ v, S\ c, S\ epi, S\ fr, S\ p, (^s (vs, v e. var) *s okCodeP c epi tctx fr p ip 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;
@@ -358,24 +359,23 @@ $ A. vs E. n tctx_type tctx vs =>*s ty @' vs @' n $;
 @mmc-th local def ok0: set = $ 0 $;
 
 @_ local def okScope (bctx: set) (fr p: nat): wff =
-$ okReturn bctx fr /\ len (epi_regs (pctx_epi bctx)) = len (fr_pushed fr) /\
+$ okReturn bctx fr /\
   s_ok
     (bctx_labelGroups bctx @' gctx_content bctx @' pctx_epi bctx @' fr @' p)
     (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 /\
+$ E. s (y = x + len s /\ text_start + p + y e. u64 /\
     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 -> okScope bctx fr p ->
-  okCodeN bctx tctx2 fr (p + y) -> okCodeN bctx tctx1 fr (p + x)) $;
+$ okBCtx bctx -> A. p A. x A. y A. fr (okFramePCtx bctx fr ->
+  okAsmd bctx code p x y -> okScope bctx fr p ->
+  okCodeN bctx tctx2 fr p (suc y) -> okCodeN bctx tctx1 fr p (suc x)) $;
 
 theorem okCode_rev:
   $ (okBCtx bctx -> okCode bctx tctx1 code tctx2) -> okCode bctx tctx1 code tctx2 $ =
-(named @ iterate 4 (fn (x) '(sylbir alim1 @ alimi ,x))
-  '(bi1i @ bitr3 impexp @ imeq1i @ bitr3 anass @ aneq1i anidm));
+(named 'imidm);
 
 @mmc-th theorem okCode_0: $ okCode bctx ok0 code ok0 $ = 'sorry;
 
@@ -392,21 +392,20 @@ theorem okCode_rev:
   $ okCode bctx tctx1 ASM0 tctx3 $ = 'sorry;
 
 @mmc-th local def okPrologue
-  (epi1 sp: nat) (mctx code: set) (epi2: nat) (mctx2: set): wff = $ sorry_wff $; -- TODO
+  (epi1: nat) (mctx code: set) (epi2: nat) (mctx2: set): wff = $ sorry_wff $; -- TODO
 
 @mmc-th theorem okPrologue_push
-  (h: $ sp + x8 = sp2 $)
-  (h2: $ pushMCtx mctx1 (FREE r) mctx2 $)
-  (h3: $ okPrologue (epiPop r epi) sp2 mctx2 code epi2 mctx3 $):
-  $ okPrologue epi sp mctx1 (instPush (IRM_reg r) +asm code) epi2 mctx3 $ =
+  (h1: $ pushMCtx mctx1 (FREE r) mctx2 $)
+  (h2: $ okPrologue (epiPop r epi) mctx2 code epi2 mctx3 $):
+  $ okPrologue epi mctx1 (instPush (IRM_reg r) +asm code) epi2 mctx3 $ =
 'sorry;
 
 @mmc-th theorem okPrologue_alloc0 (h1: $ okMCtx mctx $):
-  $ okPrologue epi sp mctx ASM0 epi mctx $ = 'sorry;
+  $ okPrologue epi mctx ASM0 epi mctx $ = 'sorry;
 
 @mmc-th theorem okPrologue_alloc
-  (h1: $ okMCtx mctx $) (h2: $ sp + n = m $) (h3: $ m < ,{2 ^ 12} $):
-  $ okPrologue epi sp mctx ,(instSub 'wSz64 RSP '(IRM_imm32 n))
+  (h1: $ okMCtx mctx $) (h2: $ n <= ,{{2 ^ 12} - 8} $):
+  $ okPrologue epi mctx ,(instSub 'wSz64 RSP '(IRM_imm32 n))
       (epiFree n epi) (mctx +M stkFREE x0 n) $ = 'sorry;
 
 @mmc-th local def okAssembled (pctx: set) (code: set): wff =
@@ -474,31 +473,33 @@ $ mctx2 == (mctx1 +M S\ vs, Sum (s_clob clob) L_emp) $;
   (h1: $ okAssembled (mkPCtx gctx (mkPCtx1 ret epi se)) (asmEntry start (prol +asm code)) $)
   (h2: $ accumArgs args vctx1 sz1 $)
   (h3: $ accumClob clob mctx1 mctx2 $)
-  (h4: $ okPrologue epiRet x0 mctx2 prol epi mctx3 $)
+  (h4: $ okPrologue epiRet mctx2 prol epi mctx3 $)
   (h5: $ okCode (mkBCtx (mkPCtx gctx (mkPCtx1 ret epi se)) LG0)
     (mkTCtx vctx1 sz1 mctx3) code ok0 $):
   $ okProc gctx start (mkArgs args mctx1) ret clob se $ = 'sorry;
 
-@mmc-th local def buildStart (gctx pctx: set) (fs ms: nat) (tctx: set): wff =
-$ pctx == mkPCtx gctx (mkPCtx1 noRet epiRet F.) /\ (
-    gctx_filesz gctx = fs -> gctx_memsz gctx = ms ->
-    F.) $; -- TODO
+@mmc-th local def buildStart (gctx pctx: set) (tctx: set): wff =
+$ pctx == mkPCtx gctx (mkPCtx1 noRet epiRet T.) /\
+  tctx == mkTCtx vctx0 x0 mctx0 $; -- TODO: global variables
 
 @mmc-th theorem buildStartI:
-  $ buildStart gctx (mkPCtx gctx (mkPCtx1 noRet epiRet F.)) fs ms tctx $ =
-'(iani eqsid sorry); -- TODO
+  $ buildStart gctx (mkPCtx gctx (mkPCtx1 noRet epiRet T.)) (mkTCtx vctx0 x0 mctx0) $ =
+'(iani eqsid eqsid);
 
-@mmc-th local def okStart (gctx: set) (fs ms: nat): wff =
-$ gctx_filesz gctx = fs -> gctx_memsz gctx = ms ->
-  F. $; -- TODO
+@mmc-th local def okStart (gctx: set): wff = $ sorry_wff $; -- TODO
 
 @mmc-th theorem okStartI
   (h1: $ okAssembled pctx (asmEntry x0 (ASM0 +asm code)) $)
-  (h2: $ buildStart gctx pctx fs ms tctx $)
+  (h2: $ buildStart gctx pctx tctx $)
   (h3: $ okCode (mkBCtx pctx LG0) tctx code ok0 $):
-  $ okStart gctx fs ms $ = 'sorry;
+  $ okStart gctx $ = 'sorry;
+
+@mmc-th local def okBlock (bctx: set) (ip: nat) (tctx: set): wff =
+$ okBCtx bctx -> A. p A. fr (okFramePCtx bctx fr -> okScope bctx fr p ->
+  okCodeN bctx tctx fr p ip) $;
 
-@mmc-th local def okBlock (bctx: set) (ip: nat) (tctx: set): wff = $ sorry_wff $; -- TODO
+theorem okBlock_rev: $ (okBCtx bctx -> okBlock bctx ip tctx) -> okBlock bctx ip tctx $ =
+(named 'imidm);
 
 @mmc-th theorem okBlock_weak
   (h1: $ okCode bctx tctx1 ASM0 tctx2 $)
@@ -536,29 +537,28 @@ $ gctx_filesz gctx = fs -> gctx_memsz gctx = ms ->
   (h2: $ addLabels bctx ls B $):
   $ addLabels bctx ls (A +L B) $ = 'sorry;
 
+@mmc-th local def variantValue (var val: set): wff = $ sorry_wff $; -- TODO
+
 @mmc-th theorem addLabels_1
   (h1: $ okAssembled pctx (asmAt ip code) $)
-  (h2: $ okCode (mkBCtx pctx (LG(var, ls); L)) tctx code ok0 $):
+  (h2: $ variantValue var val $)
+  (h3: $ okCode (mkBCtx pctx (LG(val, ls); L)) tctx code ok0 $):
   $ addLabels (mkBCtx pctx L) ls (label1 (suc ip) var tctx) $ = 'sorry;
 
 @mmc-th theorem addLabels_0
-  (h: $ okCode (mkBCtx pctx (LG(var, ls); L)) tctx ASM0 ok0 $):
+  (h1: $ variantValue var val $)
+  (h2: $ okCode (mkBCtx pctx (LG(val, ls); L)) tctx ASM0 ok0 $):
   $ addLabels (mkBCtx pctx L) ls (label1 0 var tctx) $ = 'sorry;
 
+--| The main induction lemma
 @mmc-th theorem okLabels_I (h: $ addLabels bctx ls ls $): $ okLabels bctx ls $ = 'sorry;
 
-@mmc-th local def getEpi (bctx ret: set) (epi: nat): wff =
-$ pctx_ret bctx == ret /\ pctx_epi bctx = epi $;
-
-@mmc-th theorem getEpiI: $ getEpi (mkBCtx (mkPCtx gctx (mkPCtx1 ret epi se)) labs) ret epi $ =
-'(iani pctx_ret_BI pctx_epi_BI);
-
 @_ local def instEpiRegs (regs: nat): set = $ sorry_set $; -- TODO
 theorem instEpiRegs0: $ instEpiRegs 0 == instRet $ = 'sorry;
 theorem instEpiRegsS: $ instEpiRegs (r : regs) == instPop r +asm instEpiRegs regs $ = 'sorry;
 
 @_ local def instEpilogue (epi: nat): set =
-$ If (epi_sp epi = 0)
+$ If (epi_sp_opt epi = 0)
   (instEpiRegs (epi_regs epi))
   (instAddN wSz64 ,RSP (IRM_imm32 (epi_sp epi)) +asm instEpiRegs (epi_regs epi)) $;
 
@@ -572,22 +572,29 @@ $ pctx_ret bctx == ret ->
 @_ @mmc-th local def okEpilogue (epi: nat) (code: set): wff =
 $ epi_ok epi -> instEpilogue epi == code $;
 
+@mmc-th local def getEpi (bctx ret code: set): wff =
+$ pctx_ret bctx == ret /\ okEpilogue (pctx_epi bctx) code $;
+
+@mmc-th theorem getEpiI (h: $ okEpilogue epi code $):
+  $ getEpi (mkBCtx (mkPCtx gctx (mkPCtx1 ret epi se)) labs) ret code $ =
+'(iani pctx_ret_BI @ mpbir (okEpilogueeq1 pctx_epi_BI) h);
+
 @mmc-th theorem okEpilogue_E
-  (h1: $ getEpi bctx ret epi $)
-  (h2: $ checkRet bctx tctx ret $)
-  (h3: $ okEpilogue epi code $):
+  (h1: $ getEpi bctx ret code $)
+  (h2: $ checkRet bctx tctx ret $):
   $ okCode bctx tctx code ok0 $ =
-'(okCode_rev @ mpbid (anwr @ okCodeeq3d @ mpbir (okEpilogueeq1 @ anr h1) h3) @ a1i @ h2 (anl h1));
+'(okCode_rev @ anwr @ mpbii (h2 @ anl h1) @ okCodeeq3d @ anr h1);
 
 @mmc-th theorem okEpilogue_free
   (h: $ okEpilogue epi code $):
   $ okEpilogue (epiFree n epi) (,(instAdd 'wSz64 RSP '(IRM_imm32 n)) +asm code) $ =
 (named @ focus
   (have 'h2 $ _ -> epi_regs (epiFree n epi) = epi_regs epi /\ epi_sp (epiFree n epi) = n $
-    '(sylib prth @ syl5eq fstsnd @ syl6eq sucsub1 @ subeq1d ifpos))
-  '(rsyl (con1 ifneg) @ eqstrd (syl Ifneg @ mpbird (neeq1d @ anrd h2) anlr) @
-    ASM_Aeqd (rsyl h2 ,eqtac) @
-    eqstrd (instEpiRegseqd @ anld h2) @ eqstr3d (anwr Ifpos) @ anwll h));
+    '(syl (anim2 @ syl6eq sucsub1 subeq1) @
+      sylib prth @ syl5eq fstsnd @ syl6eq sucsub1 @ subeq1d ifpos))
+  '(rsyl (con1 ifneg) @ eqstrd (syl Ifneg @ mpbiri peano1 @ neeq1d @
+      syl6eq sndpr @ sndeqd @ syl6eq sucsub1 @ subeq1d ifpos) @
+    ASM_Aeqd (rsyl h2 ,eqtac) @ eqstrd (instEpiRegseqd @ anld h2) @ eqstr3d (anwr Ifpos) @ anwl h));
 
 @mmc-th theorem okEpilogue_pop
   (h: $ okEpilogue epi code $):
@@ -600,7 +607,7 @@ $ epi_ok epi -> instEpilogue epi == code $;
 
 @mmc-th local def spillslot (v: nat): nat = $ sorry_nat $; -- TODO
 
-@mmc-th local def okRead (tctx1: set) (src v: nat): wff = $ F. $; -- TODO
+@mmc-th local def okRead (tctx1: set) (src v: nat): wff = $ sorry_wff $; -- TODO
 @mmc-th local def okWrite (tctx1: set) (dst v: nat) (tctx2: set): wff = $ sorry_wff $; -- TODO
 
 @mmc-th theorem ok_movRR
@@ -729,7 +736,7 @@ $ isBasicElfN elf /\ A. k (initialConfigN elf k -> terminates_ensuring k T) $;
 @mmc-th local def okProg (elf: string) (T: set): wff = $ okProgN elf T $;
 
 @mmc-th theorem okProgI
-  (h1: $ okStart (mkGCtx c fs ms T) fs ms $)
+  (h1: $ okStart (mkGCtx c fs ms T) $)
   (hfs: $ parseUBytes ,(sucs 7) fs fss $)
   (hms: $ parseUBytes ,(sucs 7) ms mss $):
   $ okProg (ELF_lit fss mss c) T $ = 'sorry;
diff --git a/mm0-lean4/MM0/Basic.lean b/mm0-lean4/MM0/Basic.lean
index 89fd52a4..a72f2b91 100644
--- a/mm0-lean4/MM0/Basic.lean
+++ b/mm0-lean4/MM0/Basic.lean
@@ -75,26 +75,24 @@ inductive ReturnABI
 
 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)
+inductive EpilogueR where
+  | pop : RegNum → EpilogueR → EpilogueR
+  | ret : EpilogueR
+
+inductive Epilogue where
+  | free : Nat → EpilogueR → Epilogue
+  | nostack : EpilogueR → Epilogue
+
+def EpilogueR.regs : EpilogueR → List RegNum
+  | .ret => []
+  | .pop reg epi => reg :: epi.regs
+
+def Epilogue.regs : Epilogue → List RegNum
+  | .free _ epi | .nostack epi => epi.regs
+
+def Epilogue.sp : Epilogue → Nat
+  | .free n _ => n
+  | .nostack _ => 0
 
 structure GCtx where
   content : List UInt8
@@ -107,12 +105,12 @@ structure GCtx where
 
 structure PCtx1 where
   ret : ReturnABI
-  epi : Epilogue'
+  epi : Epilogue
   se : Bool
 
 structure PCtx extends GCtx, PCtx1
 
-def BlockLoc := Option UInt64
+def BlockLoc := Option Nat
 
 structure Frame where
   frame : Heap
@@ -149,10 +147,12 @@ inductive VCtx where
   | var (n : Option Nat) (ty : Ty)
   | and (A B : VCtx)
 
+@[match_pattern] def VCtx.hyp := VCtx.var none
+
 def VCtx.eval : VCtx → VProp
   | .emp => .emp
   | .var (some n) ty => isTyped (eVar n) ty
-  | .var none ty => isHyp ty
+  | .hyp ty => isHyp ty
   | .and A B => fun vs => A.eval vs ∗ B.eval vs
 
 inductive VCtx.OK1 : VCtx → Prop where
@@ -192,38 +192,78 @@ def StackLayout.eval : StackLayout → Valuation → Nat → Nat → SProp
   | .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
+inductive MCtxR where
   | emp
+  | false
   | free (r : RegNum)
-  | stkFree (off n : Nat)
   | reg (reg : RegNum) (val : Expr)
-  | and (A B : MCtx)
+  | and (A B : MCtxR)
 
-def MCtx.lctx : MCtx → Valuation → SProp
+inductive MCtxR.OK : MCtxR → RegNum → RegNum → Prop where
+  | emp : MCtxR.OK .emp (0:Fin _) (0:Fin _)
+  | free : MCtxR.OK (.free r) r r
+  | reg : MCtxR.OK (.reg r v) r r
+  | and : MCtxR.OK A a b → b < c → MCtxR.OK A c d → MCtxR.OK (A.and B) a d
+
+def MCtxR.eval : MCtxR → Valuation → SProp
   | .emp, _ => .emp
+  | .false, _ => .false
   | .free r, _ => ∃ₛ v, r ↦ᵣ v
-  | .stkFree _ _, _ => .emp
   | .reg r val, vs => r ↦ᵣ val vs
-  | .and A B, vs => A.lctx vs ∗ B.lctx vs
+  | .and A B, vs => A.eval vs ∗ B.eval 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 MCtxS where
+  | free (off n : Nat)
+  | and (A B : MCtxS)
+
+inductive MCtx where
+  | nostack : MCtxR → MCtx
+  | stack : MCtxR → MCtxS → MCtx
+
+def MCtx.R : MCtx → MCtxR
+  | .nostack r | .stack r _ => r
+
+def MCtxS.layout : MCtxS → StackLayout
+  | .free off n => .pad off n
+  | .and A B => .and A.layout B.layout
 
-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
+def MCtx.layout : MCtx → StackLayout
+  | .nostack _ => .emp
+  | .stack _ s => s.layout
 
-inductive MCtx.OKStack : MCtx → Prop where
+inductive MCtxS.OK : MCtxS → 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)
+  | nostack : MCtxR.OK A a b → OK (.nostack A)
+  | stack : MCtxR.OK A a b → MCtxS.OK B → OK (.stack A B)
+
+inductive MCtxR.push : MCtxR → MCtxR → MCtxR → Prop
+  | emp : MCtxR.push .emp A A
+  | oneL : MCtxR.push A B (.and B A)
+  | oneR : MCtxR.push A B (.and A B)
+  | R : MCtxR.push B val B' → MCtxR.push (.and A B) val (.and A B')
+  | L : MCtxR.push A val A' → MCtxR.push (.and A B) val (.and A' B)
+  | rotL : MCtxR.push M val (.and A (.and B C)) → MCtxR.push M val (.and (.and A B) C)
+  | rotR : MCtxR.push M val (.and (.and A B) C) → MCtxR.push M val (.and A (.and B C))
+
+inductive MCtxS.push : MCtxS → MCtxS → MCtxS → Prop
+  | oneL : MCtxS.push A B (.and B A)
+  | oneR : MCtxS.push A B (.and A B)
+  | R : MCtxS.push B val B' → MCtxS.push (.and A B) val (.and A B')
+  | L : MCtxS.push A val A' → MCtxS.push (.and A B) val (.and A' B)
+  | rotL : MCtxS.push M val (.and A (.and B C)) → MCtxS.push M val (.and (.and A B) C)
+  | rotR : MCtxS.push M val (.and (.and A B) C) → MCtxS.push M val (.and A (.and B C))
+
+inductive MCtxInsert where
+  | free (r : RegNum)
+  | reg (reg : RegNum) (val : Expr)
+  | stkFree (off n : Nat)
+
+inductive MCtx.push : MCtx → MCtxR ⊕ MCtxS → MCtx → Prop
+  | reg : MCtxR.push A val A' → MCtx.push (.nostack A) (.inl val) (.nostack A')
+  | reg' : MCtxR.push A val A' → MCtx.push (.stack A B) (.inl val) (.stack A' B)
+  | stk0 : MCtx.push (.nostack A) (.inr val) (.stack A val)
+  | stk : MCtxS.push B val B' → MCtx.push (.stack A B) (.inr val) (.stack A B')
 
 structure TCtx where
   vctx : VCtx
@@ -231,9 +271,9 @@ structure TCtx where
   mctx : MCtx
 
 def TCtx.type (tctx : TCtx) : VProp :=
-  fun vs => tctx.vctx.eval vs ∗ tctx.mctx.lctx vs
+  fun vs => tctx.vctx.eval vs ∗ tctx.mctx.R.eval vs
 
-def TCtx.layout (tctx : TCtx) : StackLayout := tctx.mctx.mctx
+def TCtx.layout (tctx : TCtx) : StackLayout := tctx.mctx.layout
 
 inductive TCtx.pushVar : TCtx → Ty → TCtx → Prop where
   | mk {vctx mctx} : VCtx.push vctx (.var (some sz) ty) vctx' →
@@ -247,6 +287,11 @@ 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
 
+def TCtx.false : TCtx where
+  vctx := .hyp .false
+  vctxSz := 0
+  mctx := .nostack .false
+
 axiom Variant : Type
 axiom Variant.eval : Variant → Valuation → Nat → Prop
 
@@ -254,13 +299,16 @@ 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)
+def okCodeP (c : List UInt8) (epi : Epilogue) (tctx : TCtx)
+    (fr : Frame) (p : Nat) (ip : BlockLoc) (vs : Valuation) : SProp :=
+  SProp.heap fr.frame ∗ (
+    (match ip with
+    | some x => mainLayout c (textStart + p.toUInt64 + x.toUInt64)
     | none => ∃ₛ ip, mainLayout c ip) ∗
-    var.eval vs v ∗
     fr.stackLayout 8 epi.sp (tctx.layout.eval vs) ∗ tctx.type vs)
+
+def LabelGroup.eval : LabelGroup → Valuation → Nat → List UInt8 → Epilogue → Frame → Nat → SProp
+  | .one ip var tctx, vs, v, c, epi, fr, p => var.eval vs v ∗ okCodeP c epi tctx fr p ip 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
@@ -270,27 +318,49 @@ inductive findLabel : LabelGroup → BlockLoc → Variant → TCtx → Prop
 
 def LabelGroups := List (Expr × LabelGroup)
 
-def LabelGroups.eval : LabelGroups → List UInt8 → Epilogue' → Frame → Nat → SProp
+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
 
+inductive findLabels : LabelGroups → Expr → LabelGroup → Prop
+  | one : findLabels ((var, ls) :: labs) var ls
+  | cons : findLabels labs var ls → findLabels ((var', ls') :: labs) var ls
+
 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)
+def okCodeN (bctx : BCtx) (tctx : TCtx) (fr : Frame) (p : Nat) (ip : BlockLoc) : Prop :=
+  bctx.result.ok <| ∃ₛ vs, okCodeP bctx.content bctx.epi tctx fr p ip vs
+
+inductive IRM where
+  | reg : RegNum → IRM
+  | imm32 : UInt32 → IRM
+
+inductive Size where
+  | sz64
+instance : OfNat Size 64 := ⟨.sz64⟩
+
+axiom Inst : Type
+axiom Inst.push : IRM → Inst
+axiom Inst.pop : RegNum → Inst
+axiom Inst.ret : Inst
+axiom Inst.sub : Size → RegNum → IRM → Inst
+axiom Inst.add : Size → RegNum → IRM → Inst
+axiom Inst.jump : Nat → Inst
+
+axiom Inst.eval : Inst → Nat → List UInt8 → Nat → Prop
 
 inductive LAsm where
   | nil
+  | inst (_ : Inst)
   | 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
+  | inst : I.eval p s x → eval (.inst I) p s 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
@@ -313,6 +383,127 @@ 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 :=
+def okCode.sema (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)
+    okCodeN bctx tctx' fr p (some y) → okCodeN bctx tctx fr p (some x)
+
+inductive okPrologue :
+    (epi : EpilogueR) → (mctx : MCtxR) →
+    (code : LAsm) → (epi' : Epilogue) → (mctx' : MCtx) → Prop
+  | push :
+    MCtxR.push mctx₁ (.free r) mctx₂ →
+    okPrologue (.pop r epi) mctx₂ code epi' mctx₃ →
+    okPrologue epi mctx₁ (.seq (.inst (.push (.reg r))) code) epi' mctx₃
+  | alloc0 : MCtxR.OK mctx a b → okPrologue epi mctx .nil (.nostack epi) (.nostack mctx)
+  | alloc : MCtxR.OK mctx a b → n.toNat ≤ 2^12-8 →
+    okPrologue epi mctx (.inst (.sub 64 RSP (.imm32 n)))
+      (.free n.toNat epi) (.stack mctx (.free 0 n.toNat))
+
+axiom assembled : GCtx → GAsm → Prop
+
+inductive okAssembled : PCtx → LAsm → Prop
+  | I : assembled pctx.toGCtx (.proc start code) → okAssembled pctx code
+  | l : okAssembled pctx (.seq A B) → okAssembled pctx A
+  | r : okAssembled pctx (.seq A B) → okAssembled pctx B
+
+inductive Arg where
+  | var (ty : Ty)
+  | hyp (ty : Ty)
+
+inductive Args where
+  | nil
+  | snoc (a : Args) (b : Arg)
+
+inductive accumArgs : Args → VCtx → Nat → Prop
+  | nil : accumArgs .nil .emp 0
+  | var :
+    accumArgs args vtcx n →
+    VCtx.push vtcx (.var (some n) ty) vctx' →
+    accumArgs (.snoc args (.var ty)) vtcx' (n+1)
+  | hyp :
+    accumArgs args vtcx n →
+    VCtx.push vtcx (.hyp ty) vctx' →
+    accumArgs (.snoc args (.hyp ty)) vtcx' n
+
+structure ArgsM where
+  args : Args
+  mctx : MCtxR
+
+def Clobbers := List RegNum
+inductive accumClob : Clobbers → MCtxR → MCtxR → Prop
+  | nil : accumClob [] mctx mctx
+  | cons : MCtxR.push mctx₁ (.free r) mctx₁ →
+    accumClob clob mctx₂ mctx₃ → accumClob (r :: clob) mctx₁ mctx₃
+
+axiom checkRet : BCtx → TCtx → ReturnABI → Prop
+
+def EpilogueR.toCode : EpilogueR → LAsm
+  | .ret => .inst .ret
+  | .pop r epi => .seq (.inst (.pop r)) epi.toCode
+
+def Epilogue.toCode : Epilogue → LAsm
+  | .nostack epi => epi.toCode
+  | .free n epi => .seq (.inst (.add 64 RSP (.imm32 n.toUInt32))) epi.toCode
+
+inductive getEpi : BCtx → ReturnABI → LAsm → Prop
+  | mk : getEpi ⟨⟨gctx, ret, epi, se⟩, labs⟩ ret epi.toCode
+
+inductive okPushVariant : Expr → Variant → TCtx → TCtx → Prop
+
+inductive variantValue : Variant → Expr → Prop
+
+mutual
+
+inductive addLabels : BCtx → LabelGroup → LabelGroup → Prop
+  | and : addLabels bctx ls A → addLabels bctx ls B → addLabels bctx ls (.and A B)
+  | none :
+    variantValue var val →
+    okCode ⟨bctx, (val, ls) :: L⟩ tctx .nil .false →
+    addLabels ⟨bctx, L⟩ ls (.one none var tctx)
+  | some :
+    okAssembled pctx (.at ip code) →
+    variantValue var val →
+    okCode ⟨bctx, (val, ls) :: L⟩ tctx code .false →
+    addLabels ⟨bctx, L⟩ ls (.one (some ip) var tctx)
+
+inductive okLabels : BCtx → LabelGroup → Prop
+  | l : okLabels bctx (.and A B) → okLabels bctx A
+  | r : okLabels bctx (.and A B) → okLabels bctx B
+  | mk : addLabels bctx ls ls → okLabels bctx ls
+
+inductive okBlock : BCtx → BlockLoc → TCtx → Prop
+  | weak : okCode bctx tctx .nil tctx' → okBlock bctx ip tctx' → okBlock bctx ip tctx
+  | mk : okAssembled bctx.toPCtx (.at ip code) →
+    okCode bctx tctx code .false → okBlock bctx (some ip) tctx
+  | unreachable : okCode bctx tctx .nil .false → okBlock bctx none tctx
+  | label :
+    findLabels L var1 ls →
+    findLabel ls ip var2 tctx →
+    okPushVariant var1 var2 tctx tctx' →
+    okBlock ⟨pctx, L⟩ ip tctx'
+  | ofLabel : okLabels bctx (.one ip var tctx) → okBlock bctx ip tctx
+
+inductive okCode : BCtx → TCtx → LAsm → TCtx → Prop
+  | epilogue : getEpi bctx ret code → checkRet bctx tctx ret → okCode bctx tctx code .false
+  | jump : okBlock bctx (some tgt) tctx → okCode bctx tctx (.inst (.jump tgt)) .false
+
+end
+
+inductive okProc : GCtx → Nat → ArgsM → ReturnABI → List RegNum → Bool → Prop
+  | mk :
+    okAssembled pctx (.entry start (.seq prol code)) →
+    accumArgs args vctx₁ sz₁ →
+    accumClob clob mctx₁ mctx₂ →
+    okPrologue .ret mctx₂ prol pctx.epi mctx₃ →
+    okCode ⟨pctx, []⟩ ⟨vctx₁, sz₁, mctx₃⟩ code .false →
+    okProc pctx.toGCtx start ⟨args, mctx₁⟩ pctx.ret clob pctx.se
+
+inductive buildStart : GCtx → PCtx → TCtx → Prop
+  | mk : buildStart gctx ⟨gctx, .noRet, .nostack .ret, true⟩ ⟨.emp, 0, .nostack .emp⟩
+
+inductive okStart : GCtx → Prop
+  | mk :
+    okAssembled pctx (.entry start (.seq .nil code)) →
+    buildStart gctx pctx tctx →
+    okCode ⟨pctx, []⟩ tctx code .false →
+    okStart gctx
diff --git a/mm0-rs/src/mmc/proof/compiler.rs b/mm0-rs/src/mmc/proof/compiler.rs
index da34b3be..a8ce865b 100644
--- a/mm0-rs/src/mmc/proof/compiler.rs
+++ b/mm0-rs/src/mmc/proof/compiler.rs
@@ -54,7 +54,7 @@ impl Ctx {
     let ok0 = app!(de, (ok0));
     let asm0 = app!(de, (ASM0));
     let gctx = app!(de, ({t_gctx}));
-    let ret = app!(de, (ok0)); // TODO
+    let ret = app!(de, (noRet)); // TODO
     let se = app!(de, (tru)); // TODO
     let mut epi = app!(de, (epiRet));
     for &reg in proc.saved_regs() {
@@ -1029,40 +1029,35 @@ impl ProcProver<'_> {
     }
   }
 
-  /// Returns `|- okPrologue epiRet x0 mctx1 code epi mctx2`
+  /// Returns `|- okPrologue epiRet mctx1 code epi mctx2`
   fn ok_prologue(&mut self, mctx: &mut P<MCtx>, mut code: ProofId) -> ProofId {
     let mut epi = app!(self.thm, (epiRet));
-    let mut sp = self.hex.h2n(&mut self.thm, 0);
     let mut stack = vec![];
     for &reg in self.proc.saved_regs() {
       let r = reg.index(); let er = self.hex[r];
       app_match!(self.thm, let (ASM_A _ code2) = code);
-      let n = self.hex.h2n(&mut self.thm, 8);
-      let (sp2, h1) = self.hex.add(&mut self.thm, sp, n);
       let mctx1 = mctx.1;
       let t = ((r, MCtxRegValue::Free), app!(self.thm, (FREE er)));
-      let h2 = MCtx::push_reg::<PushMCtx>(mctx, &mut self.thm, t);
-      stack.push([code, code2, epi, mctx1, mctx.1, er, *sp, *sp2, h1, h2]);
+      let h1 = MCtx::push_reg::<PushMCtx>(mctx, &mut self.thm, t);
+      stack.push([code, code2, epi, mctx1, mctx.1, er, h1]);
       epi = app!(self.thm, epiPop[er, epi]);
-      sp = sp2;
       code = code2;
     }
     let h1 = mctx.0.ok(&mut self.thm);
     let mctx1 = mctx.1;
     let mut th = if self.sp_max.val == 0 {
-      thm!(self.thm, (okPrologue[epi, *sp, mctx1, code, epi, mctx1]) =>
-        okPrologue_alloc0(epi, mctx1, *sp, h1))
+      thm!(self.thm, (okPrologue[epi, mctx1, code, epi, mctx1]) =>
+        okPrologue_alloc0(epi, mctx1, h1))
     } else {
       MCtx::add_stack(mctx, &mut self.thm, self.ctx.sp_max);
-      let (m, h2) = self.hex.add(&mut self.thm, sp, self.ctx.sp_max);
-      let max = self.hex.from_u32(&mut self.thm, 1 << 12);
-      let h3 = self.hex.lt(&mut self.thm, m, max);
-      thm!(self.thm, (okPrologue[epi, *sp, mctx1, code, self.epi, mctx.1]) =>
-        okPrologue_alloc(epi, *m, mctx1, *self.sp_max, *sp, h1, h2, h3))
+      let max = self.hex.from_u32(&mut self.thm, (1 << 12) - 8);
+      let h2 = self.hex.le(&mut self.thm, self.ctx.sp_max, max);
+      thm!(self.thm, (okPrologue[epi, mctx1, code, self.epi, mctx.1]) =>
+        okPrologue_alloc(epi, mctx1, *self.sp_max, h1, h2))
     };
-    for [code, code2, epi1, mctx1, mctx2, er, sp, sp2, h1, h2] in stack.into_iter().rev() {
-      th = thm!(self.thm, (okPrologue[epi1, sp, mctx1, code, epi, mctx.1]) =>
-        okPrologue_push(code2, epi1, epi, mctx1, mctx2, mctx.1, er, sp, sp2, h1, h2, th))
+    for [code, code2, epi1, mctx1, mctx2, er, h1] in stack.into_iter().rev() {
+      th = thm!(self.thm, (okPrologue[epi1, mctx1, code, epi, mctx.1]) =>
+        okPrologue_push(code2, epi1, epi, mctx1, mctx2, mctx.1, er, h1, th))
     }
     th
   }
@@ -1084,13 +1079,17 @@ impl ProcProver<'_> {
     })
   }
 
-  /// Returns `(fs, ms, tctx, |- buildStart gctx pctx fs ms tctx)`
-  fn build_start(&mut self, bl: BlockProof<'_>, root: VCtx) -> (Num, Num, PTCtx, ProofId) {
-    let fs = self.hex.from_u64(&mut self.thm, self.elf_proof.p_filesz());
-    let ms = self.hex.from_u64(&mut self.thm, self.elf_proof.p_memsz());
-    let tctx = self.block_tctx(bl, root, CtxId::ROOT);
-    let bproc = app!(self.thm, buildStart[self.gctx, self.pctx, *fs, *ms, tctx.1]);
-    (fs, ms, tctx, thm!(self.thm, sorry(bproc): bproc)) // TODO
+  /// Returns `|- getEpi bctx ret code`
+  fn get_epi(&mut self, code: ProofId) -> ProofId {
+    let h = self.ok_epilogue(self.epi, code);
+    thm!(self.thm, (getEpi[self.bctx, self.ret, code]) =>
+      getEpiI(code, self.epi, self.gctx, self.labs, self.ret, self.se, h))
+  }
+
+  /// Returns `(tctx, |- buildStart gctx pctx tctx)`
+  fn build_start(&mut self, bl: BlockProof<'_>, root: VCtx) -> (PTCtx, ProofId) {
+    let (tctx, l1) = self.block_tctx(bl, root, CtxId::ROOT);
+    ((tctx, l1), thm!(self.thm, buildStartI(self.gctx): buildStart[self.gctx, self.pctx, l1]))
   }
 
   /// Returns `(v, |- okRead tctx loc v)`
@@ -1155,18 +1154,14 @@ impl ProcProver<'_> {
       CONV({th} => (getResult (UNFOLD({self.t_gctx}); u_gctx) ty))))
   }
 
-  /// Returns `|- getEpi bctx ret epi`
-  fn get_epi(&mut self) -> ProofId {
-    thm!(self.thm, (getEpi[self.bctx, self.ret, self.epi]) =>
-      getEpiI(self.epi, self.gctx, self.labs, self.ret, self.se))
-  }
-
   /// Returns `|- checkRet bctx tctx ret`
   fn check_ret(&mut self,
     tctx: &mut P<&mut TCtx>, outs: &[VarId], args: &[(VarId, bool, Operand)]
   ) -> ProofId {
-    let th = thm!(self.thm, (checkRet[self.bctx, tctx.1, self.ret]) =>
-      checkRetI(self.bctx, self.ret, tctx.1));
+    // let th = thm!(self.thm, (checkRet[self.bctx, tctx.1, self.ret]) =>
+    //   checkRetI(self.bctx, self.ret, tctx.1));
+    let ret = app!(self.thm, checkRet[self.bctx, tctx.1, self.ret]);
+    let th = thm!(self.thm, sorry(ret): ret); // TODO
     tctx.1 = self.ok0;
     th
   }
@@ -1226,10 +1221,9 @@ impl ProcProver<'_> {
         okProcI(args, clob, code, self.epi, self.gctx, mctx1, mctx2, mctx3,
           prol, self.ret, self.se, start, sz1, vctx1, h1, h2, h3, h4, h5))
     } else {
-      let (fs, ms, (mut tctx, l1), h2) = self.build_start(bl, root);
+      let ((mut tctx, l1), h2) = self.build_start(bl, root);
       let h3 = self.ok_stmts(bl, code, (&mut *tctx, l1));
-      thm!(self.thm, (okStart[self.gctx, *fs, *ms]) =>
-        okStartI(code, *fs, self.gctx, *ms, self.pctx, l1, h1, h2, h3))
+      thm!(self.thm, okStartI(code, self.gctx, self.pctx, l1, h1, h2, h3): okStart[self.gctx])
     }
   }
 }
@@ -1597,12 +1591,11 @@ impl<'a> cl::Visitor<'a> for BlockProofVisitor<'a, '_> {
       Terminator::Return(outs, args) => {
         assert!(!matches!(cl, cl::Terminator::Ghost), "ghost return not allowed, I think");
         self.inst_state = InstState::None;
-        let h1 = self.get_epi();
         let proc = &mut *self.proc;
+        let h1 = proc.get_epi(self.code);
         let h2 = proc.check_ret(&mut self.tctx, outs, args);
-        let h3 = proc.ok_epilogue(proc.epi, self.code);
         let th = thm!(proc.thm, (okCode[proc.bctx, self.lhs_tctx, self.code, proc.ok0]) =>
-          okEpilogue_E(proc.bctx, self.code, proc.epi, proc.ret, self.lhs_tctx, h1, h2, h3));
+          okEpilogue_E(proc.bctx, self.code, proc.ret, self.lhs_tctx, h1, h2));
         self.finish(th)
       }
       Terminator::Unreachable(_) => todo!(),
diff --git a/mm0-rs/src/mmc/proof/predefs.rs b/mm0-rs/src/mmc/proof/predefs.rs
index bd40a545..bca8619d 100644
--- a/mm0-rs/src/mmc/proof/predefs.rs
+++ b/mm0-rs/src/mmc/proof/predefs.rs
@@ -525,6 +525,8 @@ make_predefs! {
 
   ok0: TermId => "ok0";
 
+  noRet: TermId => "noRet";
+
   labelGroup0: TermId => "labelGroup0";
   labelGroup: TermId => "labelGroup";