Update VST Iris support for Rocq dev and current dependencies - #865
Draft
JasonGross wants to merge 8 commits into
Draft
Update VST Iris support for Rocq dev and current dependencies#865JasonGross wants to merge 8 commits into
JasonGross wants to merge 8 commits into
Conversation
This file was generated by clightgen 3.10 and is checked in; CompCert 3.17 changed two things it depends on. 1. [typelist] ([Tnil]/[Tcons]) was replaced by [list type]. Shimmed with two [Local Notation]s, following the precedent in lib/proof/spec_threads.v. 2. [AST.rettype] was replaced by [AST.xtype], its constructors renamed T* -> X*, and [sig_args] retyped from [list typ] to [list xtype]. These occurrences are written qualified ([AST.Tint]), which a [Local Notation] cannot shadow, so the six names in use are renamed in place: Tint/Tlong/Tfloat/Tsingle -> Xint/Xlong/Xfloat/Xsingle, Tvoid -> Xvoid, Tint16unsigned -> Xint16unsigned. The rename is meaning-preserving -- [proj_xtype Xint = Tint] and likewise for the others -- and is exactly what clightgen 3.17 emits for these tokens. We deliberately do NOT regenerate the file with clightgen 3.17: the regenerated output drops identifiers this development refers to and changes the pointer depth of [gvar_info], which breaks dependent proofs silently. The file now compiles. It is outside the `vst` make target, so this does not affect coq-vst / coq-vst-32. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
… veric/bi.v The VST-side Iris files were last touched in 2022 (ab599ce, Iris 4.0.0) and have not tracked Iris since. None of what follows is Rocq-dev drift. Complete, and regression-tested against the `vst` target on both bitsizes: * veric/bi.v: [iris.proofmode.tactics] -> [iris.proofmode.proofmode]; the former module no longer exists. * Lower the VST [|==>] and [|={E1,E2}=>] / [|={E}=>] notations from level 99 to level 20 in msl/ghost_seplog.v, veric/ghosts.v and veric/fupd.v, matching the levels Iris reserves in iris/bi/notation.v. Argument levels are unchanged. A notation's level is global per notation string, so the two developments must agree. `make vst` is byte-for-byte unchanged in scope on 64-bit and 32-bit (msl 59, veric 86, floyd 81 .vo, all three simpleconc targets), exit 0. Partial -- veric/bi.v still does NOT compile: * Iris renamed the third OfeMixin field [mixin_dist_S] (x ={S n}= y -> x ={n}= y) to [mixin_dist_le] (x ={n}= y -> m <= n -> x ={m}= y). The proof of [mpred_ofe_mixin] is adjusted for the extra index and hypothesis. * Iris generalised step-indices to an abstract type [sidx]. With the finite instance [natSI] the index is [nat] and [(n <= m)%sidx] is convertible to [(n <= m)%nat], but [lia] does not unfold the [sidx] projections. Added a [sidx_lia] tactic that peels them off, and used it for the [chain_cauchy] side conditions. * [Cofe] gained the transfinite bounded-limit operator [lbcompl] and its laws, so it can no longer be built from [compl] alone. [mpred_cofe] now goes through Iris's own finite-step-index constructor [cofe_finite]. * REMAINING BLOCKER: Iris split [bi_persistently] out of [BiMixin] into a separate [BiPersistentlyMixin], and the [bi] structure now takes BiMixin + BiPersistentlyMixin + BiLaterMixin. [mpred_bi_mixin] is one 40-bullet [split] covering all of them and must be re-partitioned. That is a porting project, not a fix, and it is where this file stops. veric/bi.v did not compile before these changes either. It and atomics/hashtable_atomic.v are outside the `vst` make target, so coq-vst and coq-vst-32 are unaffected; this is all on the coq-vst-iris path. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
Two remaining pieces of Iris drift, on top of the OfeMixin/sidx/Cofe fixes in ccfaf5b. 1. Iris moved [bi_persistently] out of [BiMixin] into its own [BiPersistentlyMixin], and [Structure bi] gained a [bi_bi_persistently_mixin] field between the bi and later mixins. Split [mpred_bi_mixin] accordingly: drop the trailing [persistently] argument, and relocate the [persistently_ne] bullet plus the final seven persistently bullets into a new [mpred_bi_persistently_mixin]. The eight bullets were already in exactly the order [BiPersistentlyMixin] declares its fields (ne, mono, idemp_2, emp_2, and_2, exist_1, absorbing, and_sep_elim), so no proof text changed -- this is pure relocation. [mpred_bi_later_mixin] already had the 4.x shape and is untouched. 2. [dist_later] is now a record quantifying over all smaller step-indices rather than a [match] on the index, so [unfold dist_later] no longer works. Use iris's own backwards-compatibility bridge [dist_later_fin_iff]: [dist_later_fin] is definitionally the [match] that [mpred_later_contractive] was written against, so the rest of that proof is unchanged. veric/bi.v now compiles clean against rocq-iris dev.2026-07-27. It remains outside the `vst` make target, so coq-vst / coq-vst-32 are unaffected. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
concurrency/ghostsI.v now COMPILES. Two independent breakages: 1. [valid] resolved to stdpp's cmra validity class rather than VST's [ghost.valid], so the local restatements of own_alloc_strong / own_alloc / own_list_alloc / own_list_alloc' no longer matched the lemmas they [exact]. Qualified as [ghost.valid] at the four reference sites (the [valid a := True] at the Ghost instance is a field name and is untouched). 2. stdpp changed [map_included] to take a KEY-INDEXED relation ([R : K -> A -> B -> Prop], via [map_relation]) instead of a plain [relation A]. Passing VST's [ord] directly sent instance resolution hunting for a [Lookup] instance and overflowed the stack -- the error is a stack overflow, which does not look like an arity problem at all. Fixed by passing [fun _ => ord]. concurrency/invariants.v is advanced but does NOT yet compile: 3. stdpp's [coPpick_elem_of] now takes [X <> empty] rather than [~ set_finite X]. [set_infinite_non_empty] is the bridge, and the proof then stays in [set_infinite] throughout -- [nclose_infinite] is already stated as [set_infinite (up N)], so the [coPset_infinite_finite] round-trip that used to be needed is now actively wrong. Fixed. 4. NEXT BLOCKER (not fixed): [elem_of_list_In] has been REMOVED from stdpp outright -- there is no rename to chase, and no List.In interop lemma left in stdpp/list_basics.v. The [in_map_iff] chain in [fresh_inv_name] has to be rewritten in terms of stdpp's own [elem_of_list_fmap]/[elem_of_list_lookup]. That is a proof adaptation rather than a rename, and it is where this stops. Neither file is in the `vst` make target; coq-vst / coq-vst-32 are unaffected (`make -q vst` still reports up to date). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01L9BGQT7XUuubV6C619DW4b
Two independent bits of drift, both fixed by naming rather than by adapting any proof. fresh_inv_name: [elem_of_list_In] is now [list_elem_of_In], moved from stdpp/list_basics.v to stdpp/base.v with the statement unchanged ([x in l <-> In x l]). It is part of a wider [elem_of_list_*] -> [list_elem_of_*] rename, but only this one link of the chain moved -- [elem_of_list_to_set] (stdpp/sets.v) and [elem_of_gset_to_coPset] (stdpp/coPset.v) kept their names, so the surrounding chain stands as written. later_nonexpansive1: iris/bi/extensions.v exports a [later_contractive] projection ([Contractive (bi_later (PROP:=PROP))]) that shadows VST's [msl/contractive.v] lemma. Qualified to [contractive.later_contractive], which is the idiom this file already used for [contractive.wand_nonexpansive]. The error to recognise is [Unable to unify "bi_car ?PROP" with "predicates_hered.pred rmap"]: an Iris-flavoured type where an rmap one belongs. concurrency/invariants.vo now builds clean against rocq-dev.
iris/bi/lib/atomic.v:231 states [atomic_update_mask_weaken] as Eo1 subseteq Eo2 -> atomic_update Eo1 Ei a b Phi -* atomic_update Eo2 Ei a b Phi where it used to conclude with an entailment. At the top level a wand reads [emp |-- _ -* _], which no longer unifies with a goal of the form [_ |-- _]; the error names [emp |-- atomic_update ?Eo1 .. -* ..] against VST's [derives], which makes it look like a bi-vs-derives mismatch rather than a shape change. The statement is otherwise identical, so introducing the hypothesis and applying through the wand suffices. This one lemma was also the sole blocker for atomics/SC_atomics.v, which needed no edit of its own.
Two unrelated failures in the same proof. forward_if reported only "No matching clauses for match", which names nothing. That message comes from the outer [match goal] of [forward_if'_new] (floyd/forward.v:2891); since [match goal] backtracks, a clause whose body fails is reported as if no clause matched, and the real error is discarded. Re-running that clause under [lazymatch] gives it: [Hypothesis Delta_specs depends on the bodies of Heqv0 v0], a clearbody failure from the [remember]/[subst] pair inside [do_compute_expr_helper2] (floyd/forward.v:1726-1748). [remember] abstracts its term everywhere, including inside the body of the let-bound [Delta_specs], and the following [subst] then cannot clear it. Calling floyd's own [clear_Delta_specs] first drops that body; nothing later in the proof needs it. No change to floyd. Separately, the impossible branch of each [forward_if] now arrives as a bare arithmetic contradiction rather than as [False]: [H : 1 = 0] in the first bullet and [H : 0 <> 0] in the second. [contradiction] acts on neither and [discriminate] only on the first, so both bullets use [congruence].
…nFun Six fixes for rocq-dev (9.4+alpha) / current iris: - body_add_item's atomic commit: pass the committed bool to "Hclose" explicitly ($! ...) instead of letting iApply unify for it. Left to guess, iApply now instantiates it delta-expanded through EqDec_Z, which desynchronises the later if_tac and surfaces as an unrelated unification failure thirty lines away. - Three sites where iFrame now instantiates an existential itself when framing a resource determines the witness; the iExists that used to follow has nothing left to introduce and fails with "... not an existential". Delete the redundant iExists. - forward_if no longer substitutes the branch condition, so List.filter id [b] stays stuck as "if b then [b] else []" and Zlength_cons finds no cons. Case on b in both branches. - FinFun.Injective_map_NoDup moved to Stdlib.Lists.Finite. Verified: atomics/verif_hashtable_atomic.vo builds clean against the rocq-dev switch.
Collaborator
|
Thank you for working on this. |
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
2 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.
Update
coq-vst-irisfor Rocq dev, CompCert 3.17, stdpp 1.12, and Iris 4.x. The changes adapt the CompCert Clight AST, Iris BI/persistently mixins and proof-mode notation/imports, stdpp lemmas,atomic_update_mask_weaken, and the atomic lock and hashtable proofs.All 11 files beyond
make vstcompiled against the Rocq development switch. The separately validatedcoq-vstandcoq-vst-32targets need no Rocq source changes. #861 covers the excluded opam-bound commits.Wordsmithed by Codex.