{"id":"092181ac-5079-4546-8bbf-ea334b8a8eed","arxiv_id":"2501.12313","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Correctness witness format 2.0 is extended with function contracts and ACSL-style expressions \\result, \\old, and \\at(_, Pre) for encoding pre- and post-conditions.","lead":"Software verification witnesses are files that let one verification tool record and hand off proof hints to another tool. This paper extends the standard witness format so it can carry function contracts, the before-and-after specifications that modular program verifiers need.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Function-contract validity is defined only for calls reachable from main, so a witness can be valid while the encoded contract is false for other calls satisfying its requires; this undercuts the claimed exchange with modular deductive verifiers.","rationale":"The paper is transparent about the main-centric definition: Section 3 explicitly restricts validity to executions starting in main, and Section 4 states that the contracts 'do not necessarily allow for modular verification.' For SV-COMP-style single-main programs, this is a deliberate and defensible scoping choice. However, the paper's own framing goes further: the abstract and Section 1 advertise 'exchange of information with tools that require function contracts.' Deductive verifiers (Frama-C, VerCors, Dafny) interpret a requires clause as an assumption and expect ensures to hold for every call satisfying that assumption, independent of which calls are reachable from a particular main. The Section 3 semantics instead inspect only calls that actually occur in main-reachable executions. This is a real semantic mismatch, not merely a question of test coverage: a witness can be valid under Section 3 even though the encoded contract is false for a requires-satisfying call, and a tool that requires standard function contracts cannot soundly use the witness as a contract without additional, unstated assumptions. The paper's Section 4 caveat ('a validator based on a deductive verifier may validate a witness, but it cannot determine that a witness is invalid') is sound but does not rescue the exchange claim; it confirms that the format's function_contract entries are not modular contracts. This is the most load-bearing concern because it directly affects the central promised benefit rather than a surface detail of the grammar. The reader's weakest assumption identified the same root cause: the main-only validity semantics. I agree with that assessment. The concern can be settled by the proposed concrete tests: if a validator following Section 3 accepts the f(1)-only witness while Frama-C rejects the corresponding ACSL contract, then the claimed exchange with contract-based tools is not supported. The authors could address this by either extending the semantics to all entry points (or all requires-satisfying calls), or by explicitly narrowing the paper's claims to 'main-validated annotations' rather than 'function contracts.' Since such a revision is feasible and the paper does disclose the limitation, the appropriate verdict remains CONDITIONAL, matching the reader's assessment.","tokens_in":7242,"tokens_out":14569,"duration_ms":157630,"concrete_test":"Test A: construct a program with f(int x) { if (x==2) return 0; return 1; }, a witness containing requires x > 0 and ensures \\result == 1 for f, and a main that calls f(1) and asserts f(1)==1. Check that a validator implementing the Section 3 semantics accepts the witness. Then run Frama-C on f with those clauses as an ACSL contract. If Frama-C cannot prove the contract because of the x==2 case, the witness is valid while the encoded contract is not a modular function contract, confirming the semantic gap. Test B: add a function_contract for main with requires false and ensures false; under Section 3 this should be accepted, since main is never called within an execution starting in main, showing the entry-point invocation is missing from the validity definition.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Section 3 defines requires/ensures validity only 'for every function call of f in every program execution starting in an initial state, i.e., starting in main.' Thus a function_contract is a whole-program, single-entry annotation, not a function contract in the standard assume-guarantee sense. Concretely, let f be defined as returning 1 normally but returning 0 when its argument is 2, with witness entries requires x > 0 and ensures \\result == 1. If main only ever calls f(1), the contract entry is valid under Section 3, yet the contract is false for the requires-satisfying call f(2). A modular deductive verifier such as Frama-C cannot accept this pair as a valid contract. Section 4 acknowledges this ('they do not necessarily encode a modular proof'), but the abstract and Section 1 still claim the format 'allows for the exchange of information with tools that require function contracts.' Since those tools require modular contracts, the central exchange claim is not established. A related edge case: a contract on main itself is vacuously valid under Section 3, because main is never 'called' in a program execution starting in main.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes an extension to the software correctness witness format 2.0 that adds a new entry type 'function_contract' with optional 'requires' and 'ensures' clauses, and an 'acsl_expression' expression format supporting \\result, \\old, and \\at(_, Pre). The syntax and a semantics are given: a function contract is valid if its requires and ensures clauses hold at every call of the function in every program execution that starts in main. The paper claims backward compatibility with witness format 2.0 and argues that the extension enables exchange of information with tools that require function contracts, such as deductive verifiers. It also discusses validation strategies and remaining limitations involving heap, pointers, and data abstraction.","tokens_in":7426,"tokens_out":4827,"duration_ms":55448,"significance":"If the proposed extension worked as claimed, it would address a genuine gap in the witness format: correctness witnesses in version 2.0 cannot express relational pre/post-conditions of functions. The design is presented with concrete examples and a careful syntax discussion, and the paper is transparent about several limitations. However, the central claim that the format allows exchange with tools that require function contracts is currently not supported, because the validity semantics in Section 3 defines a whole-program, single-entry property rather than a modular, caller-independent function contract. This is not merely a presentation issue: it changes what a witness certifies and makes the proposed 'function contract' incompatible with standard contract semantics used by deductive verifiers. The paper's own Section 4 note that the entries 'do not necessarily encode a modular proof' partially acknowledges this, but the abstract and introduction still overstate the contribution. With a revised semantics or appropriately qualified claims, the proposal could be a useful step toward richer correctness witnesses.","major_comments":[{"comment":"The validity definition for requires and ensures clauses is not a function-contract semantics in the standard assume-guarantee sense. A requires clause is defined to be valid only if it evaluates to true at every call reachable from main, rather than being an assumption under which the ensures clause must hold. Consequently, a witness can be valid even when the encoded contract is false for a call that satisfies the precondition but is not reachable from main. Concretely, let f return 1 normally but return 0 when its argument is 2, and let the witness contain requires x > 0 and ensures \\result == 1. If main only calls f(1), the witness is valid under the paper's definition, yet the contract is false for the precondition-satisfying call f(2). A modular deductive verifier such as Frama-C would not accept this pair as a valid contract. Since the abstract and Section 1 claim that the format allows 'exchange of information with tools that require function contracts,' this semantic mismatch is load-bearing and must be addressed: either change the semantics to a caller-independent, assume-guarantee definition, or substantially weaken the exchange claim in the abstract and introduction.","section":"Section 3, 'Semantics'"},{"comment":"The validity of every entry is defined over 'every program execution starting in an initial state, i.e., starting in main,' but the paper does not say what an initial state is. This matters for programs with nondeterministic functions, uninitialized globals, input parameters, and library functions. Without a precise definition of initial state, the set of executions over which requires and ensures are quantified is not well defined, so the semantics of the new format is incomplete. The paper should either define initial state with respect to the C standard plus the SV-COMP convention for nondeterminism, or state explicitly that the semantics is only a proposal that requires such a definition.","section":"Section 3, definition of 'initial state'"},{"comment":"For a function contract with format c_expression, the paper says the ensures clause is evaluated 'after every return statement ... before returning to the caller,' but it does not specify the variable environment at that point. Since C function parameters are local variables, a parameter may have been modified in the function body, and it is unclear whether a mention of that parameter in the ensures clause denotes its value before the call, its final value in the callee frame, or something else. The paper only clarifies this for acsl_expression, where a parameter 'always evaluates to the value before the call' and \\old is available. The missing clarification affects the meaning of every c_expression ensures clause and should be resolved with an explicit rule, for example by stating that c_expression ensures clauses are evaluated in the caller's state after the return value has been computed, or by defining the callee-frame evaluation precisely.","section":"Section 3, evaluation of c_expression ensures"}],"minor_comments":[{"comment":"There is a duplicated word in 'for every function call of f in in every program execution'; it should read 'in every program execution.'","section":"Section 3, first paragraph"},{"comment":"The paper requires that clauses be 'side effect-free C expressions,' but side-effect-freeness is a semantic property, not a syntactic one. Since the format is meant to be machine-checkable, the syntax should either define a syntactic fragment that guarantees absence of side effects or specify how side effects are detected and rejected.","section":"Section 2, function_contract syntax"},{"comment":"The terms 'backwards compatible for verifiers' and 'forwards compatible for validators' are used without definition. A brief explanation of what each direction means would help readers who are not familiar with the witness-format terminology.","section":"Section 4, 'Compatibility'"},{"comment":"The table says the acsl_expression format 'is always the case when keywords like \\old and \\result are used,' but it is not stated whether the 'format' field is mandatory and what a validator should do if it is absent while the expression contains an ACSL keyword. Making the format field required and defining validation of this consistency would remove ambiguity.","section":"Table 1 and Section 2"},{"comment":"The paper states that multiple function contracts are allowed for the same function and 'all need to be valid for the witness to be valid,' but it does not say whether multiple contracts for one function are interpreted as a conjunction or as independent certificates. A one-sentence clarification would prevent misinterpretation by tool implementers.","section":"Section 2, multiple contracts"}],"recommendation":"major_revision","confidential_remarks":"The paper is a design proposal rather than a full implementation report, and the main technical contribution is the syntax and semantic proposal. I believe the central claim can be repaired within the scope of the paper, but only by either adopting a genuinely modular contract semantics or by clearly presenting the entries as whole-program annotations and removing the unfounded exchange-with-modular-verifiers claim. The single-entry semantic restriction and the missing definition of initial state are the main blockers. No concerns about novelty or citation behavior beyond what is already stated in the review."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The new thing here is real: witness format 2.0 only encodes loop and location invariants in C expressions, and this paper adds a function_contract entry type plus an acsl_expression format with \\result, \\old, and \\at(_, Pre). That lets a witness carry pre/post conditions and relational facts about pre- and post-states that were previously inexpressible. The syntax and semantics are carefully written — defaults for missing clauses, what \\old means for globals vs. parameters, where \\at(_, Pre) can appear, and the compatibility argument are all clear. The examples are helpful, and the paper is honest about several limitations in Section 4.\n\nThe soft spot is the validity semantics. Section 3 defines requires/ensures only for calls reachable from main. The stress-test example is correct: if main only calls f(1), a contract with requires x > 0 and ensures \\result == 1 is valid even though f(2) violates it. That is not a modular function contract in the assume-guarantee sense. The paper does acknowledge this in Section 4 ('they do not necessarily encode a modular proof'), but the abstract and Section 1 still claim exchange with tools that require function contracts. A deductive verifier like Frama-C cannot accept such a witness as a valid contract. So the central exchange claim is overstated relative to the semantics, and the paper needs to either generalize the semantics or reframe the claim. The vacuous-contract-on-main edge case is minor but worth a sentence.\n\nOther gaps: no artifact beyond a proposed schema, no validator integration, and compatibility is argued by example. For a design/position paper that is acceptable, but a reference implementation would strengthen the case considerably.\n\nWho this is for: researchers working on verification witness formats and cooperative verification. It is a useful, well-scoped contribution that deserves a serious referee. I would cite it if I worked in that area.","headline":"A clean, well-scoped design paper extending witness format 2.0 with function contracts; the main caveat is the single-entry validity semantics, which the paper acknowledges but the abstract overstates.","tokens_in":7992,"tokens_out":2267,"would_cite":true,"duration_ms":23343,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Correctness witnesses can now encode function contracts","keywords":["correctness witnesses","function contracts","software verification","ACSL","exchange format","program invariants","modular verification","witness validation"],"falsifier":"Take a program with two entry points, such as `main` and a second start function, where function `f` satisfies its `requires` and `ensures` clauses on all calls reachable from `main` but violates `ensures` when called from the second entry point; under the paper's semantics the witness is valid, while under a definition quantifying over all calls from all entry points it is invalid.","tokens_in":1370,"feed_emoji":"✅","tokens_out":1271,"duration_ms":45249,"temperature":0.7,"pith_summary":"This paper extends software verification witness format 2.0 so that a correctness witness can carry function-level pre- and post-conditions, not just loop and location invariants. The extension introduces a `function_contract` entry type with `requires` and `ensures` clauses, and adds an ACSL-inspired expression format that supports `\\result`, `\\old`, and `\\at(_, Pre)`. That lets a witness express relations between a function's pre-state and post-state, such as `ensures g < \\old(g)`, which were inexpressible in the previous format. It matters because when a verifier exports a witness, it can now pass modular proof information that deductive verifiers can consume, and validators can instrument code to check the contracts.","feed_headline":"Correctness witnesses can now encode function contracts","feed_subtitle":"New witness entries express pre- and post-conditions, so verifiers can share modular proofs and validate them deductively.","key_machinery":"The central machinery is a new entry type `function_contract` placed inside the `invariant_set`, together with a new expression format `acsl_expression`. The entry has optional `requires` and `ensures` clauses that default to true; the format allows `\\result` for the return value and `\\old(x)` or `\\at(x, Pre)` for the values of globals and parameters in the pre-state of the current function call. This machinery carries the argument by giving validators a source-level contract to check at function entry and exit, and by giving verifiers a way to export relational summaries that cannot be expressed as location or loop invariants.","core_discovery":"The paper claims that witness validity can be defined for function contracts by requiring each `requires` clause to hold before the first statement of the function body and each `ensures` clause to hold after every return, for every call reachable from `main`, with `\\old(x)` evaluated in the pre-state and `\\result` in the post-state. With this semantics, the extension is backward compatible for verifiers and forward compatible for validators: an empty witness remains valid, every version 2.0 witness is accepted, and validators can check the new entries or return `unknown` when a deductive validator cannot establish correctness.","pith_inferences":["If the format is adopted widely, witness producers could increasingly emit modular proof artifacts, potentially shifting cooperative verification from whole-program invariants toward compositional summaries.","The single-entry semantics means that two witnesses for the same function could disagree when the function is linked under different calling contexts; an alternative semantics quantifying over all entry points would make contracts absolute, at the cost of harder validation.","The restriction of `\\old` to variables and `\\at` to `Pre` keeps parsing simple, but a straightforward extension to arbitrary expressions would align the witness format with full ACSL and may be needed for realistic heap-aware contracts.","A testable prediction is that adding function-contract witnesses to a validator should shorten re-verification time on modular programs relative to location invariants, because the validator can check the summary instead of re-discovering it."],"forward_implications":["Any witness in version 2.0 remains valid, and the empty witness remains valid, so the change does not break existing verifiers or validators.","Validators can handle `c_expression` contracts by treating `requires` like a location invariant at function entry and `ensures` like a check after the returned expression is evaluated.","Supporting `acsl_expression` can be implemented by instrumenting ghost variables that record `\\old(x)`, `\\at(x, Pre)`, and `\\result`.","Deductive verifiers can validate witnesses with function contracts as modular inductive certificates; if they cannot establish correctness, the validator must answer `unknown` rather than reject the witness.","The format still cannot express heap and pointer invariants or data abstraction, so some correctness arguments remain inexpressible."],"supporting_citations":[{"why":"Defines the witness format 2.0 that this extension builds on and extends.","marker":"[1]"},{"why":"Provides the ACSL specification language from which the extension borrows \\result, \\old, and \\at.","marker":"[2]"},{"why":"Establishes witness validation and stepwise testification, the context in which validator compatibility matters.","marker":"[4]"},{"why":"Prior work on cooperation between automatic and interactive software verifiers that motivates exchanging information with deductive verifiers.","marker":"[8]"},{"why":"Offers a proposal for a common interchange format for system specification, which the paper points to for future data-abstraction extensions.","marker":"[13]"}],"fun_headline_variants":["Witness format gains function contracts for modular proofs","Function contracts now expressible in verifier witnesses","Witness format 2.0 extended with function contracts","Share modular proofs with function contract witnesses","Function contract witnesses enable deductive validation"],"cache_read_input_tokens":10112,"weakest_assumption_plain":"The whole validity definition is anchored to program executions that start in `main`, so a contract may be certified as valid even if it fails for a call made from another entry point, a library, or differently linked code.","fun_headline_variants_meta":{"raw":{"variants":["Witness format gains function contracts for modular proofs","Function contracts now expressible in verifier witnesses","Witness format 2.0 extended with function contracts","Share modular proofs with function contract witnesses","Function contract witnesses enable deductive validation"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001095,"raw_usage":{"total_tokens":4500,"prompt_tokens":799,"completion_tokens":3701,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":415,"completion_tokens_details":{"reasoning_tokens":3632}},"tokens_in":415,"tokens_out":3701,"duration_ms":24994,"temperature":1.0,"reasoning_tokens":3632,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T17:16:58.689222+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a program with two entry points, such as `main` and a second start function, where function `f` satisfies its `requires` and `ensures` clauses on all calls reachable from `main` but violates `ensures` when called from the second entry point; under the paper's semantics the witness is valid, while under a definition quantifying over all calls from all entry points it is invalid.","supporting_citations":[{"cited_title":"In: Proc","cited_arxiv_id":null,"evidence_quote":"Defines the witness format 2.0 that this extension builds on and extends."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Provides the ACSL specification language from which the extension borrows \\result, \\old, and \\at."},{"cited_title":"In: Proc","cited_arxiv_id":null,"evidence_quote":"Prior work on cooperation between automatic and interactive software verifiers that motivates exchanging information with deductive verifiers."},{"cited_title":"In: Proc","cited_arxiv_id":null,"evidence_quote":"Offers a proposal for a common interchange format for system specification, which the paper points to for future data-abstraction extensions."}],"review_version":1}