Conversation
Prove the Loop case for evaluate_stack_swap (stack swap property) and permute_swap_lemma2 (permutation swap property) in wordPropsScript. The evaluate_stack_swap Loop case handles all result types including the complex Exception case with LASTN composition. The permute_swap_lemma2 Loop case uses suspend/Resume/Finalise to isolate the Loop case for cleaner proof development. Remaining cheats in locals_rel_evaluate_thm are pre-existing and require a theorem statement change (Break/Continue cases marked "not true"). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Change the conclusion to give locals_rel (not equality) for Break and Continue results. Use suspend/Resume/Finalise to restructure the proof. Break, Continue, and most other cases are proven. Remaining cheats: Call, Seq, Loop, remaining (Return). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- Change conclusion to give locals_rel for Break/Continue results - Use suspend/Resume/Finalise to restructure proof - Fix all cases: Break, Continue, Seq, Call, and all simple cases - Loop case blocked: every_var for Loop in wordLangScript.sml is always T; needs proper constraint (every_name P names ∧ every_var P c ∧ every_name P exit_names) before this case can be proven Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add proper every_var and every_stack_var clauses for Loop in wordLangScript.sml, then prove the Loop case of locals_rel_evaluate_thm. The key insight is that cut_state normalizes locals to the cutset, so extra temporaries don't affect evaluation. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- max_var_def: add Loop clause computing max over cutset names and body - remove_must_terminate_def: add Loop clause recursing into body - word_remove_correct: prove Loop case using evaluate_add_clock composition for the recursive cont_loop branch Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Definition changes: - inst_select_def: add Loop clause recursing into body - three_to_two_reg_def: add Loop clause recursing into body - pmatch theorems updated for both Proof changes (word_instProofScript.sml): - inst_select_thm statement updated for Break/Continue (locals_rel) - Proof restructured with suspend/Resume for all 9 cases - 7 cases proven (Assign, Set, Store, Seq, MustTerminate, ShareInst, If) - Call and Loop cheated: Loop requires clock induction (inst_select_ind only gives body IH, not recursive IH for loop iteration) - three_to_two_reg_correct: Loop case cheated (same clock induction issue) - Seq case: fixed EVERY_CASE_TAC/metis_tac looping with Break/Continue - ShareInst case: fixed every_case_tac looping in abbreviation proof Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Definition changes: - SimpSeq_def: Break/Continue make following code unreachable - Seq_assoc_right_def: Loop clause recursing into body Proof changes (all complete, no cheats): - evaluate_SimpSeq: works unchanged - evaluate_Loop_body_eq: NEW helper lemma proving Loop with equivalent body evaluates equivalently (by clock induction) - evaluate_Seq_assoc_right_lemma: Loop case proven via evaluate_Loop_body_eq with INST_TYPE to bridge type variable mismatch from Seq_assoc_right_ind - evaluate_remove_unreach: works unchanged Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add Loop clause to find_word_ref_def. Refactor word_removal_lemma proof to use suspend/Resume for all cases. Add Break/Continue cases (trivial) and Loop case with body IH, cont_loop IH, Break 0 exit, and exit_loop handling. Add get_locals_inter_subset helper lemma. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- Added Loop clause to call_graph_def: recurse into body - Break/Continue handled by existing catch-all (Leaf) - Fixed Call case in max_depth_call_graph_lemma for bad_fun_return change in evaluate_def (added rpt strip_tac for vacuous locals_size implications in tail-call cases) - Added Break/Continue cases (trivial) - Loop case: NONE cont_loop subcase proven, exit_loop proven - 2 cheats remain: Continue 0 and Break 0 subcases in Loop need locals_size preservation lemma for Break/Continue results Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add Loop clauses to Seq_assoc, const_fp_loop, simp_duplicate_if, and push_out_if_aux definitions. Fix all proofs: add Loop body congruence lemmas (evaluate_Loop_body_cong, evaluate_Loop_body_cong_gc) proved by clock induction, refactor evaluate_sf_gc_consts with suspend/Resume for Call/Loop cases with Break/Continue result handling. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Strengthen the 2nd conjunct of max_depth_call_graph_lemma to cover Break/Continue results (not just NONE) for locals_size preservation. This is needed because Loop body can return Break/Continue which must preserve locals_size for the Loop proof case. - Fix Loop Resume: NONE case (add conj_tac for strengthened goal), Continue 0 case (mirror NONE proof with Cases_on x''), Break 0 (auto-solved by gvs with strengthened IH), exit_loop (unchanged) - Fix Seq case for strengthened conjunct - Refactor Call into TailCall/NoHandler/WithHandler suspend/Resume - NoHandler/WithHandler: cheated (fs [] too slow with Break/Continue disjuncts in IH — needs proof restructuring for performance) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Definitions: - word_copy: Loop optimizes body from empty_eq (conservative), Break/Continue pass through copy state unchanged - word_cse: Loop optimizes body from empty_data (conservative), Break/Continue pass through CSE data unchanged Proofs: - word_copyProof: evaluate_Loop_body_cong_err helper for Loop body congruence, copy_prop_correct Loop via suspend/Resume - word_cseProof: comp_correct Loop case with clock induction, word_cse_data_conventions refactored to suspend/Resume, Loop cases added to full_inst_ok_less, pre_alloc_conventions, every_inst distinct_tar_reg, every_inst two_reg_inst Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Thread loop target list (lt) through get_live, get_clash_tree, remove_dead, ssa_cc_trans, and colouring_ok to support Loop/Break/Continue. - get_live: Loop pushes (names,exit_names) onto lt; Break/Continue look up exit/entry liveness via oEL - get_clash_tree: same lt threading as get_live - remove_dead: add explicit Loop case to recurse into body with updated lt; Break/Continue handled by catchall - ssa_cc_trans: Loop pushes (ssa,names,exit_names) onto lt for SSA reconciliation; Break/Continue reconcile to entry SSA map - Top-level callers pass [] as initial lt Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add inst_select_Loop_helper using clock induction to prove
that inst_select preserves Loop semantics modulo locals_rel.
Export locals_rel_cut_env{,s} from wordPropsTheory.
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Restructures comp_correct[Call] via suspend/Resume into sub-theorems, adds Loop/Loop_rec/Break/Continue cases, extends state_rel_IMP_semantics and ancillary lemmas (lab_pres, stack_asm_name/remove, alloc_arg, reg_bound) to cover the new constructors. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Threads the new lt parameter through ssa_cc_trans and remove_dead theorem statements in wordConvsProof, and adds Loop/Break/Continue cases across word_simp, word_cse, copy_prop, remove_unreach, and the full_ssa_cc_trans layer. Fixes to_livesets_0_def to supply the empty lt argument to get_clash_tree. In word_bignumProof, adapts the Continue and LoopBody-cont branches of compile_thm to the new bad_fun_return gate on tail-call semantics. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Replace the old Call-NONE-NONE wrap `(NONE,s) => Error | res => res` with `(res,s) => if bad_fun_return res then Error else (res,s)` in four theorems whose statements asserted tail-call-semantics equivalence: InstallCode_code_thm, InstallData_code_thm, evaluate_AppendMainLoop_code_alt and evaluate_AppendLenLoop_code. Proof patches add a Cases_on on the SOME constructor with wordSemTheory.bad_fun_return_def so fs can collapse the Break/Continue branches that the new gate promotes to Error. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adjust get_live (Loop _ body _) to return names (loop entry-live) rather than descending into the body; body's entry-live is re-established via strong_locals_rel extension inside the proof. Add evaluate_apply_colour_Loop_helper via clock induction on st.clock and permute_swap_lemma to close the cont_loop recursion, and Resume blocks for [Loop], [Break], [Continue] that discharge the three new cases. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…Loop/Break/Continue Strengthen wf_cutsets (Loop) to include wf names/exit_names so the clash_tree_colouring_ok body IH can discharge wf live. Restructure get_clash_tree (Loop) to Seq-of-Sets ordering that simultaneously establishes body live=names, INJ on exit_names, and outer livein=names. Switch Break/Continue NONE branch to Set LN (matches get_live = LN). Add EVERY wf premise and reorder quantifiers (lt second) on clash_tree_colouring_ok to match the induction principle; fix call sites. Extend word_alloc_correct's conclusion with Break/Continue as T since evaluate_apply_colour gives T for them when lt=[]. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
remove_dead: Break and Continue now return nlivein = [] instead of passing it through. Pass-through was unsound: store-DCE across a Break/Continue could eliminate a Set whose "overwriting" successor is skipped by the jump (e.g. Set a v1; Break 0; Set a v2). evaluate_remove_dead: post-condition for Break/Continue now asserts rst.store = tstore' (in addition to the locals relation). Holds because Break/Continue set nlivein = [] and the body's remaining Sets on the straight-line path run identically in original and optimised. evaluate_remove_dead_Loop_helper (clock induction), helper's [none]/[break]/[continue] Resume blocks, evaluate_remove_dead[Loop], evaluate_remove_dead[Break]/[Continue]/[Seq]/[CallSome] and evaluate_remove_dead_prog all close cleanly — no cheats remain in the remove_dead block. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds Loop/Break/Continue handling to ssa_cc_trans (compiler/backend/word_allocScript.sml) and discharges the Loop case end-to-end in word_allocProofScript.sml. Verified cheat-free with Status: OK: - ssa_cc_trans_Loop_helper (parent, 241 steps) - Resume ssa_cc_trans_Loop_helper[break0] (26 steps) - Resume ssa_cc_trans_Loop_helper[none] (170 steps) - Resume ssa_cc_trans_Loop_helper[continue0] (236 steps) - ssa_cc_trans_correct[Loop] (74 steps, downstream consumer) NOTE: tactics are still messy. Lots of Resume/Suspend scaffolding, duplicated chains across Skip / non-Skip ssa_reconcile branches, and ad-hoc `simp[Once evaluate_def] >> simp[cut_state_def] >> ... >> fs[...] >> gvs[]` endings in [none]/[continue0]. Worth a tidy-up pass once the rest of the helper structure stabilises.
Holmake --qof now builds word_allocProofTheory (CHEATED, 468s). NOTE: _main body is still messy and worth a tidy-up pass. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
word_allocProofTheory builds OK (~24m, 0 cheats). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
compile_single_correct and no_install_no_alloc_compile_single_correct restructured to suspend/Resume across 26 ctors. word_to_word_compile_semantics ported with cake-while adaptations. Tail-call closes via bad_fun_return_def; IMAGE_CONG tail in compile_semantics extracted to Resume[tail]. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…aluate_stack_size_limit_const_panLang; bad_fun_return discharge in loop_to_word Call/NONE-ret Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Inlines previously-nested Resume blocks into their parent suspend sites and removes a handful of TRY wrappers around now-explicit branching. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Inlines further single-use Resume blocks into their parent suspend sites and collapses a per-ctor transitive_chain duplication. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
tanyongkiam
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.