From 255052ab244022e6d2a13d47516cfa920209457a Mon Sep 17 00:00:00 2001
From: Magnus Myreen <magnus.myreen@cl.cam.ac.uk>
Date: Tue, 10 Jan 2023 09:50:25 +0800
Subject: [PATCH 01/11] Define every_exp for source AST

---
 semantics/astScript.sml | 35 +++++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)

diff --git a/semantics/astScript.sml b/semantics/astScript.sml
index f59e7db0b9..f569d86617 100644
--- a/semantics/astScript.sml
+++ b/semantics/astScript.sml
@@ -275,4 +275,39 @@ Definition pat_bindings_def:
   pats_bindings ps (pat_bindings p already_bound)
 End
 
+Definition every_exp_def[simp]:
+  (every_exp p (Raise e) ⇔
+             p (Raise e) ∧ every_exp p e) ∧
+  (every_exp p (Handle e pes) ⇔
+             p (Handle e pes) ∧ every_exp p e ∧ EVERY (λ(pat,e). every_exp p e) pes) ∧
+  (every_exp p (ast$Lit l) ⇔
+             p (ast$Lit l)) ∧
+  (every_exp p (Con cn es) ⇔
+             p (Con cn es) ∧ EVERY (every_exp p) es) ∧
+  (every_exp p (Var v) ⇔
+             p (Var v)) ∧
+  (every_exp p (Fun x e) ⇔
+             p (Fun x e) ∧ every_exp p e) ∧
+  (every_exp p (App op es) ⇔
+             p (App op es) ∧ EVERY (every_exp p) es) ∧
+  (every_exp p (Log lop e1 e2) ⇔
+             p (Log lop e1 e2) ∧ every_exp p e1 ∧ every_exp p e2) ∧
+  (every_exp p (If e1 e2 e3) ⇔
+             p (If e1 e2 e3) ∧ every_exp p e1 ∧ every_exp p e2 ∧ every_exp p e3) ∧
+  (every_exp p (Mat e pes) ⇔
+             p (Mat e pes) ∧ every_exp p e ∧ EVERY (λ(pat,e). every_exp p e) pes) ∧
+  (every_exp p (Let x e1 e2) ⇔
+             p (Let x e1 e2) ∧ every_exp p e1 ∧ every_exp p e2) ∧
+  (every_exp p (Tannot e a) ⇔
+             p (Tannot e a) ∧ every_exp p e) ∧
+  (every_exp p (Lannot e a) ⇔
+             p (Lannot e a) ∧ every_exp p e) ∧
+  (every_exp p (FpOptimise sc e) ⇔
+             p (FpOptimise sc e) ∧ every_exp p e) ∧
+  (every_exp p (Letrec funs e) ⇔
+             p (Letrec funs e) ∧ every_exp p e ∧ EVERY (λ(n,v,e). every_exp p e) funs)
+Termination
+  WF_REL_TAC ‘measure $ exp_size o SND’
+End
+
 val _ = export_theory()

From c98406d3b9e090e111344354036e0a7f9324af5f Mon Sep 17 00:00:00 2001
From: Magnus Myreen <magnus.myreen@cl.cam.ac.uk>
Date: Tue, 10 Jan 2023 18:59:24 +0800
Subject: [PATCH 02/11] Add con_check to the top of Dlet and Dletrec

---
 semantics/evaluateScript.sml           | 8 ++++++--
 semantics/semanticPrimitivesScript.sml | 5 +++++
 2 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/semantics/evaluateScript.sml b/semantics/evaluateScript.sml
index d8f65e227c..bd80d777b7 100644
--- a/semantics/evaluateScript.sml
+++ b/semantics/evaluateScript.sml
@@ -243,7 +243,9 @@ Definition evaluate_def[nocompute]:
      | (st1,Rerr v7) => (st1,Rerr v7))
   ∧
   evaluate_decs st env [Dlet locs p e] =
