Conversation
dongjaelee1
left a comment
dongjaelee1
left a comment
There was a problem hiding this comment.
I don't see a clear motivation behind some examples.
Otherwise LGTM
There was a problem hiding this comment.
I thinks Cross-STS sim idea in this file is cool, but I don't get the motivation behind this.
Probably merge Example5.v and Example7.v into a single file and come up with a better example that demonstrates Cross-STS technique, if you want to keep this idea in the tutorial.
But again, I don't see a clear motivation in keeping this idea in the tutorial.
There was a problem hiding this comment.
Motivation is simple: sometimes users want to prove behavioral refinement between two semantics that are built on different underlying semantics styles (e.g., Imp vs. ITreeLang). For example, I’ve previously proved a simulation between a CompCert-style small-step semantics and an ITree-style semantics.
There was a problem hiding this comment.
I have a few thoughts.
If we are keeping this in the tutorial, we should make "Advance examples" directory and put this there,
because I think this technique is not strictly necessary for the purpose of tutorial (it feels much more specific and advanced).
If we decide to have "Advanced examples" directory and put this technique in there, we should devise a minimal yet motivating example for this technique.
Maybe something like a minimal version of CompCert-ITree simulation (simulation between low-level & high-level languages)?
There was a problem hiding this comment.
If we are keeping this in the tutorial, we should make "Advance examples" directory and put this there, because I think this technique is not strictly necessary for the purpose of tutorial (it feels much more specific and advanced).
I agree about this.
Maybe something like a minimal version of CompCert-ITree simulation (simulation between low-level & high-level languages)?
In my case, I proved a simulation between ITree-style Clight and CompCert-style Clight. Separately, I think it's important to separate concerns: changing the semantics style and proving an optimization pass are really two different proof obligations, so compilation proofs are more naturally done within a single semantics style.
If we decide to have "Advanced examples" directory and put this technique in there, we should devise a minimal yet motivating example for this technique.
That said, one could imagine an exercise where students do program logic reasoning on an ITree-style source language and then prove a compilation pass in CompCert-style semantics. But I worry that would be overkill for a tutorial — as you mentioned before, the semantic-style bridging alone is already nontrivial.
There was a problem hiding this comment.
Reorganized the directory structure — examples are now under tutorial/examples/ and cross-STS examples under tutorial/advanced_examples/. Let me know if you'd prefer a different layout.
Add handle_mem refinement proving ITree semantics with memory handled refines the memory-silent Imp STS for all programs. Proved: - Memory handler (handle_mem) and all helper lemmas - Continuation denotation (denote_cont) and denote_seq_cont - aeval_handle_sim at 3 levels (paco4, _sim, gpaco4) - Combined STS (X_STS) and handled ITree STS - CSkip, CAsgn (with kont dispatch), CSeq cases fully Remaining (Admitted): - CIf, CWhile, CRet, CMemLoad, CMemStore, CExternal cases - Blocking issue: sim_progress needs ps=true, but aeval_handle_sim' may leave ps'=false for deterministic expressions (ANum, AId) - Fix: destruct ps' + kont dispatch for false case Also: added tau;; to denote_com CSeq to ensure source progress. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- Reverted the tau;; added to denote_com CSeq (keeps original semantics) - Added com_size measure and well-founded induction (lt_wf_ind) to handle CSeq chains without requiring source progress - CSkip, CAsgn, CSeq, CIf cases structurally complete (with admits for Step_silent_undefined subcases where source UB needs to be shown) - Key pattern: gstep at top, aeval_handle_sim' for expressions, IHsz for CSeq (smaller command), econs 6 + gfinal.left for CIH - Remaining: CWhile iter unfolding, CRet, CMemLoad/Store, CExternal need individual MCP debugging for bind structure Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Key discoveries: - gstep at top + IHsz (well-founded induction) for CSeq chains - kont_dispatch tactic for Kstop (UB) / Kseq (tau + ES_Skip) dispatch - aeval_handle_sim' for expression eval inside _sim - CWhile WhileTrue: replace continuation with denote_cont via func_ext_dep - No tau;; added to denote_com CSeq (original semantics preserved) Still Admitted - remaining cases need bind structure debugging: - CMemLoad, CMemStore, CExternal bind/norm patterns - Step_silent_undefined subcases (source UB proof) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- Reverted tau;; from denote_com CSeq - Added no_aeval_sim: if aeval doesn't hold, source reaches UB - Main theorem proof structure complete but Admitted - Remaining: CMemLoad/CExternal bind normalization issues Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
2 participants
No description provided.