Merge pull request #716 from CakeML/stack-opt-2

Stack optimisation that improves tail calls

compiler/backend/README.md

@@ -278,6 +278,13 @@ implementation of the garbage collector.
 This compiler phase renames the registers to fit with the target
 architecture.
 
+[stack_rawcallScript.sml](stack_rawcallScript.sml):
+This compiler phase introduces calls past the stack allocation code
+that is present at almost every start of function. A call past stack
+allocation is called a RawCall. RawCalls are introduced to shortcut
+some bookkeeping during tail-calls to known locations, i.e
+`Call NONE (INL dest) ..`.
+
 [stack_removeScript.sml](stack_removeScript.sml):
 This compiler phase implements all stack operations as normal memory
 load/store operations.

compiler/backend/backendComputeLib.sml

@@ -703,6 +703,7 @@ val add_backend_compset = computeLib.extend_compset
      ``:'a stackLang$prog``
     ,``:stackLang$store_name``
     ]
+  ,computeLib.Defs (theory_computes "stack_rawcall")
   ,computeLib.Defs
     [stackLangTheory.list_Seq_def
     ,backend_commonTheory.word_shift_def
@@ -821,6 +822,7 @@ val add_backend_compset = computeLib.extend_compset
     ,stack_to_labTheory.is_gen_gc_def
     ,stack_to_labTheory.compile_jump_def
     ,stack_to_labTheory.negate_def
+    ,stack_to_labTheory.is_Seq_def
     ,stack_to_labTheory.flatten_def
     ,stack_to_labTheory.prog_to_section_def
     ,stack_to_labTheory.compile_def

compiler/backend/data_to_wordScript.sml

@@ -510,11 +510,11 @@ val AnyArith_code_def = Define `
       Set (Temp 3w) (Shift Lsr (Var 6) 2);
       Assign 3 (Const 0w);
       (* zero out result array *)
-      Call (SOME (0,fromList [()],Skip,AnyArith_location,1))
+      Call (SOME (0,fromList [()],Skip,AnyArith_location,2))
         (SOME Replicate_location) [2;3;1;0] NONE;
       (* perform bignum calculation *)
       Set (Temp 29w) (Op Add [Lookup (Temp 29w); Const bytes_in_word]);
-      Call (SOME (1,fromList [()],Skip,AnyArith_location,2))
+      Call (SOME (1,fromList [()],Skip,AnyArith_location,3))
         (SOME Bignum_location) [] NONE;
       (* convert bignum to smallnum if possible without loss of info *)
       Get 1 (Temp 10w);
@@ -676,7 +676,7 @@ val Equal1_code_def = Define `
         (Seq (Assign 2 (Const 1w)) (Return 0 2)) Skip;
       Assign 1 (Load (Var 4));
       Assign 3 (Load (Var 6));
-      Call (SOME (5,list_insert [0;2;4;6] LN,Skip,Equal1_location,1))
+      Call (SOME (5,list_insert [0;2;4;6] LN,Skip,Equal1_location,2))
         (SOME Equal_location) [1;3] NONE;
       If Equal 5 (Imm 1w) Skip (Return 0 5);
       Assign 2 (Op Sub [Var 2; Const 1w]);
@@ -2029,7 +2029,7 @@ val comp_def = Define `
                     (Call ret target (MAP adjust_var args) handler, l1)`
 
 val compile_part_def = Define `
-  compile_part c (n,arg_count,p) = (n,arg_count+1n,FST (comp c n 1 p))`
+  compile_part c (n,arg_count,p) = (n,arg_count+1n,FST (comp c n 2 p))`
 
 val MemCopy_code_def = Define `
   MemCopy_code =

compiler/backend/proofs/README.md

@@ -117,6 +117,9 @@ Correctness proof for stack_alloc
 [stack_namesProofScript.sml](stack_namesProofScript.sml):
 Correctness proof for stack_names
 
+[stack_rawcallProofScript.sml](stack_rawcallProofScript.sml):
+Correctness proof for stack_rawcall
+
 [stack_removeProofScript.sml](stack_removeProofScript.sml):
 Correctness proof for stack_remove
 

compiler/backend/proofs/backendProofScript.sml

@@ -1389,7 +1389,7 @@ Proof
   \\ qx_genl_tac[`l1`,`l2`] \\ strip_tac
   \\ simp[GSYM stack_namesProofTheory.stack_names_lab_pres]
   \\ simp[GSYM stack_removeProofTheory.stack_remove_lab_pres]
-  \\ qspecl_then[`l1`,`next_lab l2 1`,`l2`]mp_tac stack_allocProofTheory.stack_alloc_lab_pres
+  \\ qspecl_then[`l1`,`next_lab l2 2`,`l2`]mp_tac stack_allocProofTheory.stack_alloc_lab_pres
   \\ simp[UNCURRY]
   \\ reverse impl_tac >- rw []
   \\ drule compile_word_to_stack_lab_pres
@@ -1425,7 +1425,7 @@ Proof
   \\ PairCases_on`pp4`
   \\ pop_assum(assume_tac o SYM o SIMP_RULE std_ss [markerTheory.Abbrev_def])
   \\ fs[data_to_wordTheory.compile_part_def]
-  \\ qspecl_then[`c4_data_conf`,`pp40`,`1`,`pp42`]mp_tac data_to_wordProofTheory.data_to_word_lab_pres_lem
+  \\ qspecl_then[`c4_data_conf`,`pp40`,`2`,`pp42`]mp_tac data_to_wordProofTheory.data_to_word_lab_pres_lem
   \\ simp[]
   \\ pairarg_tac \\ fs[]
   \\ simp[EVERY_MEM]
@@ -1489,10 +1489,11 @@ Theorem MAP_Section_num_stack_to_lab_SUBSET:
   set (MAP Section_num (compile sc dc max_heap sp offset prog)) ⊆ labs
 Proof
   simp [stack_to_labTheory.compile_def, MAP_prog_to_section_Section_num]
-  \\ simp [stack_removeTheory.compile_def, MAP_MAP_o, o_DEF,
-       stack_allocTheory.compile_def, Q.ISPEC `FST` ETA_THM]
-  \\ EVAL_TAC
-  \\ simp []
+  \\ simp [stack_removeTheory.compile_def,
+       stack_rawcallTheory.compile_def,
+       stack_allocTheory.compile_def, MAP_MAP_o, o_DEF, Q.ISPEC `FST` ETA_THM]
+  \\ fs [UNCURRY,Q.ISPEC `FST` ETA_THM]
+  \\ EVAL_TAC \\ simp []
 QED
 
 Theorem to_data_labels_ok:
@@ -1527,7 +1528,7 @@ Theorem to_word_labels_ok:
   EVERY (λn. n > raise_stub_location) (MAP FST p) /\
   EVERY (λ(n,m,p).
     let labs = wordProps$extract_labels p in
-    EVERY (λ(l1,l2). l1 = n ∧ l2 ≠ 0) labs ∧ ALL_DISTINCT labs) p
+    EVERY (λ(l1,l2). l1 = n ∧ l2 ≠ 0 ∧ l2 ≠ 1) labs ∧ ALL_DISTINCT labs) p
 Proof
   rw [to_word_def]
   \\ rpt (pairarg_tac \\ fs [])
