Merge pull request #921 from CakeML/cons_check

Add a cons check to Dlet and Dletrec in source semantics

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,

compiler/backend/proofs/source_evalProofScript.sml

@@ -1180,13 +1180,20 @@ 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
   rpt disch_tac
   \\ 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)

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 ();
-

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 []

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,

semantics/alt_semantics/bigStepScript.sml

@@ -393,42 +393,49 @@ 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 |>))
 
 /\ (! 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)))
 
 /\ (! 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()

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) ∧

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 >>

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[] >>