-    (if ALL_DISTINCT (pat_bindings p []) then
+    (if ALL_DISTINCT (pat_bindings p []) ∧
+        every_exp (one_con_check env.c) e
+     then
        case evaluate st env [e] of
          (st',Rval v) =>
            (st',
@@ -257,7 +259,9 @@ Definition evaluate_def[nocompute]:
   ∧
   evaluate_decs st env [Dletrec locs funs] =
     (st,
-     if ALL_DISTINCT (MAP (λ(x,y,z). x) funs) then
+     if ALL_DISTINCT (MAP (λ(x,y,z). x) funs) ∧
+        EVERY (λ(f,n,e). every_exp (one_con_check env.c) e) funs
+     then
        Rval <|v := build_rec_env funs env nsEmpty; c := nsEmpty|>
      else Rerr (Rabort Rtype_error))
   ∧
diff --git a/semantics/semanticPrimitivesScript.sml b/semantics/semanticPrimitivesScript.sml
index 4d2e602911..e98b4c4804 100644
--- a/semantics/semanticPrimitivesScript.sml
+++ b/semantics/semanticPrimitivesScript.sml
@@ -249,6 +249,11 @@ Definition do_con_check_def:
     | SOME n => case nsLookup cenv n of NONE => F | SOME (l',v2) => l = l'
 End
 
+Definition one_con_check_def[simp]:
+  one_con_check envc (Con cn es) = do_con_check envc cn (LENGTH es) ∧
+  one_con_check envc _ = T
+End
+
 Definition build_conv_def:
   build_conv (envC:((string),(string),(num#stamp))namespace) cn vs =
   case cn of

From 116e60ebac10cb6d38688e10f49cf11ccb270e14 Mon Sep 17 00:00:00 2001
From: tanyongkiam <tanyongkiam@gmail.com>
Date: Tue, 10 Jan 2023 22:49:06 +0800
Subject: [PATCH 03/11] fix semantics/proofs

---
 semantics/proofs/fpSemPropsScript.sml   |  2 ++
 semantics/proofs/typeSoundScript.sml    | 41 +++++++++++++++++++++++--
 semantics/proofs/typeSysPropsScript.sml |  1 +
 3 files changed, 42 insertions(+), 2 deletions(-)

diff --git a/semantics/proofs/fpSemPropsScript.sml b/semantics/proofs/fpSemPropsScript.sml
index aa572be13c..5fcac1ddb4 100644
--- a/semantics/proofs/fpSemPropsScript.sml
+++ b/semantics/proofs/fpSemPropsScript.sml
@@ -417,6 +417,7 @@ Proof
   >- (
     reverse TOP_CASE_TAC \\ fs[]
     >- solve_simple
+    >- solve_simple
     \\ ntac 2 (reverse TOP_CASE_TAC \\ gs[])
     >- solve_simple
     \\ TOP_CASE_TAC \\ gs[]
@@ -761,6 +762,7 @@ Proof
   >- (
     reverse TOP_CASE_TAC \\ gs[]
     >- gs[fpState_component_equality, semState_comp_eq]
+    >- gs[fpState_component_equality, semState_comp_eq]
     \\ ntac 2 $ reverse TOP_CASE_TAC \\ gs[]
     >- solve_simple
     \\ TOP_CASE_TAC \\ gs[]
diff --git a/semantics/proofs/typeSoundScript.sml b/semantics/proofs/typeSoundScript.sml
index 2bef705736..468d4e28f0 100644
--- a/semantics/proofs/typeSoundScript.sml
+++ b/semantics/proofs/typeSoundScript.sml
@@ -2261,6 +2261,40 @@ Proof
   \\ metis_tac [nsAll2_nsAppend]
 QED
 
+Theorem type_e_con_check:
+ (!tenv tenvE e t.
+   type_e tenv tenvE e t ⇒
+   nsAll2 (type_ctor ctMap) envc tenv.c ⇒
+   every_exp (one_con_check envc) e) ∧
+ (!tenv tenvE es ts.
+   type_es tenv tenvE es ts ⇒
+   nsAll2 (type_ctor ctMap) envc tenv.c ⇒
+   EVERY (every_exp (one_con_check envc)) es) ∧
+ (!tenv tenvE funs env.
+   type_funs tenv tenvE funs env ⇒
+   nsAll2 (type_ctor ctMap) envc tenv.c ⇒
+   EVERY (λ(f,n,e). every_exp (one_con_check envc) e) funs)
+Proof
+  ho_match_mp_tac type_e_strongind >>
+  rw[]>>fs[]
+  >- (
+    fs [FORALL_PROD, RES_FORALL,EVERY_MEM]>>
+    metis_tac[])
+  >- (
+    imp_res_tac nsAll2_nsLookup2>>
+    fs[do_con_check_def]>>
+    TOP_CASE_TAC>>rw[]>>
+    fs[type_ctor_def]>>
+    drule type_es_length>>simp[])
+  >- metis_tac[ETA_AX]
+  >- simp[do_con_check_def]
+  >- metis_tac[ETA_AX]
+  >- metis_tac[ETA_AX]
+  >- (
+    fs [FORALL_PROD, RES_FORALL,EVERY_MEM]>>
+    metis_tac[])
+QED
+
 Theorem decs_type_sound_no_check:
   ∀(st:'ffi semanticPrimitives$state) env ds st' r ctMap tenvS tenv tids tenv'.
    evaluate_decs st env ds = (st',r) ∧
@@ -2383,7 +2417,8 @@ Proof
    >- let_tac)
  >- ( (* case let, duplicate bindings *)
    fs [Once type_d_cases]
-   >> fs [])
+   >> fs [type_sound_invariant_def,type_all_env_def]
+   >> metis_tac[type_e_con_check])
  >- ( (* case letrec *)
    drule type_d_tenv_ok
    >> fs [Once type_d_cases]
@@ -2410,7 +2445,9 @@ Proof
    >> rfs [EVERY2_MAP, tenv_add_tvs_def])
  >- ( (* case letrec duplicate bindings *)
    fs [Once type_d_cases]
-   >> metis_tac [type_funs_distinct])
+   >- metis_tac [type_funs_distinct]
+   >> fs [type_sound_invariant_def,type_all_env_def]
+   >> metis_tac[type_e_con_check,NOT_EVERY])
  >- ( (* case type definition *)
    drule type_d_tenv_ok
    >> fs [Once type_d_cases]
diff --git a/semantics/proofs/typeSysPropsScript.sml b/semantics/proofs/typeSysPropsScript.sml
index 3dd93a482f..e0660803ee 100644
--- a/semantics/proofs/typeSysPropsScript.sml
+++ b/semantics/proofs/typeSysPropsScript.sml
@@ -1615,6 +1615,7 @@ val type_e_subst_lem = Q.prove (
  >> disch_then (qspec_then `Bind_name x 0 t1 Empty` mp_tac)
  >> simp [db_merge_def, deBruijn_subst_tenvE_def, deBruijn_inc0]);
 
+
  (*
 (* ---------- tid_exn_to_tc ---------- *)
 

From c6cb74411f496248098691d33279a61e0fc9f127 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <magnus.myreen@cl.cam.ac.uk>
Date: Mon, 16 Jan 2023 11:58:58 +0100
Subject: [PATCH 04/11] Update alt_semantics for new cons check

---
 semantics/alt_semantics/bigStepScript.sml     | 102 +++---------------
 .../alt_semantics/itree_semanticsScript.sml   |   7 +-
 .../alt_semantics/proofs/bigClockScript.sml   |   6 +-
 .../proofs/bigSmallEquivScript.sml            |  11 +-
 .../proofs/funBigStepEquivScript.sml          |   3 +-
 .../alt_semantics/proofs/interpScript.sml     |   6 +-
 semantics/alt_semantics/smallStepScript.sml   |   9 +-
 7 files changed, 46 insertions(+), 98 deletions(-)

diff --git a/semantics/alt_semantics/bigStepScript.sml b/semantics/alt_semantics/bigStepScript.sml
index e257797e8b..1e0473d514 100644
--- a/semantics/alt_semantics/bigStepScript.sml
+++ b/semantics/alt_semantics/bigStepScript.sml
@@ -393,6 +393,7 @@ Inductive evaluate_dec:
 (! ck env p e v env' s1 s2 locs.
 (evaluate ck env s1 e (s2, Rval v) /\
 ALL_DISTINCT (pat_bindings p []) /\
+every_exp (one_con_check env.c) e /\
 (pmatch env.c s2.refs p v [] = Match env'))
 ==>
 evaluate_dec ck env s1 (Dlet locs p e) (s2, Rval <| v := (alist_to_ns env'); c := nsEmpty |>))
@@ -400,6 +401,7 @@ evaluate_dec ck env s1 (Dlet locs p e) (s2, Rval <| v := (alist_to_ns env'); c :
 /\ (! ck env p e v s1 s2 locs.
 (evaluate ck env s1 e (s2, Rval v) /\
 ALL_DISTINCT (pat_bindings p []) /\
+every_exp (one_con_check env.c) e /\
 (pmatch env.c s2.refs p v [] = No_match))
 ==>
 evaluate_dec ck env s1 (Dlet locs p e) (s2, Rerr (Rraise bind_exn_v)))
@@ -407,28 +409,33 @@ evaluate_dec ck env s1 (Dlet locs p e) (s2, Rerr (Rraise bind_exn_v)))
 /\ (! ck env p e v s1 s2 locs.
 (evaluate ck env s1 e (s2, Rval v) /\
 ALL_DISTINCT (pat_bindings p []) /\
+every_exp (one_con_check env.c) e /\
 (pmatch env.c s2.refs p v [] = Match_type_error))
 ==>
 evaluate_dec ck env s1 (Dlet locs p e) (s2, Rerr (Rabort Rtype_error)))
 
 /\ (! ck env p e s locs.
-(~ (ALL_DISTINCT (pat_bindings p [])))
+(~ (ALL_DISTINCT (pat_bindings p []) /\
+    every_exp (one_con_check env.c) e))
 ==>
 evaluate_dec ck env s (Dlet locs p e) (s, Rerr (Rabort Rtype_error)))
 
 /\ (! ck env p e err s s' locs.
 (evaluate ck env s e (s', Rerr err) /\
-ALL_DISTINCT (pat_bindings p []))
+ALL_DISTINCT (pat_bindings p []) /\
+every_exp (one_con_check env.c) e)
 ==>
 evaluate_dec ck env s (Dlet locs p e) (s', Rerr err))
 
 /\ (! ck env funs s locs.
-(ALL_DISTINCT (MAP (\ (x,y,z) .  x) funs))
+(ALL_DISTINCT (MAP (\ (x,y,z) .  x) funs) /\
+ EVERY (λ(f,n,e). every_exp (one_con_check env.c) e) funs)
 ==>
 evaluate_dec ck env s (Dletrec locs funs) (s, Rval <| v := (build_rec_env funs env nsEmpty); c := nsEmpty |>))
 
 /\ (! ck env funs s locs.
-(~ (ALL_DISTINCT (MAP (\ (x,y,z) .  x) funs)))
+(~ (ALL_DISTINCT (MAP (\ (x,y,z) .  x) funs) /\
+    EVERY (λ(f,n,e). every_exp (one_con_check env.c) e) funs))
 ==>
 evaluate_dec ck env s (Dletrec locs funs) (s, Rerr (Rabort Rtype_error)))
 
@@ -505,62 +512,11 @@ evaluate_decs ck (extend_dec_env new_env env) s2 ds (s3, r))
 evaluate_decs ck env s1 (d::ds) (s3, combine_dec_result new_env r))
 End
 
-(*
-indreln [evaluate_top : forall 'ffi. bool -> sem_env v -> state 'ffi -> top ->
-              state 'ffi * result (sem_env v) v -> bool]
-
-tdec1 : forall ck s1 s2 env d new_env.
-evaluate_dec ck env s1 d (s2, Rval new_env)
-==>
-evaluate_top ck env s1 (Tdec d) (s2, Rval new_env)
-and
-
-tdec2 : forall ck s1 s2 env d err.
-evaluate_dec ck env s1 d (s2, Rerr err)
-==>
-evaluate_top ck env s1 (Tdec d) (s2, Rerr err)
-
-and
-
-tmod1 : forall ck s1 s2 env ds mn specs new_env.
-evaluate_decs ck env s1 ds (s2, Rval new_env)
-==>
-evaluate_top ck env s1 (Tmod mn specs ds) (s2, Rval <| v = nsLift mn new_env.v; c = nsLift mn new_env.c |>)
-
-and
-
-tmod2 : forall ck s1 s2 env ds mn specs err.
-evaluate_decs ck env s1 ds (s2, Rerr err)
-==>
-evaluate_top ck env s1 (Tmod mn specs ds) (s2, Rerr err)
-
-indreln [evaluate_prog : forall 'ffi. bool -> sem_env v -> state 'ffi -> prog ->
-             state 'ffi * result (sem_env v) v -> bool]
-
-empty : forall ck env s.
-true
-==>
-evaluate_prog ck env s [] (s, Rval <| v = nsEmpty; c = nsEmpty |>)
-
-and
-
-cons1 : forall ck s1 s2 s3 env top tops new_env r.
-evaluate_top ck env s1 top (s2, Rval new_env) &&
-evaluate_prog ck (extend_dec_env new_env env) s2 tops (s3,r)
-==>
-evaluate_prog ck env s1 (top::tops) (s3, combine_dec_result new_env r)
-
-and
-
-cons2 : forall ck s1 s2 env top tops err.
-evaluate_top ck env s1 top (s2, Rerr err)
-==>
-evaluate_prog ck env s1 (top::tops) (s2, Rerr err)
-*)
-
 Inductive dec_diverges:
 (! env st locs p e.
-(ALL_DISTINCT (pat_bindings p []) /\ e_diverges env (st.refs, st.ffi) st.fp_state e)
+(ALL_DISTINCT (pat_bindings p []) /\
+ every_exp (one_con_check env.c) e /\
+ e_diverges env (st.refs, st.ffi) st.fp_state e)
 ==>
 dec_diverges env st (Dlet locs p e))
 
@@ -592,34 +548,4 @@ decs_diverges (extend_dec_env new_env env) s2 ds)
 decs_diverges env s1 (d::ds))
 End
 
-(*
-indreln [top_diverges : forall 'ffi. sem_env v -> state 'ffi -> top -> bool]
-
-tdec : forall st env d.
-dec_diverges env st d
-==>
-top_diverges env st (Tdec d)
-
-and
-
-tmod : forall env s1 ds mn specs.
-decs_diverges env s1 ds
-==>
-top_diverges env s1 (Tmod mn specs ds)
-
-indreln [prog_diverges : forall 'ffi. sem_env v -> state 'ffi -> prog -> bool]
-
-cons1 : forall st env top tops.
-top_diverges env st top
-==>
-prog_diverges env st (top::tops)
-
-and
-
-cons2 : forall s1 s2 env top tops new_env.
-evaluate_top false env s1 top (s2, Rval new_env) &&
-prog_diverges (extend_dec_env new_env env) s2 tops
-==>
-prog_diverges env s1 (top::tops)
-*)
 val _ = export_theory()
diff --git a/semantics/alt_semantics/itree_semanticsScript.sml b/semantics/alt_semantics/itree_semanticsScript.sml
index 5587fd4ec9..2922b97231 100644
--- a/semantics/alt_semantics/itree_semanticsScript.sml
+++ b/semantics/alt_semantics/itree_semanticsScript.sml
@@ -645,11 +645,14 @@ End
 
 Definition dstep_def:
   dstep benv st (Decl $ Dlet locs p e) c = (
-    if ALL_DISTINCT (pat_bindings p []) then
+    if ALL_DISTINCT (pat_bindings p []) ∧
+       every_exp (one_con_check (collapse_env benv c).c) e then
       dreturn st c (ExpVal (collapse_env benv c) (Exp e) [] locs p)
     else Dtype_error st.fp_state) ∧
   dstep benv st (Decl $ Dletrec locs funs) c = (
-    if ALL_DISTINCT (MAP FST funs) then
+    if ALL_DISTINCT (MAP FST funs) ∧
+       EVERY (\ (x,y,z) .
+         every_exp (one_con_check (collapse_env benv c).c) z) funs then
       dreturn st c (Env $
         <| v := build_rec_env funs (collapse_env benv c) nsEmpty; c := nsEmpty |>)
     else Dtype_error st.fp_state) ∧
diff --git a/semantics/alt_semantics/proofs/bigClockScript.sml b/semantics/alt_semantics/proofs/bigClockScript.sml
index c7907c55f4..26ab52bbeb 100644
--- a/semantics/alt_semantics/proofs/bigClockScript.sml
+++ b/semantics/alt_semantics/proofs/bigClockScript.sml
@@ -1027,6 +1027,7 @@ Proof
   >- (irule_at Any OR_INTRO_THM1 >> goal_assum drule >> simp[])
   >- (irule_at Any OR_INTRO_THM1 >> goal_assum drule >> simp[])
   >- (irule_at Any EQ_REFL)
+  >- (irule_at Any EQ_REFL)
   >- (
     irule_at Any OR_INTRO_THM2 >> irule_at Any OR_INTRO_THM2 >>
     goal_assum drule >> simp[]
@@ -1039,6 +1040,7 @@ Proof
   >- irule_at Any EQ_REFL
   >- irule_at Any EQ_REFL
   >- irule_at Any EQ_REFL
+  >- irule_at Any EQ_REFL
   >- (irule_at Any EQ_REFL >> simp[] >> pop_assum $ irule_at Any)
   >- (
     irule_at Any OR_INTRO_THM1 >>
@@ -1109,12 +1111,14 @@ Proof
   PairCases_on `cd` >> rename1 `clk,d` >> gvs[FORALL_PROD, LEX_DEF_THM, SF DNF_ss] >>
   Cases_on `d` >> rw[Once evaluate_dec_cases, SF DNF_ss]
   >- ( (* Dlet *)
-    Cases_on `ALL_DISTINCT (pat_bindings p [])` >> gvs[] >>
+    Cases_on `ALL_DISTINCT (pat_bindings p []) ∧
+              every_exp (one_con_check env.c) e` >> gvs[] >>
     qspecl_then [`st with clock := clk`,`env`,`e`] assume_tac big_clocked_total >>
     gvs[] >> Cases_on `r` >> gvs[SF SFY_ss] >>
     Cases_on `pmatch env.c s'.refs p a []` >> gvs[SF SFY_ss]
     )
   >- rw[DISJ_EQ_IMP]
+  >- rw[DISJ_EQ_IMP]
   >- (
     gvs[astTheory.dec_size_def] >>
     drule_at Any evaluate_decs_total_lemma >>
diff --git a/semantics/alt_semantics/proofs/bigSmallEquivScript.sml b/semantics/alt_semantics/proofs/bigSmallEquivScript.sml
index 08629520f0..159e4a9657 100644
--- a/semantics/alt_semantics/proofs/bigSmallEquivScript.sml
+++ b/semantics/alt_semantics/proofs/bigSmallEquivScript.sml
@@ -1483,7 +1483,8 @@ Proof
   rw[Once evaluate_dec_cases, Once dec_diverges_cases, GSYM untyped_safety_exp] >>
   gvs[]
   >- (
-    Cases_on `ALL_DISTINCT (pat_bindings p [])` >>
+    Cases_on `ALL_DISTINCT (pat_bindings p []) ∧
+              every_exp (one_con_check env.c) e` >>
     gvs[GSYM small_big_exp_equiv, to_small_st_def] >>
     eq_tac >- metis_tac[] >> rw[] >>
     PairCases_on `r` >>
@@ -1504,7 +1505,7 @@ Proof
       goal_assum drule >> simp[]
       )
     )
-  >- metis_tac[]
+  >- metis_tac[NOT_EVERY]
   >- metis_tac[NOT_EVERY]
   >- (
     eq_tac >> rw[] >> gvs[EXISTS_PROD, PULL_EXISTS] >>
@@ -1663,6 +1664,8 @@ Proof
     )
   >- (qexists_tac ‘st.fp_state’ >> simp[] >>
       irule_at Any RTC_REFL >> simp[decl_step_def])
+  >- (qexists_tac ‘st.fp_state’ >> simp[] >>
+      irule_at Any RTC_REFL >> simp[decl_step_def,collapse_env_def])
   >- (
     Cases_on `err` >> gvs[small_eval_dec_def] >>
       simp[Once RTC_CASES1, SF decl_step_ss] >>
@@ -1685,6 +1688,10 @@ Proof
   >- (irule RTC_SINGLE >> simp[SF decl_step_ss, collapse_env_def])
   >- (qexists_tac ‘st.fp_state’ >> simp[] >>
       irule_at Any RTC_REFL >> simp[decl_step_def])
+  >- (qexists_tac ‘st.fp_state’ >> simp[] >>
+      irule_at Any RTC_REFL >> simp[decl_step_def] >>
+      IF_CASES_TAC >> fs [collapse_env_def] >>
+      gvs [EVERY_MEM,EXISTS_MEM])
   >- (irule RTC_SINGLE >> simp[SF decl_step_ss])
   >- (
     qexists_tac ‘st.fp_state’ >> simp[] >>
diff --git a/semantics/alt_semantics/proofs/funBigStepEquivScript.sml b/semantics/alt_semantics/proofs/funBigStepEquivScript.sml
index a5fdbfcbab..7e5e6cb681 100644
--- a/semantics/alt_semantics/proofs/funBigStepEquivScript.sml
+++ b/semantics/alt_semantics/proofs/funBigStepEquivScript.sml
@@ -103,7 +103,8 @@ Proof
   imp_res_tac evaluatePropsTheory.eval_no_eval_simulation >> gvs [] >>
   rpt (qpat_x_assum ‘∀x. _’ kall_tac) >>
   gvs [evaluate_eq_run_eval_list] >>
-  gvs [run_eval_def,result_return_def,result_bind_def]
+  gvs [run_eval_def,result_return_def,result_bind_def] >>
+  gvs [EVERY_MEM,EXISTS_MEM]
 QED
 
 Theorem functional_evaluate_decs:
diff --git a/semantics/alt_semantics/proofs/interpScript.sml b/semantics/alt_semantics/proofs/interpScript.sml
index a5d10bca9e..5fa999751b 100644
--- a/semantics/alt_semantics/proofs/interpScript.sml
+++ b/semantics/alt_semantics/proofs/interpScript.sml
@@ -497,7 +497,8 @@ QED
 
 Definition run_eval_dec_def:
   (run_eval_dec env ^st (Dlet _ p e) =
-   if ALL_DISTINCT (pat_bindings p []) then
+   if ALL_DISTINCT (pat_bindings p []) ∧
+      every_exp (one_con_check env.c) e then
      case run_eval env e st of
      | (st', Rval v) =>
          (case pmatch env.c st'.refs p v [] of
@@ -508,7 +509,8 @@ Definition run_eval_dec_def:
    else
      (st, Rerr (Rabort Rtype_error))) ∧
   (run_eval_dec env ^st (Dletrec _ funs) =
-   if ALL_DISTINCT (MAP FST funs) then
+   if ALL_DISTINCT (MAP FST funs) ∧
+      EVERY (λ(_,_,e). every_exp (one_con_check env.c) e) funs then
      (st, Rval <| v := build_rec_env funs env nsEmpty; c := nsEmpty |>)
    else
      (st, Rerr (Rabort Rtype_error))) ∧
diff --git a/semantics/alt_semantics/smallStepScript.sml b/semantics/alt_semantics/smallStepScript.sml
index 06561b7e8a..41b1d74d3d 100644
--- a/semantics/alt_semantics/smallStepScript.sml
+++ b/semantics/alt_semantics/smallStepScript.sml
@@ -396,11 +396,16 @@ val _ = Define `
     Decl d =>
       (case d of
         Dlet locs p e =>
-          if ALL_DISTINCT (pat_bindings p []) then
+          if ALL_DISTINCT (pat_bindings p []) ∧
+             every_exp (one_con_check (collapse_env benv c).c) e
+          then
             Dstep (st, ExpVal (collapse_env benv c) (Exp e) [] locs p, c)
           else Dabort (st.fp_state, Rtype_error)
       | Dletrec locs funs =>
-          if ALL_DISTINCT (MAP (\ (x,y,z) .  x) funs) then
+          if ALL_DISTINCT (MAP (\ (x,y,z) .  x) funs) ∧
+             EVERY (\ (x,y,z) .
+               every_exp (one_con_check (collapse_env benv c).c) z) funs
+          then
             Dstep (st,
               Env <| v := (build_rec_env funs (collapse_env benv c) nsEmpty); c := nsEmpty |>,
               c)

From f4370203be4888b4a7dcc241dcb69fe3622b480c Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Sat, 14 Jan 2023 20:50:01 +0100
Subject: [PATCH 05/11] Fix compiler proofs for new cons_checks

---
 .../backend/proofs/source_evalProofScript.sml    |  8 ++++++++
 .../backend/proofs/source_letProofScript.sml     | 16 +++++++++++++---
 2 files changed, 21 insertions(+), 3 deletions(-)

diff --git a/compiler/backend/proofs/source_evalProofScript.sml b/compiler/backend/proofs/source_evalProofScript.sml
index e9c5afee78..73a0a5ceb3 100644
--- a/compiler/backend/proofs/source_evalProofScript.sml
+++ b/compiler/backend/proofs/source_evalProofScript.sml
@@ -1180,6 +1180,12 @@ Proof
   \\ insts_tac
 QED
 
+Triviality env_rel_imp_c:
+  env_rel x env env' ⇒ env'.c = env.c
+Proof
+  fs [env_rel_def]
+QED
+
 Triviality eval_simulation_Dletrec:
   ^(#get_goal eval_simulation_setup `Case (_, [Dletrec _ _])`)
 Proof
@@ -1187,6 +1193,7 @@ Proof
   \\ eval_cases_tac
   \\ insts_tac
   \\ fs [miscTheory.FST_triple, MAP_MAP_o, o_DEF, ELIM_UNCURRY, ETA_THM]
+  \\ imp_res_tac env_rel_imp_c
   \\ simp [build_rec_env_merge, nsAppend_to_nsBindList]
   \\ irule env_rel_add_nsBindList
   \\ simp []
@@ -1329,6 +1336,7 @@ Proof
     (* big hammer for similar cases *)
     eval_cases_tac
     \\ fs []
+    \\ imp_res_tac env_rel_imp_c
     \\ insts_tac
     \\ fs [do_con_check_def, build_conv_def, do_log_def, do_if_def]
     \\ TRY (drule_then (drule_then assume_tac) can_pmatch_all)
diff --git a/compiler/backend/proofs/source_letProofScript.sml b/compiler/backend/proofs/source_letProofScript.sml
index 3fecc9b056..bf495bd3fd 100644
--- a/compiler/backend/proofs/source_letProofScript.sml
+++ b/compiler/backend/proofs/source_letProofScript.sml
@@ -13,6 +13,12 @@ val _ = set_grammar_ancestry [
   "semanticPrimitivesProps", "misc", "semantics"
   ];
 
+Triviality env_c_lemma:
+  (<|v := build_rec_env q env env1; c := nsEmpty|> +++ env).c = env.c
+Proof
+  fs [extend_dec_env_def]
+QED
+
 Theorem evaluate_lift_let:
   evaluate_decs s env [d] = (s', res) ∧
   res ≠ Rerr (Rabort Rtype_error) ∧
@@ -25,8 +31,13 @@ Proof
     TOP_CASE_TAC \\ gs []
     \\ TOP_CASE_TAC \\ gvs [dest_Letrec_SOME]
     \\ rw [] \\ gs [evaluate_decs_def, evaluate_def]
-    \\ IF_CASES_TAC \\ gs []
-    \\ IF_CASES_TAC \\ gs []
+    \\ reverse IF_CASES_TAC \\ gs [env_c_lemma]
+    >-
+     (qsuff_tac ‘~EVERY (λ(n,v,e'). every_exp (one_con_check env.c) e') q’
+      \\ rpt strip_tac \\ full_simp_tac bool_ss [] \\ fs []
+      \\ fs [EVERY_MEM,EXISTS_MEM,EXISTS_PROD,FORALL_PROD,SF SFY_ss]
+      \\ res_tac \\ fs [])
+    \\ IF_CASES_TAC \\ gs [env_c_lemma]
     \\ gs [extend_dec_env_def]
     \\ ‘<| v := nsAppend (build_rec_env q env nsEmpty) env.v;
            c := env.c|> =
@@ -151,4 +162,3 @@ Proof
 QED
 
 val _ = export_theory ();
-

From 23a28df1d04830baafb81efc06daad4777ea3972 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Mon, 16 Jan 2023 12:00:07 +0100
Subject: [PATCH 06/11] Update ml_progTheory for new cons check

---
 translator/ml_progScript.sml | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/translator/ml_progScript.sml b/translator/ml_progScript.sml
index 012431a0c6..1d084d2ac1 100644
--- a/translator/ml_progScript.sml
+++ b/translator/ml_progScript.sml
@@ -391,7 +391,8 @@ val eval_match_rel_def = Define `
 Theorem Decls_Dlet:
    !env s1 v e s2 env2 locs.
       Decls env s1 [Dlet locs (Pvar v) e] env2 s2 <=>
-      ?x. eval_rel s1 env e s2 x /\ (env2 = write v x empty_env)
+      ?x. eval_rel s1 env e s2 x /\ (env2 = write v x empty_env) /\
+          every_exp (one_con_check env.c) e
 Proof
   simp [Decls_def,evaluate_decs_def,eval_rel_def]
   \\ rw [] \\ eq_tac \\ rw [] \\ fs [bool_case_eq]
@@ -418,6 +419,7 @@ Theorem Decls_Dletrec:
       Decls env s1 [Dletrec locs funs] env2 s2 <=>
       (s2 = s1) /\
       ALL_DISTINCT (MAP (\(x,y,z). x) funs) /\
+      EVERY (λ(f,n,e). every_exp (one_con_check env.c) e) funs /\
       (env2 = write_rec funs env empty_env)
 Proof
   simp [Decls_def,evaluate_decs_def,bool_case_eq,PULL_EXISTS]
@@ -723,6 +725,9 @@ val build_rec_env_APPEND = Q.prove(
 Theorem ML_code_Dletrec:
    !fns locs. ML_code env0 ((comm, s1, prog, env2) :: bls) s2 ==>
       ALL_DISTINCT (MAP (λ(x,y,z). x) fns) ==>
+      EVERY
+        (λ(f,n,e).
+           every_exp (one_con_check (merge_env env2 (ML_code_env env0 bls)).c) e) fns ==>
       let code_env = ML_code_env env0 ((comm, s1, prog, env2) :: bls) in
       let env3 = write_rec fns code_env env2 in
       ML_code env0 ((comm, s1, SNOC (Dletrec locs fns) prog, env3) :: bls) s2
@@ -739,6 +744,7 @@ Theorem ML_code_Dlet_var:
   ∀cenv e s3 x n locs. ML_code env0 ((comm, s1, prog, env1) :: bls) s2 ==>
     eval_rel s2 cenv e s3 x ==>
     cenv = ML_code_env env0 ((comm, s1, prog, env1) :: bls) ==>
+    every_exp (one_con_check (merge_env env1 (ML_code_env env0 bls)).c) e ==>
     let env2 = write n x env1 in let s3_abbrev = s3 in
     ML_code env0 ((comm, s1, SNOC (Dlet locs (Pvar n) e) prog, env2)
         :: bls) s3_abbrev
@@ -750,6 +756,7 @@ QED
 
 Theorem ML_code_Dlet_Fun:
   ∀n v e locs. ML_code env0 ((comm, s1, prog, env1) :: bls) s2 ==>
+    every_exp (one_con_check (merge_env env1 (ML_code_env env0 bls)).c) e ==>
     let code_env = ML_code_env env0 ((comm, s1, prog, env1) :: bls) in
     let v_abbrev = Closure code_env v e in
     let env2 = write n v_abbrev env1 in
@@ -769,7 +776,7 @@ Theorem ML_code_Dlet_Var_Var:
         :: bls) s2
 Proof
   rw []
-  \\ irule (SIMP_RULE std_ss [LET_THM] ML_code_Dlet_var)
+  \\ irule (SIMP_RULE std_ss [LET_THM] ML_code_Dlet_var) \\ fs []
   \\ first_x_assum $ irule_at $ Pos hd
   \\ fs [eval_rel_def,evaluate_def,state_component_equality]
 QED
@@ -786,7 +793,7 @@ Theorem ML_code_Dlet_Var_Ref_Var:
         :: bls) s2_abbrev
 Proof
   rw []
-  \\ irule (SIMP_RULE std_ss [LET_THM] ML_code_Dlet_var)
+  \\ irule (SIMP_RULE std_ss [LET_THM] ML_code_Dlet_var) \\ fs []
   \\ first_x_assum $ irule_at $ Pos hd
   \\ fs [eval_rel_def,evaluate_def,state_component_equality,AllCaseEqs(),
          do_app_def,store_alloc_def, isFpBool_def, getOpClass_def]

From 6a2f4a7efeb53847c1fb85e0e12eef4ee8ef9a97 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Mon, 16 Jan 2023 13:25:36 +0100
Subject: [PATCH 07/11] Get translator to work with new cons check

---
 translator/ml_progLib.sml       | 43 ++++++++++++++++++---------------
 translator/ml_progScript.sml    | 12 +++++++++
 translator/ml_translatorLib.sml |  5 ++--
 3 files changed, 39 insertions(+), 21 deletions(-)

diff --git a/translator/ml_progLib.sml b/translator/ml_progLib.sml
index 9489ec18cb..63116d274d 100644
--- a/translator/ml_progLib.sml
+++ b/translator/ml_progLib.sml
@@ -155,6 +155,8 @@ fun prove_assum_by_conv conv th = let
 
 val prove_assum_by_eval = prove_assum_by_conv reduce_conv
 
+fun eval_every_exp_one_con_check tm = EVAL tm;
+
 fun is_const_str str = can prim_mk_const {Thy=current_theory(), Name=str};
 
 fun find_name name = let
@@ -393,20 +395,17 @@ fun add_Dlet eval_thm var_str = let
         @ [stringSyntax.fromMLstring var_str,unknown_loc])
   in ML_code_upd "add_Dlet" mp_thm
     [solve_ml_imp_mp eval_thm,
-        solve_ml_imp_conv (SIMP_CONV bool_ss []
-            THENC SIMP_CONV bool_ss [ML_code_env_def]),
-        let_env_abbrev ALL_CONV, let_st_abbrev reduce_conv]
+     solve_ml_imp_conv (SIMP_CONV bool_ss []
+                        THENC SIMP_CONV bool_ss [ML_code_env_def]),
+     solve_ml_imp_conv eval_every_exp_one_con_check,
+     let_env_abbrev ALL_CONV, let_st_abbrev reduce_conv]
   end
 
-fun add_Dlet_lit loc n exp =
+fun add_Dlet_lit loc n l =
   let
-    val theVal = EVAL (Parse.Term ‘case evaluate s env [^exp] of |(_, Rval [v]) => v’) |> concl |> rhs
-    val mp_thm =
-      SPECL [exp,“s2:'a semanticPrimitives$state”, theVal, n, loc] (SIMP_RULE std_ss [] ML_code_Dlet_var)
-    val eval_rel_proof = prove (UNDISCH mp_thm |> concl |> dest_imp |> fst, EVAL_TAC >> ntac 2 $ qexists_tac ‘s2.clock’ >> simp[])
-    val clean_mp_thm = UNDISCH mp_thm |> (fn th => MP th eval_rel_proof) |> DISCH_ALL
+    val mp_thm = SPECL [loc,n,l] ML_code_Dlet_var_lit
   in
-    ML_code_upd "add_Dlet_lit" clean_mp_thm [let_env_abbrev ALL_CONV, let_env_abbrev ALL_CONV]
+    ML_code_upd "add_Dlet_lit" mp_thm [let_env_abbrev ALL_CONV, let_env_abbrev ALL_CONV]
 end
 
 fun add_Denv eval_thm var_str = let
@@ -427,8 +426,10 @@ val (n,v,exp) = (v_tm,w,body)
 
 fun add_Dlet_Fun loc n v exp v_name = ML_code_upd "add_Dlet_Fun"
     (SPECL [n, v, exp, loc] ML_code_Dlet_Fun)
-    [let_conv_ML_upd (REWRITE_CONV [ML_code_env_def]),
-        let_v_abbrev v_name ALL_CONV, let_env_abbrev ALL_CONV]
+    [solve_ml_imp_conv eval_every_exp_one_con_check,
+     let_conv_ML_upd (REWRITE_CONV [ML_code_env_def]),
+     let_v_abbrev v_name ALL_CONV,
+     let_env_abbrev ALL_CONV]
 
 fun add_Dlet_Var_Var loc n var_name = ML_code_upd "add_Dlet_Var_Var"
     (SPECL [n, var_name, loc] ML_code_Dlet_Var_Var)
@@ -465,8 +466,10 @@ fun add_Dletrec loc funs v_names = let
         (th, ML_code (ss,envs,v_defs @ vs,mlth)) end
   in ML_code_upd "add_Dletrec"
     (SPECL [funs, loc] ML_code_Dletrec)
-    [solve_ml_imp_conv EVAL, let_conv_ML_upd (REWRITE_CONV [ML_code_env_def]),
-        proc]
+    [solve_ml_imp_conv EVAL,
+     solve_ml_imp_conv eval_every_exp_one_con_check,
+     let_conv_ML_upd (REWRITE_CONV [ML_code_env_def]),
+     proc]
   end
 
 fun get_block_names (ML_code (ss,envs,vs,th))
@@ -519,9 +522,10 @@ fun add_dec dec_tm pick_name s =
   else if is_Dlet dec_tm
           andalso is_Lit (rand dec_tm)
           andalso is_Pvar (rand (rator dec_tm)) then let
-    val (loc,p,l) = dest_Dlet dec_tm
-    val v_tm = dest_Pvar p
-    in add_Dlet_lit loc v_tm l s end
+    val (loc,p,lit) = dest_Dlet dec_tm
+    val l = dest_Lit lit
+    val n = dest_Pvar p
+    in add_Dlet_lit loc n l s end
   else if is_Dlet dec_tm
           andalso is_Var (rand dec_tm)
           andalso is_Pvar (rand (rator dec_tm)) then let
@@ -663,9 +667,10 @@ fun pick_name str =
 (*
 
 val s = init_state
-val dec1_tm = ``Dlet (ARB 1) (Pvar "f") (Fun "x" (Var (Short "x")))``
+val dec1_tm = ``Dlet (ARB 1) (Pvar "f") (Lit (IntLit 5))``
 val dec2_tm = ``Dlet (ARB 2) (Pvar "g") (Fun "x" (Var (Short "x")))``
-val prog_tm = ``[^dec1_tm; ^dec2_tm]``
+val dec3_tm = ``Dletrec (ARB 3) [("foo","n",Var (Short "n"))]``
+val prog_tm = ``[^dec1_tm; ^dec2_tm; ^dec3_tm]``
 
 val s = (add_prog prog_tm pick_name init_state)
 
diff --git a/translator/ml_progScript.sml b/translator/ml_progScript.sml
index 1d084d2ac1..4eb5c3b6c0 100644
--- a/translator/ml_progScript.sml
+++ b/translator/ml_progScript.sml
@@ -754,6 +754,18 @@ Proof
   \\ fs [write_def,merge_env_def,empty_env_def,sem_env_component_equality]
 QED
 
+Theorem ML_code_Dlet_var_lit:
+  ∀loc name l. ML_code env0 ((comm, s1, prog, env1)::bls) s2 ⇒
+    let env2 = write name (Litv l) env1 in let s3_abbrev = s2 in
+      ML_code env0 ((comm,s1,SNOC (Dlet loc (Pvar name) (Lit l)) prog,env2)::bls) s3_abbrev
+Proof
+  rpt strip_tac
+  \\ irule ML_code_Dlet_var \\ fs []
+  \\ pop_assum $ irule_at Any
+  \\ fs [eval_rel_def,evaluateTheory.evaluate_def]
+  \\ fs [semanticPrimitivesTheory.state_component_equality]
+QED
+
 Theorem ML_code_Dlet_Fun:
   ∀n v e locs. ML_code env0 ((comm, s1, prog, env1) :: bls) s2 ==>
     every_exp (one_con_check (merge_env env1 (ML_code_env env0 bls)).c) e ==>
diff --git a/translator/ml_translatorLib.sml b/translator/ml_translatorLib.sml
index b431361395..58d7212d8d 100644
--- a/translator/ml_translatorLib.sml
+++ b/translator/ml_translatorLib.sml
@@ -4197,7 +4197,7 @@ fun hide_ind_goal_rule name th1 =
 
 val _ = (next_ml_names := ["+","+","+","+","+"]);
 
-val def = Define `foo n = if n = 0 then 0 else foo (n-1n)`
+val def = Define `foo n = if n = 0 then 0:num else foo (n-1n)`
 
 val def = listTheory.APPEND;
 val def = sortingTheory.PART_DEF;
@@ -4452,7 +4452,7 @@ val (th,(fname,ml_fname,def,_,pre)) = hd (zip results thms)
    in raise e end;
 
 (*
-val def = Define `d = 5:num`
+val def = Define `d = [5:num]`
 val options = tl [NoInd]
 val options = [NoInd]
 *)
@@ -4524,6 +4524,7 @@ fun translate_options options def =
         val _ = (end_timing start_fun; end_timing start)
         in save_thm(fname ^ "_v_thm",v_thm) end
       else let (* not is_fun *)
+
         val start_v = start_timing "processing val case"
         val th = th |> INST [env_tm |-> get_curr_env()]
         val th = UNDISCH_ALL (clean_assumptions (D th))

From fca3ade4f69f85ed41223b4204540187408a678e Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Mon, 16 Jan 2023 13:39:26 +0100
Subject: [PATCH 08/11] Make sure nsLookup_cons is used

---
 translator/ml_progLib.sml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/translator/ml_progLib.sml b/translator/ml_progLib.sml
index 63116d274d..98757b0776 100644
--- a/translator/ml_progLib.sml
+++ b/translator/ml_progLib.sml
@@ -155,7 +155,10 @@ fun prove_assum_by_conv conv th = let
 
 val prove_assum_by_eval = prove_assum_by_conv reduce_conv
 
-fun eval_every_exp_one_con_check tm = EVAL tm;
+val eval_every_exp_one_con_check =
+  SIMP_CONV (srw_ss()) [semanticPrimitivesTheory.do_con_check_def,ML_code_env_def]
+  THENC DEPTH_CONV nsLookup_conv
+  THENC reduce_conv;
 
 fun is_const_str str = can prim_mk_const {Thy=current_theory(), Name=str};
 
@@ -669,7 +672,8 @@ fun pick_name str =
 val s = init_state
 val dec1_tm = ``Dlet (ARB 1) (Pvar "f") (Lit (IntLit 5))``
 val dec2_tm = ``Dlet (ARB 2) (Pvar "g") (Fun "x" (Var (Short "x")))``
-val dec3_tm = ``Dletrec (ARB 3) [("foo","n",Var (Short "n"))]``
+val dec3_tm = ``Dletrec (ARB 3) [("foo","n",Con (SOME (Short "::"))
+                  [Var (Short "n");Var (Short "n")])]``
 val prog_tm = ``[^dec1_tm; ^dec2_tm; ^dec3_tm]``
 
 val s = (add_prog prog_tm pick_name init_state)

From ae6b86a78d69ba8d03eeaa0f95708f30f57094a1 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Tue, 17 Jan 2023 07:14:23 +0100
Subject: [PATCH 09/11] Fix for new cons check

---
 compiler/repl/evaluate_skipScript.sml | 32 ++++++++++++++++++++++-----
 1 file changed, 26 insertions(+), 6 deletions(-)

diff --git a/compiler/repl/evaluate_skipScript.sml b/compiler/repl/evaluate_skipScript.sml
index b264fb198a..05d3c49aa1 100644
--- a/compiler/repl/evaluate_skipScript.sml
+++ b/compiler/repl/evaluate_skipScript.sml
@@ -2266,12 +2266,28 @@ Proof
   \\ gs [SF SFY_ss]
 QED
 
+Theorem env_rel_one_con_check:
+  env_rel fr ft fe env env1 ⇒
+  one_con_check env1.c = one_con_check env.c
+Proof
+  fs [one_con_check_def,FUN_EQ_THM]
+  \\ strip_tac \\ Cases \\ fs [one_con_check_def]
+  \\ rename [‘do_con_check _ a’] \\ Cases_on ‘a’ \\ fs [do_con_check_def]
+  \\ fs [env_rel_def,ctor_rel_def]
+  \\ pop_assum kall_tac
+  \\ drule namespacePropsTheory.nsAll2_nsLookup_none
+  \\ disch_then $ qspec_then ‘x’ assume_tac
+  \\ rpt (CASE_TAC \\ fs [])
+  \\ drule_all namespacePropsTheory.nsAll2_nsLookup2 \\ fs []
+QED
+
 Theorem evaluate_update_decs_Dlet:
   ^(get_goal "Dlet")
 Proof
-  rw [evaluate_decs_def]
-  >~ [‘¬ALL_DISTINCT _’] >- (
-    first_assum (irule_at Any) \\ gs [SF SFY_ss])
+  reverse $ rw [evaluate_decs_def]
+  >- (first_assum (irule_at Any) \\ gs [SF SFY_ss]
+      \\ imp_res_tac env_rel_one_con_check \\ fs [])
+  \\ imp_res_tac env_rel_one_con_check
   \\ gvs [CaseEqs ["prod", "result"], PULL_EXISTS]
   \\ first_x_assum (drule_all_then strip_assume_tac) \\ gs []
   \\ Cases_on ‘res1’ \\ gs []
@@ -2297,9 +2313,13 @@ QED
 Theorem evaluate_update_decs_Dletrec:
   ^(get_goal "Dletrec")
 Proof
-  rw [evaluate_decs_def]
-  >~ [‘¬ALL_DISTINCT _’] >- (
-    first_assum (irule_at Any) \\ gs [])
+  reverse $ rw [evaluate_decs_def]
+  >- (first_assum (irule_at Any) \\ gs [SF SFY_ss])
+  >- (CCONTR_TAC \\ fs []
+      \\ imp_res_tac env_rel_one_con_check \\ fs []
+      \\ gvs [EVERY_MEM,EXISTS_MEM] \\ res_tac \\ fs [])
+  >- (imp_res_tac env_rel_one_con_check \\ fs []
+      \\ gvs [EVERY_MEM,EXISTS_MEM] \\ res_tac \\ fs [])
   \\ gvs [CaseEqs ["prod", "result"], PULL_EXISTS]
   \\ first_assum (irule_at Any) \\ gs []
   \\ gs [env_rel_def, ctor_rel_def, PULL_EXISTS, SF SFY_ss,

From 79a3cdc7dd3ecd59549755d29fe7f928c317bac4 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Tue, 17 Jan 2023 09:17:24 +0100
Subject: [PATCH 10/11] Fix for new cons check

---
 .../bootstrap/compilation/x64/64/proofs/replProofScript.sml     | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/compiler/bootstrap/compilation/x64/64/proofs/replProofScript.sml b/compiler/bootstrap/compilation/x64/64/proofs/replProofScript.sml
index 5baf5440b1..ecbc973169 100644
--- a/compiler/bootstrap/compilation/x64/64/proofs/replProofScript.sml
+++ b/compiler/bootstrap/compilation/x64/64/proofs/replProofScript.sml
@@ -1154,7 +1154,7 @@ Proof
   \\ fs [evaluate_decs_def,astTheory.pat_bindings_def]
   \\ simp [Once evaluate_def,evaluate_Var,evaluate_Con,evaluate_list,
            namespaceTheory.nsOptBind_def,evaluate_Lit]
-  \\ CONV_TAC (DEPTH_CONV ml_progLib.nsLookup_conv) \\ simp []
+  \\ CONV_TAC (DEPTH_CONV ml_progLib.nsLookup_conv) \\ simp [do_con_check_def]
   \\ rewrite_tac [main_v_def]
   \\ rewrite_tac [EVAL “semanticPrimitives$do_opapp
        [Recclosure env [("main","u", e)] "main"; Conv NONE []]”] \\ simp []

From 8c06d086dd078e98ff013625b7dbcdc5bc2ea6e0 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <myreen@chalmers.se>
Date: Tue, 17 Jan 2023 10:12:37 +0100
Subject: [PATCH 11/11] Fix for new cons check

---
 candle/prover/candle_prover_evaluateScript.sml | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/candle/prover/candle_prover_evaluateScript.sml b/candle/prover/candle_prover_evaluateScript.sml
index b92b47cf54..d3690a0b27 100644
--- a/candle/prover/candle_prover_evaluateScript.sml
+++ b/candle/prover/candle_prover_evaluateScript.sml
@@ -1065,10 +1065,9 @@ QED
 Theorem evaluate_v_ok_decs_Dlet:
   ^(get_goal "Dlet")
 Proof
-  rw [evaluate_decs_def]
-  >~ [‘¬ALL_DISTINCT _’] >- (
-    gs [state_ok_def]
-    \\ first_assum (irule_at Any) \\ gs [SF SFY_ss])
+  reverse $ rw [evaluate_decs_def]
+  >- (gs [state_ok_def]
+      \\ first_assum (irule_at Any) \\ gs [SF SFY_ss])
   \\ gvs [CaseEqs ["prod", "semanticPrimitives$result"]]
   \\ drule_then strip_assume_tac evaluate_sing \\ gvs []
   \\ first_x_assum (drule_all_then strip_assume_tac)
@@ -1086,10 +1085,9 @@ QED
 Theorem evaluate_v_ok_decs_Dletrec:
   ^(get_goal "Dletrec")
 Proof
-  rw [evaluate_decs_def]
-  >~ [‘¬ALL_DISTINCT _’] >- (
-    gs [state_ok_def]
-    \\ first_assum (irule_at Any) \\ gs [])
+  reverse $ rw [evaluate_decs_def]
+  >- (gs [state_ok_def]
+      \\ first_assum (irule_at Any) \\ gs [SF SFY_ss])
   \\ gvs [CaseEqs ["prod", "semanticPrimitives$result"]]
   \\ first_assum (irule_at Any) \\ gs []
   \\ gs [extend_dec_env_def, build_rec_env_merge, env_ok_def,