Backport three rocqchk fixes (vm_caml_prim arity, -norec validation order, VM bytecode trust) - #9
Merged
archanaburra merged 4 commits intoAug 18, 2026
Conversation
checker/values.ml capped vm_caml_prim at 6, the number of caml_prim constructors when the VM validator was added in 09336f2. 15c0443 grew the type to 12 by adding the string primitives without updating the validator, so rocqchk -bytecode-compiler yes failed to intern any .vo whose VM data references one, including Corelib.Strings.PrimString. Fixes rocq-prover#22360. (cherry picked from commit d9af170)
rocqchk read the marshalled data of a library without validation whenever it was interned in Dep mode, that is as a dependency of a -norec argument. Since the first intern of a library wins and the -norec roots are interned in reverse command line order, a library named with -norec could be pulled in as a dependency of another one and read raw, with neither structural validation nor a comparison of the recorded segment checksums. Which files were validated thus depended on the order of the -norec arguments. Force validation for the libraries named on the command line, minus those named with -admit. What gets checked is unchanged. Fixes rocq-prover#22362. (cherry picked from commit 527737e)
rocqchk with -bytecode-compiler yes typechecked each constant's body but took the VM bytecode from the separately serialized vmlibrary segment of the .vo, with nothing binding the two together. A crafted file whose vmlibrary disagrees with its library makes a VM conversion prove False, and rocqchk accepts the result with no axioms reported. The checker now compiles the bytecode itself, from the bodies it checks, so the two agree by construction. The vmlibrary segment is not read at all, and the code descriptor stored in each declaration (const_body_code) is replaced rather than kept: BCalias and the unused-argument mask are attacker-controlled too, and the mask is used by ordinary conversion as well. Libraries imported with -admit or as dependencies of -norec get the same treatment, so the trusted surface is uniformly the declarations that are read. Recompiling the bytecode and comparing it against the stored one instead is not workable: stored and recompiled code legitimately differ in relocation names (user vs canonical), in alias collapsing, in the unused-argument mask, and in the inlining of const_inline_code bodies. Fixes rocq-prover#22352. Co-authored-by: Jason Gross <jason@theorem.dev> (cherry picked from commit 89832f7)
The check compared the VM bytecode stored in the .vo against bytecode recompiled from the checked body, and rejected the constant when the two differed. That cannot be made to work: stored and recompiled bytecode differ for perfectly ordinary code. The stored relocation entries name constants by their user names while a fresh compilation produces canonical ones, get_alias collapses aliases, the unused-argument mask is computed from information the checker does not have, and bodies declared inline are inlined into their callers' code. A module containing an axiom and a definition that mentions it is already enough to trip it. It is also pointless here. The checker now compiles the bytecode of every constant itself and replaces const_body_code wholesale before any constant is checked, and it never reads the vmlibrary segment of the .vo at all, so by the time check_constant_declaration ran there was no stored bytecode left to compare against: the check was comparing one recompilation against another. That doubled the bytecode compilation work, and because the two compilations happen in slightly different environments it could also reject honest code for no reason. Drop the check and the equality helpers in kernel/vmemitcodes that existed only to serve it. Nothing else used them.
archanaburra
merged commit Aug 18, 2026
1f3085b
into
v9.2+typewise-isomorphism-stable
3 of 7 checks passed
archanaburra
deleted the
backport/checker-vm-and-validation-v9.2-stable
branch
August 18, 2026 22:46
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.
Backports three rocqchk fixes from upstream onto the 9.2 stable branch, in this order:
checker: accept all 12 caml_prim constructors in VM data validation rocq-prover/rocq#22361 (fixes rocqchk -bytecode-compiler yes rejects any .vo using primitive strings (vm_caml_prim validator arity is 6, caml_prim has 12) rocq-prover/rocq#22360) —
checker/values.mldeclared only 6 constructors for thevm_caml_primenum, but there are 12. Validating a.vowhose VM data used one of the last 6 aborted with a spurious "unexpected value" failure.checker: validate every library named on the rocqchk command line rocq-prover/rocq#22363 (fixes rocqchk: which modules are validated depends on the order of the -norec arguments rocq-prover/rocq#22362) — a library named on the rocqchk command line was read without structural validation whenever it happened to be interned as a dependency of another
-norecargument. Because the first intern of a library wins and the-norecroots are interned in reverse command-line order, which files got validated depended on the order of the-norecarguments. Libraries named on the command line (minus those named with-admit) are now always validated.Do not trust the serialized VM bytecode in rocqchk rocq-prover/rocq#22353 (fixes coqchk -bytecode-compiler yes accepts a proof of False from a .vo with mismatched VM bytecode rocq-prover/rocq#22352) — with
-bytecode-compiler yes, rocqchk typechecked each constant's body but took the VM bytecode from the separately serializedvmlibrarysegment of the.vo, with nothing binding the two together. A crafted file whosevmlibrarydisagrees with itslibrarymade a VM conversion proveFalse, and rocqchk accepted it with no axioms reported. The checker now compiles the bytecode itself from the bodies it typechecks and replacesconst_body_codewholesale; thevmlibrarysegment is no longer read at all.Two regression tests come with the commits:
test-suite/misc/rocqchk_vm_bytecode.shandtest-suite/misc/norec-validation-order.sh. Both pass here, as does a fullrocqchk -bytecode-compiler yesrun overCorelib.Init.Prelude(658 constants).Note on overlap: this branch already carries 24dd96e "Verify serialized VM bytecode in coqchk" (#8), which attacks the same problem by recompiling each constant's bytecode and comparing it against the stored one. Upstream deliberately did not take that route — stored and recompiled code legitimately differ in relocation names, alias collapsing, the unused-argument mask, and the inlining of
const_inline_codebodies. With rocq-prover#22353 applied,const_body_codehas already been replaced by the recompiled code beforecheck_constant_declarationsees it, so that check degenerates into comparing a recompilation against itself: harmless and passing, but redundant work. That check is removed in this PR (0163210). Besides being dead weight — it roughly doubled the bytecode compilation work — the two recompilations it compares happen in slightly different environments, so keeping it left a spurious rejection structurally possible for no benefit. The equality helpers #8 added tokernel/vmemitcodes.ml{,i}(equal_body_code,equal_to_patch_and_patches,equal_fv_elem, andPositions.equal) had no other users and are removed with it, restoring both files to their pre-#8 contents.The same three commits have been applied directly to
master+typewise-isomorphismandv9.2+typewise-isomorphism.Opened autonomously by Claude (Opus 5) on behalf of Jason Gross (jason@theorem.dev).