Summary
A user function name that collides with a name the proof contract declares — or with one of the eight helpers the emitter writes into every preamble — produces a .v that coqc rejects. sanitize_rocq_identifier denies only the Coq prelude, so the mechanism exists but its deny-list is missing the two name sets the emitter itself controls.
No test can catch this today: the coqc gate only compiles fixtures, and no fixture is named after a contract constructor.
Found while auditing coqc-gate coverage for #401.
Reproduction A — a contract constructor
fn BI_call(x: i32) -> i32 { return x; }
plus any caller, compiled with infc -v and then run through coqc against the vendored stub:
Error: Illegal application (Non-functional construction):
The expression "BI_call" of type "module_func"
cannot be applied to the term "0%N" : "N"
Reproduction B — a preamble helper
A file Mi.inf containing fn Mi(x: i32) -> i32 emits Definition Mi three times — once as the preamble import helper, once as the function, once in the module record:
File ".../Mi.v", line 27, characters 11-13:
Error: Mi already exists.
The eight preamble helpers are Vi32, Vi64, Mt, Mm, Mg, Mi, Me, Ma.
Cause
REJECTED_ROCQ_STDLIB_NAMES in core/wasm-to-v/src/rocq_names.rs covers Coq prelude names only. The mechanism works where it is applied — fn nat correctly sanitizes to nat_ — so this is a gap in the list, not in the design.
Two name sets are missing:
- every name the vendored stub declares (~160, and the same set the real library declares);
- the eight preamble helpers the emitter writes itself.
Suggested fix
Extend the deny-list with both sets, so a colliding name is sanitized the way nat already is. #401 added a stub_declarations() parser to tests/src/rocq_typecheck.rs that enumerates set 1 mechanically; a test could hold the deny-list to it, so the two cannot drift as the contract grows.
Reachability
Reachable from ordinary Inference source, with no foreign .wasm involved — the user only has to name a function unluckily. The failure surfaces at coqc or at the prover rather than at infc, which is the wrong end of the pipeline for a name the compiler chose.
Summary
A user function name that collides with a name the proof contract declares — or with one of the eight helpers the emitter writes into every preamble — produces a
.vthatcoqcrejects.sanitize_rocq_identifierdenies only the Coq prelude, so the mechanism exists but its deny-list is missing the two name sets the emitter itself controls.No test can catch this today: the
coqcgate only compiles fixtures, and no fixture is named after a contract constructor.Found while auditing
coqc-gate coverage for #401.Reproduction A — a contract constructor
plus any caller, compiled with
infc -vand then run throughcoqcagainst the vendored stub:Reproduction B — a preamble helper
A file
Mi.infcontainingfn Mi(x: i32) -> i32emitsDefinition Mithree times — once as the preamble import helper, once as the function, once in the module record:The eight preamble helpers are
Vi32,Vi64,Mt,Mm,Mg,Mi,Me,Ma.Cause
REJECTED_ROCQ_STDLIB_NAMESincore/wasm-to-v/src/rocq_names.rscovers Coq prelude names only. The mechanism works where it is applied —fn natcorrectly sanitizes tonat_— so this is a gap in the list, not in the design.Two name sets are missing:
Suggested fix
Extend the deny-list with both sets, so a colliding name is sanitized the way
natalready is. #401 added astub_declarations()parser totests/src/rocq_typecheck.rsthat enumerates set 1 mechanically; a test could hold the deny-list to it, so the two cannot drift as the contract grows.Reachability
Reachable from ordinary Inference source, with no foreign
.wasminvolved — the user only has to name a function unluckily. The failure surfaces atcoqcor at the prover rather than atinfc, which is the wrong end of the pipeline for a name the compiler chose.