feat: adequacy interface skeleton (depends on #393)#394
Draft
lihaokun wants to merge 23 commits into
Draft
Conversation
Stuckness inductive + IrisGS typeclass + wp_pre (实定义，命题 1:1 自 Coq Iris
weakestpre.v) + wp/wp_unfold/wp_pre_contractive 接口签名。
Phase 1-A 出口：lake build OK + 4 个预期 sorry：
• COFE (WPFun) — Phase 1-B 用 OFE.discrete_funO
• wp_pre_contractive — Phase 1-B nl-proof
• wp body — Phase 1-B 用 fixpoint (wp_pre s)
• wp_unfold body — Phase 1-B 用 fixpoint_unfold
简化（vs Coq 原版，文件头有注释）：
• num_laters_per_step = 0 （硬编码；Coq 原是 S (num_laters_per_step ns)）
• IrisGS 暂不含 state_interp_mono 字段（Phase 1-B 按需补）
References (三参考交叉)：
• Coq iris/program_logic/weakestpre.v (commit d663f775) — 命题来源（canonical）
• hxrts/iris-lean@fork/iris/vendor:src/Iris/ProgramLogic/WeakestPre.lean — 思路
• upstream Iris/Algebra/OFE.lean (Contractive/fixpoint) +
Iris/Instances/Lib/{WSat,FUpd}.lean (InvGS/uPred_fupd) +
Iris/BI/Updates.lean (|={E1,E2}=>, |={E}▷=∗^[n]) +
Iris/BI/BigOp/BigSepList.lean ([∗list]) — 算子来源
…rive
nl-proof：
- IProp GF = UPred (IResUR GF) → IsCOFE 实例 (Iris/Algebra/UPred.lean:93)
- 函数空间封闭：instance [∀ x, COFE (β x)] : COFE ((x : α) → β x)
(Iris/Algebra/OFE.lean:854) 套用 3 层 (CoPset → Expr → (Val → IProp GF))
修法：删除显式 sorry 实例，typeclass resolution 自动 derive。
Stage 1 sorry 数：4 → 3（剩 wp_pre_contractive / wp / wp_unfold）。
Phase 1-B 第 1 个 sorry 消除（按 D33 D34 nl-proof 纪律）。
…orry)
nl-proof v3：~25 行 tactic（模板 Iris/Examples/IProp.lean:131 wp_F_contractive
11 行同模式）。
结构：
- value case：unfold + simp + .rfl（W 不出现）
- non-value case：透过 5+3 层 forall_ne / 2 层 wand_ne / 4 次 BIFUpdate.ne /
sep_ne / Contractive.distLater_dist (▷ 关键步) / bigSepL_dist
upstream API 全部已验证存在：
• BI.forall_ne (DerivedLaws.lean:122)
• BI.{sep,wand}_ne (BI.lean:35-36)
• BIFUpdate.ne (Updates.lean:108)
• Contractive.distLater_dist (OFE.lean:132) — 用于 ▷ via sbi_later_contractive
(InternalEq.lean:408)
• Iris.BI.BigSepL.bigSepL_dist (BigSepList.lean:77)
工程问题：Nat.repeat _ 1 X = f X 由 rfl 自动 reduce，
{E,∅}=∗ X = wand _ (fupd E ∅ _) macro 展开后透过依次 wand_ne + BIFUpdate.ne。
Stage 1 sorry 数：3 → 2（剩 wp def + wp_unfold，可立即用 fixpoint + fixpoint_unfold）。
首次编译即通过，0 修复迭代——nl-proof v3 工程问题预解决方案有效。
…eanprover-community#3 leanprover-community#4） wp def: - wp s := fixpoint (fun W : WPFun => wp_pre s W) - 依赖 COFE (auto-derive) + Inhabited + wp_pre_contractive 全就位 wp_unfold: - 包装 ContractiveHom { f := fun W => wp_pre s W, contractive := inferInstance } - fixpoint_unfold 给 ≡ at WPFun level - 函数空间 OFE.Equiv pointwise → 应用 (E e Φ) 拿 IProp 层 Equiv - BI.equiv_iff.mp 转 ⊣⊢ Stage 1 全部 4 sorry 消除！0 sorry / 0 axiom 干净 build。 第一个完成真证明的 stage，PR-ready 候选（仍需 stage/2-4 真证明 + maintainer 沟通）。
为 upstream PR 做准备：IrisGS 补 state_interp_mono 字段（Coq weakestpre.v
irisGS_gen 第 5 字段）。
state_interp_mono (σ : State) (ns : Nat) (κs : List Obs) (nt : Nat) :
state_interp σ ns κs nt ⊢ iprop(|={∅}=> state_interp σ (ns + 1) κs nt)
调研结论（不补）：
- num_laters_per_step：hxrts 同样省（precedent）；Phase 1-2 swap/数组不需要
- hlc 参数化：upstream Examples/IProp.lean 不参数化
- Wp typeclass / WP notation：upstream Examples/IProp.lean 不注册
stage/1 现在 5/5 IrisGS 字段（vs Coq 6 字段，仅省 num_laters_per_step
sub-precedent）。0 sorry / 0 axiom build。
IrisGS 加 num_laters_per_step : Nat → Nat 字段（Coq 第 4 字段）。
wp_pre body 用 `={∅}▷=∗^[iG.num_laters_per_step ns + 1]` 替代硬编码 `^[1]`。
新增 helper `step_fupdN_ne`（10 行 induction）：透过 step_fupdN k 层
NonExpansive（每层 BIFUpdate.ne + later_ne + BIFUpdate.ne）。
wp_pre_contractive proof 增加 step_fupdN_ne 调用（透过 num_laters_per_step ns
层后到达内层 inner）；Nat.repeat (S k) X = f (Nat.repeat f k X) by rfl reduce。
stage/1 现在与 Coq Iris weakestpre.v irisGS_gen **6/6 字段全 1:1**：
• iris_invGS → extends InvGS GF
• state_interp ✓
• fork_post ✓
• num_laters_per_step ✓ (新补)
• state_interp_mono ✓ (上次补)
0 sorry / 0 axiom build。Phase 1-B 完整严格 1:1 PR-ready 状态。
…nces for PR Remove all references to hxrts/iris-lean (private fork; PR leanprover-community#149/leanprover-community#150 closed) and to project-internal terminology (Phase 1-A/B, stage/N, CLAUDE.md). Translate Chinese comments to English. All documentation now references only Coq Iris weakestpre.v and upstream iris-lean modules. Module remains 1:1 with Coq Iris weakestpre.v (commit d663f775): - 6/6 IrisGS fields - wp_pre with num_laters_per_step parameterization - wp_pre_contractive proof following Iris/Examples/IProp.lean wp_F_contractive - wp / wp_unfold via upstream fixpoint / fixpoint_unfold
Adds `(hlc : outParam Bool)` parameter to IrisGS, mirroring Coq's `irisGS_gen (hlc : has_lc)`. `extends InvGS GF` becomes `extends InvGS_gen hlc GF`. Also fixes Coq 1:1 match on bigSepL: `[∗list] ef ∈ efs, ...` (was `[∗list] _i ↦ ef ∈ efs, ...` to silence the linter, but upstream syntax supports the index-less form). stage/1 now strictly 1:1 with Coq weakestpre.v's irisGS_gen + wp_pre + wp_pre_contractive + wp + wp_unfold.
Tracks the fixpoint base scope ported in this PR: - Stuckness + IrisGS (all 5 fields) - wp_pre + Contractive instance - wp via fixpoint + wp_unfold via fixpoint_unfold Remaining items in weakestpre.v (wp_value_fupd, wp_strong_mono, wp_mono, fupd_wp, wp_fupd, wp_wand, wp_atomic, wp_frame_l/r, wp_bind/bind_inv) will follow in subsequent PRs.
…is FIXME)
Coq Iris weakestpre.v has a FIXME noting that wp_pre_contractive's proof
would simplify with a 'proper instance for step_fupdN'. This lifts the
NonExpansive lemma for `|={Eo}[Ei]▷=∗^[k]` to Iris/BI/Updates.lean (the
home of step_fupdN), generalized over any [BI PROP] [BIFUpdate PROP].
WeakestPre.lean now imports it from upstream rather than defining a
file-local helper. Also cleans up two small redundancies in opens
(removed redundant 'Iris.BI'; added 'Iris.BI.BigSepL' so the bigSepL_dist
call drops its fully-qualified path).
7 个 lemma 签名（命题 1:1 自 Coq weakestpre.v，proof 全 sorry）： • wp_value_fupd — value 情形 • wp_strong_mono — stuckness + mask + Φ 三维单调性 • wp_mono — Φ 单调（strong_mono 退化版） • fupd_wp — fupd 吸收前 • wp_fupd — fupd 吸收后 • wp_wand — wand 弱化（mono 升级版） • wp_atomic — atomic 表达式 commute 双 fupd + 辅助 def `Stuckness.atomicity : Stuckness → Atomicity` — 避免 typeclass binder 内嵌 match 触发 elaboration 失败。 References： • Coq iris/program_logic/weakestpre.v 各 lemma 1:1 • hxrts WeakestPre.lean:460/1866/3485/1950/2101/3628/3667 (思路) • upstream Iris/ProgramLogic/Language.lean (Atomic + Atomicity)
…prover-community#5) 4 行 tactic：wp_unfold → wp_pre → toVal_coe simp → rfl （toVal (ofVal v) = some v 让 match 走 some 分支 = |={E}=> Φ v） Stage 2 sorry: 7 → 6（剩 wp_strong_mono + 5 个派生）。
…nces for PR Remove hxrts/Phase 1-B/Chinese references in stage/2 lemma section. All 7 lemma statements (wp_value_fupd / wp_strong_mono / wp_mono / fupd_wp / wp_fupd / wp_wand / wp_atomic) remain 1:1 with Coq weakestpre.v.
4 个 lemma 签名（命题 1:1 自 Coq weakestpre.v，proof 全 sorry）： • wp_frame_l — resource framing 左侧 • wp_frame_r — resource framing 右侧 • wp_bind — 通过 evaluation context 复合 • wp_bind_inv — wp_bind 反方向 依赖 upstream `Iris.ProgramLogic.Language.Context K`（[rocq_alias LanguageCtx]）。 References： • Coq iris/program_logic/weakestpre.v 各 lemma 1:1 • hxrts WeakestPre.lean:3530/3575/2152/2872 (思路) wp_lift_* / wp_pure_step 放 stage/4-lifting（依赖 Lifting.lean）。
新文件 Iris/Iris/ProgramLogic/Lifting.lean。6 个 lemma 签名（命题 1:1 自 Coq
lifting.v，proof 全 sorry）：
• wp_lift_step_fupd — base lifting，non-value step → wp
• wp_lift_step — 同上，▷ 代替 inner fupd
• wp_lift_pure_step_no_fork — pure step (κ=[], σ 不变, efs=[])
• wp_lift_atomic_step_fupd — atomic step + fupd
• wp_lift_atomic_step — atomic step plain
• wp_pure_step_later — PureExec → ▷^n wp
依赖 upstream `Iris.ProgramLogic.Language.{Context, PureExec, Atomic}`。
References：
• Coq iris/program_logic/lifting.v 各 lemma 1:1
• hxrts Lifting.lean:701-810 (思路)
…nces for PR Lifting.lean: remove hxrts/Stage 4/Phase references and Chinese comments. All 6 lemma statements (wp_lift_step_fupd / wp_lift_step / wp_lift_pure_step_no_fork / wp_lift_atomic_step_fupd / wp_lift_atomic_step / wp_pure_step_later) remain 1:1 with Coq lifting.v.
按 CLAUDE.md §7 stage/6-adequacy-infra + stage/7-adequacy-main 合并打包 （两 stage 紧耦合，~9 顶级 + 6 内部 helper，无独立拆分价值）。 严格 1:1 翻译 Coq `iris/program_logic/adequacy.v` 全部 ~9 个顶级声明 + 7 个 local helper： §0 基础： - `wptp s es Φs := [∗list] e;Φ ∈ es;Φs, wp s ⊤ e Φ` - `steps_sum num_laters start n` — 累加 num_laters 在 [start, start+n) 上 §1 local lemmas（adequacy.v:21-158）： - `wp_step`（单步保持）/ `wptp_step`（线程池单步） - `wp_not_stuck`（wp ⇒ not_stuck under state_interp） - `wptp_preservation`（n-步保持） - `wptp_postconditions`（n-步终态后置条件聚合） - `wptp_progress`（NotStuck n-步进展） §2-§3 顶层（adequacy.v:161-275）： - `wp_progress_gen` — meta-level 进展定理 - `wp_strong_adequacy_gen` / `wp_strong_adequacy` （WP 存在量化签名暂用 `True` 占位，待 invGpreS 基础设施成熟） §4 corollaries（adequacy.v:281-315）： - `adequate` record（adequate_result + adequate_not_stuck） - `adequate_alt` / `adequate_tp_safe` §5-§6 简化版（adequacy.v:331-381）： - `wp_adequacy_gen` / `wp_adequacy` — state_interp 不依赖 ns/nt 的特化 - `wp_invariance_gen` / `wp_invariance` 全部 proof 留 `sorry`（Phase 1-B 接口骨架，待 ayhon weakestpre PR leanprover-community#393 合入 后真证）。WP 存在量化签名几处暂用 `True` 占位，Phase 5 配套补完整 ∀ binder （需要 `invGpreS` / `IrisG` constructor / `step_fupdN_soundness_gen` 等下游 基础设施）。 依赖： - `Iris.ProgramLogic.Language`（`Step` / `NSteps` / `NotStuck` / `ErasedStep`） - `Iris.ProgramLogic.WeakestPre`（本仓 fork stage/1，命题对齐 Coq Iris） - `Iris.BI.BigOp.BigSepList`（`bigSepL2`） - `Iris.Std.FromMathlib`（`Relation.ReflTransGen`） 度量：246 lines / 17 decls / 9 sorry。 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
按 PR leanprover-community#389 review 反馈套用同样规范： - 17 个顶级 decl 全部加 @[rocq_alias] 注解（wptp / steps_sum / wp_step / wptp_step / wp_not_stuck / wptp_preservation / wptp_postconditions / wptp_progress / wp_progress_gen / wp_strong_adequacy_gen / wp_strong_adequacy / adequate / adequate_alt / adequate_tp_safe / wp_adequacy_gen / wp_adequacy / wp_invariance_gen / wp_invariance） - 删除文件头大段 Contents / Depends-on 注释（重复 namespace 与 import 即可看出） - 删除内联 docstring 中 "Coq adequacy.v line N" 重复信息（保留必要的注解， 例如 `wp_progress_gen` 的 `_hwp : True` 占位说明） - 删除 section header `/-! ## §X ... -/` 装饰（按 PR leanprover-community#389 风格） - adequate record 字段 docstring 精简 度量：246 → 188 lines（-58）。 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
- `adequate_alt` 真证（纯 FOL；不依赖 wp/Iris proof mode）：record ↔ universally-quantified pair 的双向构造（refine ⟨..⟩ 拆 4 子目标各自 elim） - `adequate_tp_safe` 保留 sorry 并加注释（需 Mathlib-style helpers push_neg / List.append_of_mem，Iris.Std 暂未引入） - PORTING.md 加 `adequacy.v` 条目（紧接 weakestpre.v；标 in-progress； 列出已完成 wptp / steps_sum / adequate / adequate_alt，其余 sorry） Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
… 1 less type C) The two pure-FOL self-contained lemmas in adequacy.v now both proven: - adequate_alt (commit 17bdaae) - adequate_tp_safe (this commit) Proof structure follows Coq adequacy.v:302 closely: 1. by_cases on `∀ e ∈ t2, ∃ v, ToVal.toVal e = some v` (classical) 2. Right case: Classical.not_forall to extract witness e2 with no value 3. Apply adequate_not_stuck → PrimStep.NotStuck (e2, σ2) 4. NotStuck := isSome ∨ Reducible; isSome contradicts witness 5. Reducible → primStep; split t2 around e2 via List.append_of_mem; wrap with Step.of_primStep + ⟨obs, ...⟩ for ErasedStep Helpers used (all in Lean core stdlib): - Classical.not_forall (Init.Classical) - List.append_of_mem (Init.Data.List.Lemmas) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
按 Coq adequacy.v 严格 1:1 对齐：补 5 个 local lemma 缺失的 £ premise—— 之前漏看 Coq wp_step / wptp_step / wptp_preservation / wptp_postconditions / wptp_progress 都各自带一个 `£ (S num_laters_per_step ns)` 或 `£ (steps_sum num_laters_per_step ns n)` 作为 hypothesis（用于消耗 later credits 跨过 step_fupd 链）。 - wp_step: 加 `£ (iG.num_laters_per_step ns + 1) -∗` - wptp_step: 同 - wptp_preservation: 加 `£ (steps_sum iG.num_laters_per_step ns n) -∗` - wptp_postconditions: 同 - wptp_progress: 同 - wp_not_stuck: 无 £（Coq 也无），不变 注：当前 fork stage/1 的 `wp_pre` 也缺 £ premise（原 commit b884d99 翻译时 漏看 Coq line 74）。本 PR 暂不改 wp_pre——adequacy 用 `wp` 而非 `wp_pre`， 签名层独立；rebase 到 ayhon leanprover-community#393（其 wp.pre 已正确含 £）后两端自然一致。 `£` 通过 `Iris.Instances.Lib.LaterCredits` 的 `notation:max "£ " i:40 => lc i` （line 60）可见——已被 `Iris.Instances.Lib.FUpd` 间接 import 进来，无需新加 import。 Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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
1 participant
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.
Description
Lean 4 port of
iris/program_logic/adequacy.v, addressing #352. Implementsthe interface skeleton for the adequacy layer.
Status: Draft. Will be marked ready for review once @ayhon's #393
(
weakestpre.v) lands in master, at which point this PR will:wp_pre→wp.pre, etc.)_hwp : Trueplaceholders in the four meta-level theoremswith their real existential signatures (
∀ Hinv : InvGS_gen, ⊢ ∃ stateI Φs fork_post state_interp_mono, IrisG Hinv ...), using whateverconstructor syntax feat: add weakest precondition #393 finalizes for
IrisGS_gen.Overlap with #393
This PR currently includes 3 extra files (
WeakestPre.lean,Lifting.lean,and
step_fupdN_neinUpdates.lean) carried from my fork's localstage/1-stage/4branches, because adequacy needs the wp interface and itisn't in master yet. These are not part of this PR's review scope — they
will be deleted on rebase when #393 + lifting land. Reviewers can focus on
Iris/ProgramLogic/Adequacy.lean+ thePORTING.mdentry.Scope (1:1 with Coq
adequacy.v)Definitions
wptp s es Φs—[∗list] e;Φ ∈ es;Φs, WP e @ s; ⊤ {{ Φ }}(Coq line 19)steps_sum num_laters start n— accumulatednum_laters_per_stepover nphysical steps (Coq line 57)
adequaterecord — postcondition + progress (Coq line 281)Local lemmas (Coq lines 21-158)
wp_step/wptp_step/wp_not_stuckwptp_preservation/wptp_postconditions/wptp_progressTop-level theorems (Coq lines 161-381)
wp_progress_gen/wp_strong_adequacy_gen/wp_strong_adequacyadequate_alt(proven) /adequate_tp_safe(proven)wp_adequacy_gen/wp_adequacywp_invariance_gen/wp_invarianceSorry inventory
wp_step/wptp_step/wp_not_stuck/wptp_preservation/wptp_postconditions/wptp_progress(6)wp_unfold/wp_strong_mono/fupd_wp/ etc.wp_progress_gen/wp_strong_adequacy_gen/wp_adequacy_gen/wp_invariance_gen(4)∀ Hinv, ⊢ |={⊤}=> ∃ stateI ...) abstracted as_hwp : True. The required infrastructure (InvGpreS,InvGS_gen,step_fupdN_soundness_gen) is already inIris/Instances/Lib/FUpd.lean; the blocker is theIrisGS_genconstructor / extends-chain syntax, which is being finalized in #393.adequate_alt/adequate_tp_safeConventions followed (per PR #389 review)
@[rocq_alias]annotationsCoq counterpart by name)
Context
I'm porting VST to Lean 4 (see #389). The split agreed with @ayhon:
weakestpre.v(feat: add weakest precondition #393) +lifting.v(Port program_logic/lifting.v #348) +ectx_lifting.v(Port program_logic/ectx_lifting.v #349)adequacy.v(this PR, Port program_logic/adequacy.v #352)Checklist
adequacy.ventry)