@@ -2333,7 +2334,7 @@ Proof
   \\ PairCases_on`pp4`
   \\ pop_assum(assume_tac o SYM o SIMP_RULE std_ss [markerTheory.Abbrev_def])
   \\ fs[data_to_wordTheory.compile_part_def]
-  \\ qspecl_then[`c4_data_conf`,`pp40`,`1`,`pp42`]mp_tac data_to_wordProofTheory.data_to_word_lab_pres_lem
+  \\ qspecl_then[`c4_data_conf`,`pp40`,`2`,`pp42`]mp_tac data_to_wordProofTheory.data_to_word_lab_pres_lem
   \\ simp[]
   \\ pairarg_tac \\ fs[]
   \\ simp[EVERY_MEM]

compiler/backend/proofs/data_to_wordProofScript.sml

@@ -1353,12 +1353,15 @@ val labels_rel_emp = Q.prove(`
 
 Theorem stub_labels:
     EVERY (λ(n,m,p).
-    EVERY (λ(l1,l2). l1 = n ∧ l2 ≠ 0) (extract_labels p)  ∧ ALL_DISTINCT (extract_labels p))
+    EVERY (λ(l1,l2). l1 = n ∧ l2 ≠ 0 ∧ l2 ≠ 1) (extract_labels p)  ∧
+                     ALL_DISTINCT (extract_labels p))
     (stubs (:'a) data_conf)
 Proof
   simp[data_to_wordTheory.stubs_def,generated_bignum_stubs_eq]>>
-  EVAL_TAC>>
-  rw[]>>EVAL_TAC
+  rpt conj_tac >>
+  rpt (EVAL_TAC \\ rw [] \\ EVAL_TAC \\ NO_TAC) >>
+  CONV_TAC (RAND_CONV EVAL) >>
+  CONV_TAC ((RATOR_CONV o RAND_CONV) EVAL)
 QED
 
 Theorem stubs_with_has_fp_ops[simp]:
@@ -1378,7 +1381,7 @@ Theorem data_to_word_compile_lab_pres:
     MAP FST p = MAP FST (stubs(:α) data_conf) ++ MAP FST prog ∧
     EVERY (λn,m,(p:α wordLang$prog).
       let labs = extract_labels p in
-      EVERY (λ(l1,l2).l1 = n ∧ l2 ≠ 0) labs ∧
+      EVERY (λ(l1,l2).l1 = n ∧ l2 ≠ 0 ∧ l2 ≠ 1) labs ∧
       ALL_DISTINCT labs) p
 Proof
   fs[data_to_wordTheory.compile_def]>>
@@ -1395,15 +1398,15 @@ Proof
   qabbrev_tac`pp = p1 ++ p2` >>
   fs[EL_MAP,MEM_EL,FORALL_PROD]>>
   `EVERY (λ(n,m,p).
-    EVERY (λ(l1,l2). l1 = n ∧ l2 ≠ 0) (extract_labels p)  ∧ ALL_DISTINCT (extract_labels p)) pp` by
+    EVERY (λ(l1,l2). l1 = n ∧ l2 ≠ 0 ∧ l2 ≠ 1) (extract_labels p)  ∧ ALL_DISTINCT (extract_labels p)) pp` by
     (unabbrev_all_tac>>fs[EVERY_MEM]>>CONJ_TAC
     >-
       (assume_tac stub_labels>>
       fs[EVERY_MEM])
     >>
       fs[MEM_MAP,MEM_EL,EXISTS_PROD]>>rw[]>>fs[compile_part_def]>>
       qmatch_goalsub_abbrev_tac `comp data_conf2` >>
-      Q.SPECL_THEN [`data_conf2`,`p_1`,`1n`,`p_2`]assume_tac
+      Q.SPECL_THEN [`data_conf2`,`p_1`,`2n`,`p_2`]assume_tac
         data_to_word_lab_pres_lem>>
       fs[]>>pairarg_tac>>fs[EVERY_EL,PULL_EXISTS]>>
       rw[]>>res_tac>>

compiler/backend/proofs/data_to_word_assignProofScript.sml

@@ -8918,7 +8918,7 @@ Proof
     \\ TOP_CASE_TAC
     THEN1 (fs [wordSemTheory.cut_env_def,domain_lookup] \\ fs [])
     \\ qmatch_goalsub_abbrev_tac `(Equal_code c, t1)`
-    \\ first_x_assum (qspecl_then [`t1`,`Equal1_location`,`1`] mp_tac)
+    \\ first_x_assum (qspecl_then [`t1`,`Equal1_location`,`2`] mp_tac)
     \\ impl_tac THEN1
      (unabbrev_all_tac \\ fs [lookup_insert,wordSemTheory.push_env_def,wordSemTheory.flush_state_def]
       \\ pairarg_tac \\ fs [] \\ fs [eq_eval,sane_locals_size_def]

compiler/backend/proofs/data_to_word_bignumProofScript.sml

@@ -938,7 +938,7 @@ Proof
 QED
 
 Theorem IMP_bignum_code_rel:
-   compile Bignum_location 1 1 (Bignum_location + 1,[])
+   compile Bignum_location 2 1 (Bignum_location + 1,[])
              mc_iop_code = (xx1,xx2,xx3,xx4,xx5) /\
     state_rel c l1 l2 s t [] locs ==>
     code_rel (xx4,xx5) t.code
@@ -1115,7 +1115,7 @@ Proof
   \\ rfs [labPropsTheory.good_dimindex_def,dimword_def,ADD1]
 QED
 
-val s = ``s:('c,'ffi)dataSem$state``
+val s = ``s:('c,'ffi)dataSem$state``;
 
 Theorem AnyArith_thm:
    ∀op_index i j v t s r2 r1 locs l2 l1 c.
@@ -1342,7 +1342,7 @@ Proof
     (fs [Abbr`m5`] \\ SEP_W_TAC \\ fs [AC STAR_COMM STAR_ASSOC] \\ NO_TAC)
   \\ drule word_list_store_list
   \\ strip_tac \\ fs []
-  \\ qspecl_then [`Word 0w`,`Loc l1 l2`,`1`,`AnyArith_location`,`LENGTH xs`,
+  \\ qspecl_then [`Word 0w`,`Loc l1 l2`,`2`,`AnyArith_location`,`LENGTH xs`,
        `curr + bytes_in_word * n2w (heap_length ha)`,`t9`,`m2`,
        `2`,`3`,`1`] mp_tac
          (GEN_ALL Replicate_code_alt_thm |> SIMP_RULE std_ss [])
@@ -1383,7 +1383,7 @@ Proof
   \\ `code_rel c s.code t.code` by (fs [state_rel_def] \\ NO_TAC)
   \\ pop_assum mp_tac
   \\ rewrite_tac [code_rel_def,stubs_def,generated_bignum_stubs_def,LET_THM]
-  \\ Cases_on `compile Bignum_location 1 1 (Bignum_location + 1,[]) mc_iop_code`
+  \\ Cases_on `compile Bignum_location 2 1 (Bignum_location + 1,[]) mc_iop_code`
   \\ PairCases_on `r`
   \\ simp_tac (srw_ss())[APPEND,EVERY_DEF,EVAL ``domain (fromList [()]) = ∅``]
   \\ strip_tac
@@ -1413,8 +1413,8 @@ Proof
   \\ qabbrev_tac `my_frame = word_heap curr ha c *
          one (curr + bytes_in_word * n2w (heap_length ha),Word a3) *
          hb_heap * hb_heap1 * one (other,Word a3') * other_heap`
-  \\ qspecl_then [`i`,`j`,`1`,`my_frame`,`REPLICATE (LENGTH xs) 0w`,`t3`,
-          `Loc AnyArith_location 2`,`Bignum_location`,`t3.clock`,
+  \\ qspecl_then [`i`,`j`,`2`,`my_frame`,`REPLICATE (LENGTH xs) 0w`,`t3`,
+          `Loc AnyArith_location 3`,`Bignum_location`,`t3.clock`,
           `get_iop op_index`] mp_tac
        (evaluate_mc_iop |> INST_TYPE [``:'d``|->``:'ffi``])
   \\ asm_rewrite_tac [] \\ simp_tac std_ss [AND_IMP_INTRO]
@@ -1435,7 +1435,7 @@ Proof
      (qunabbrev_tac `t3` \\ fs [wordSemTheory.push_env_def]
       \\ pairarg_tac \\ fs [] \\ NO_TAC) \\ fs []
     \\ `div_code_assum (:'ffi) (:'c) t.code` by metis_tac [div_code_assum_thm]
-    \\ `get_var 0 t3 = SOME (Loc AnyArith_location 2)` by
+    \\ `get_var 0 t3 = SOME (Loc AnyArith_location 3)` by
           (qunabbrev_tac `t3` \\ fs [wordSemTheory.get_var_def] \\ NO_TAC)
     \\ simp []
     \\ imp_res_tac state_rel_imp_clock

compiler/backend/proofs/data_to_word_gcProofScript.sml

@@ -4340,7 +4340,7 @@ val code_rel_def = Define `
     EVERY (\(n,x). lookup n t_code = SOME x) (stubs (:'a) c) /\
     !n arg_count prog.
       (lookup n s_code = SOME (arg_count:num,prog)) ==>
-      (lookup n t_code = SOME (arg_count+1,FST (comp c n 1 prog)))`
+      (lookup n t_code = SOME (arg_count+1,FST (comp c n 2 prog)))`
 
 val stack_rel_def = Define `
   (stack_rel (Env s1 env) (StackFrame s2 vs NONE) <=>
@@ -5047,7 +5047,8 @@ Theorem find_code_thm = Q.prove(`
           \\ qpat_x_assum `ws <> []` (assume_tac)
           \\ imp_res_tac NOT_NIL_IMP_LAST \\ full_simp_tac(srw_ss())[])
   \\ imp_res_tac get_vars_IMP_LENGTH \\ full_simp_tac(srw_ss())[]
-  THENL [Q.LIST_EXISTS_TAC [`n`,`1`],Q.LIST_EXISTS_TAC [`x'`,`1`]] \\ full_simp_tac(srw_ss())[]
+  \\ rename [`comp c n 2 r`]
+  \\ Q.LIST_EXISTS_TAC [`n`,`2`] \\ full_simp_tac(srw_ss())[]
   \\ imp_res_tac state_rel_call_env \\ full_simp_tac(srw_ss())[]
   \\ `args <> []` by (Cases_on `args` \\ full_simp_tac(srw_ss())[] \\ Cases_on `x` \\ full_simp_tac(srw_ss())[])
   \\ `?x1 x2. args = SNOC x1 x2` by metis_tac [SNOC_CASES] \\ srw_tac[][]
@@ -5224,11 +5225,11 @@ Theorem find_code_thm_ret = Q.prove(`
           \\ qpat_x_assum `ws <> []` (assume_tac)
           \\ imp_res_tac NOT_NIL_IMP_LAST \\ full_simp_tac(srw_ss())[])
   \\ imp_res_tac get_vars_IMP_LENGTH \\ full_simp_tac(srw_ss())[]
-  THEN1 (Q.LIST_EXISTS_TAC [`x'`,`1`] \\ full_simp_tac(srw_ss())[]
+  THEN1 (Q.LIST_EXISTS_TAC [`x'`,`2`] \\ full_simp_tac(srw_ss())[]
          \\ qspecl_then [`lookup x' fs`,`NONE`] mp_tac
                (Q.GEN `ss` state_rel_call_env_push_env)
          \\ full_simp_tac(srw_ss())[])
-  \\ Q.LIST_EXISTS_TAC [`n`,`1`] \\ full_simp_tac(srw_ss())[]
+  \\ Q.LIST_EXISTS_TAC [`n`,`2`] \\ full_simp_tac(srw_ss())[]
   \\ `args <> []` by (Cases_on `args` \\ full_simp_tac(srw_ss())[] \\ Cases_on `xs` \\ full_simp_tac(srw_ss())[])
   \\ `?x1 x2. args = SNOC x1 x2` by metis_tac [SNOC_CASES] \\ srw_tac[][]
   \\ full_simp_tac(srw_ss())[MAP_SNOC]
@@ -5264,10 +5265,10 @@ Theorem find_code_thm_handler = Q.prove(`
           \\ qpat_x_assum `ws <> []` (assume_tac)
           \\ imp_res_tac NOT_NIL_IMP_LAST \\ full_simp_tac(srw_ss())[])
   \\ imp_res_tac get_vars_IMP_LENGTH \\ full_simp_tac(srw_ss())[]
-  THEN1 (Q.LIST_EXISTS_TAC [`x'`,`1`] \\ full_simp_tac(srw_ss())[]
+  THEN1 (Q.LIST_EXISTS_TAC [`x'`,`2`] \\ full_simp_tac(srw_ss())[]
          \\ match_mp_tac (state_rel_call_env_push_env |> Q.SPEC `SOME xx`
                    |> SIMP_RULE std_ss [] |> GEN_ALL) \\ full_simp_tac(srw_ss())[] \\ metis_tac [])
-  \\ Q.LIST_EXISTS_TAC [`n`,`1`] \\ full_simp_tac(srw_ss())[]
+  \\ Q.LIST_EXISTS_TAC [`n`,`2`] \\ full_simp_tac(srw_ss())[]
   \\ `args <> []` by (Cases_on `args` \\ full_simp_tac(srw_ss())[] \\ Cases_on `xs` \\ full_simp_tac(srw_ss())[])
   \\ `?x1 x2. args = SNOC x1 x2` by metis_tac [SNOC_CASES] \\ srw_tac[][]
   \\ full_simp_tac(srw_ss())[MAP_SNOC]

compiler/backend/proofs/stack_allocProofScript.sml

@@ -70,7 +70,7 @@ val get_var_imm_case = Q.prove(
   Cases_on `ri` \\ full_simp_tac(srw_ss())[get_var_imm_def]);
 
 val prog_comp_lemma = Q.prove(
-  `prog_comp = \(n,p). (n,FST (comp n (next_lab p 1) p))`,
+  `prog_comp = \(n,p). (n,FST (comp n (next_lab p 2) p))`,
   full_simp_tac(srw_ss())[FUN_EQ_THM,FORALL_PROD,prog_comp_def]);
 
 Theorem FST_prog_comp[simp]:
@@ -5404,6 +5404,29 @@ Proof
     \\ `ck + s.clock - 1 = ck + (s.clock - 1)` by decide_tac
     \\ qexists_tac `ck` \\ full_simp_tac(srw_ss())[AC ADD_COMM ADD_ASSOC]
     \\ simp[state_component_equality])
+  \\ conj_tac (* RawCall *) >- (
+     rpt strip_tac
+     \\ full_simp_tac(srw_ss())[evaluate_def]
+     \\ simp [comp_def] \\ fs [evaluate_def]
+     \\ fs [CaseEq"option"]
+     \\ drule lookup_IMP_lookup_compile
+     \\ impl_tac THEN1 (res_tac \\ fs [])
+     \\ strip_tac \\ fs []
+     \\ Cases_on `prog` \\ fs [dest_Seq_def]
+     \\ rveq \\ fs []
+     \\ once_rewrite_tac [comp_def] \\ fs []
+     \\ ntac 2 (pairarg_tac \\ simp [])
+     \\ fs [dest_Seq_def]
+     \\ fs [CaseEq"bool"]
+     THEN1
+      (qexists_tac `0` \\ fs [] \\ fs [empty_env_def,state_component_equality]
+       \\ rfs [] \\ fs [] \\ qpat_x_assum `[] = _` (assume_tac o GSYM) \\ fs [])
+     \\ fs [CaseEq"option",pair_case_eq] \\ rveq \\ fs [dec_clock_def]
+     \\ rename [`comp m4 m5 p0 = (q2,m6)`]
+     \\ last_x_assum (qspecl_then [`m5`,`m4`,`c`,`regs`] mp_tac) \\ fs []
+     \\ impl_tac THEN1 (res_tac \\ fs [alloc_arg_def] \\ rw [] \\ res_tac)
+     \\ strip_tac \\ fs [] \\ qexists_tac `ck` \\ fs []
+     \\ fs [state_component_equality])
   \\ conj_tac (* Call *) >- (
      rpt strip_tac
      \\ full_simp_tac(srw_ss())[evaluate_def]
@@ -5874,17 +5897,17 @@ val MAX_SIMP = prove(
 
 Theorem next_lab_thm:
    !p.
-      next_lab (p:'a stackLang$prog) 1 =
+      next_lab (p:'a stackLang$prog) 2 =
       case p of
-      | Seq p1 p2 => MAX (next_lab p1 1) (next_lab p2 1)
-      | If _ _ _ p1 p2 => MAX (next_lab p1 1) (next_lab p2 1)
-      | While _ _ _ p => next_lab p 1
-      | Call NONE _ NONE => 1
-      | Call NONE _ (SOME (_,_,l2)) => l2 + 1
-      | Call (SOME (p,_,_,l2)) _ NONE => MAX (next_lab p 1) (l2 + 1)
+      | Seq p1 p2 => MAX (next_lab p1 2) (next_lab p2 2)
+      | If _ _ _ p1 p2 => MAX (next_lab p1 2) (next_lab p2 2)
+      | While _ _ _ p => next_lab p 2
+      | Call NONE _ NONE => 2
+      | Call NONE _ (SOME (_,_,l2)) => MAX (l2 + 2) 2
+      | Call (SOME (p,_,_,l2)) _ NONE => MAX (next_lab p 2) (l2 + 2)
       | Call (SOME (p,_,_,l2)) _ (SOME (p',_,l3)) =>
-           MAX (MAX (next_lab p 1) (next_lab p' 1)) (MAX l2 l3 + 1)
-      | _ => 1
+           MAX (MAX (next_lab p 2) (next_lab p' 2)) (MAX l2 l3 + 2)
+      | _ => 2
 Proof
   Induct \\ simp [Once next_lab_def] \\ fs []
   \\ once_rewrite_tac [next_lab_EQ_MAX]
@@ -5902,7 +5925,7 @@ QED
 Theorem extract_labels_next_lab:
     ∀p (aux:num) e.
     MEM e (extract_labels p) ⇒
-    SND e < next_lab p 1
+    SND e < next_lab p 2
 Proof
   ho_match_mp_tac next_lab_ind>>Cases_on`p`>>rw[]>>
   once_rewrite_tac [next_lab_thm]>>fs[extract_labels_def]>>
@@ -5912,11 +5935,11 @@ QED
 
 Theorem stack_alloc_lab_pres:
     ∀n nl p aux.
-  EVERY (λ(l1,l2). l1 = n ∧ l2 ≠ 0) (extract_labels p) ∧
+  EVERY (λ(l1,l2). l1 = n ∧ l2 ≠ 0 ∧ l2 ≠ 1) (extract_labels p) ∧
   ALL_DISTINCT (extract_labels p) ∧
-  next_lab p 1 ≤ nl ⇒
+  next_lab p 2 ≤ nl ⇒
   let (cp,nl') = comp n nl p in
-  EVERY (λ(l1,l2). l1 = n ∧ l2 ≠ 0) (extract_labels cp) ∧
+  EVERY (λ(l1,l2). l1 = n ∧ l2 ≠ 0 ∧ l2 ≠ 1) (extract_labels cp) ∧
   ALL_DISTINCT (extract_labels cp) ∧
   (∀lab. MEM lab (extract_labels cp) ⇒ MEM lab (extract_labels p) ∨ (nl ≤ SND lab ∧ SND lab < nl')) ∧
   nl ≤ nl'
@@ -5934,7 +5957,7 @@ Proof
       (CCONTR_TAC>>fs[]>>
       res_tac>>fs[])
     >>
-      `next_lab q 1 ≤ m'` by fs[]>>
+      `next_lab q 2 ≤ m'` by fs[]>>
       fs[]>>rfs[]>>
       `r < nl ∧ r' < nl` by
         fs[MAX_DEF]>>
@@ -6009,7 +6032,7 @@ Proof
   fs[EVERY_MAP,EVERY_MEM,FORALL_PROD,prog_comp_def]>>
   rw[]>>res_tac>>
   drule stack_alloc_comp_stack_asm_name>>fs[]>>
-  disch_then(qspecl_then[`p_1`,`next_lab p_2 1`] assume_tac)>>
+  disch_then(qspecl_then[`p_1`,`next_lab p_2 2`] assume_tac)>>
   pairarg_tac>>fs[]
 QED