SwayamInSync · Oct 14, 2026 · Oct 14, 2026 · Oct 14, 2026 · Oct 14, 2026 · Oct 14, 2026
diff --git a/clang/test/Verify/suite/Inputs/run_backend_fidelity.py b/clang/test/Verify/suite/Inputs/run_backend_fidelity.py
@@ -147,13 +147,17 @@ def function_records(records):
     return selected
 
 
-def check_matrix(records, backend):
+def check_matrix(records, backend, replay=False):
+    # Replay proves each module alone, without the verdicts it rests on.
+    proved = "proved-obligations" if replay else "verified"
     selected = function_records(records)
     for name, expected in EXPECTED_STATUS.items():
+        if expected == "verified":
+            expected = proved
         record = selected[name]
         actual = record.get("status")
         if backend in {"cvc5", "portfolio"} and name in CONSERVATIVE_CVC5:
-            if actual == "verified":
+            if actual == proved:
                 continue
             if actual != "unresolved" or record.get("reason") != "solver.unknown":
                 fail(
@@ -365,7 +369,7 @@ def check_archive_matrix(cpp_verify, source, work, source_records):
         replayed = parse_json_lines(
             run(replay_command(cpp_verify, backend, canonical), {1})
         )
-        selected = check_matrix(replayed, backend)
+        selected = check_matrix(replayed, backend, replay=True)
         for name in INVALID_FUNCTIONS:
             if diagnostic_identity(selected[name]) != diagnostic_identity(
                 function_records(source_records[backend])[name]
@@ -383,7 +387,7 @@ def check_archive_matrix(cpp_verify, source, work, source_records):
     replayed_bmc = parse_json_lines(
         run(replay_command(cpp_verify, "bmc", bmc_archive), {1})
     )
-    selected_bmc = check_matrix(replayed_bmc, "bmc")
+    selected_bmc = check_matrix(replayed_bmc, "bmc", replay=True)
     source_bmc = function_records(source_records["bmc"])
     for name in INVALID_FUNCTIONS:
         if diagnostic_identity(selected_bmc[name]) != diagnostic_identity(

diff --git a/clang/test/Verify/suite/backend_execution.test b/clang/test/Verify/suite/backend_execution.test
@@ -118,8 +118,8 @@
 # LEAN-JOBS: error: --jobs and --proof-cache are not supported by the Lean backend
 # LOWER-CACHE: error: --proof-cache cannot be combined with --lower-only
 
-# REPLAY: Verified: cached_identity [backend=z3] [cache=[[RN:[1-9][0-9]*]]/[[RN]]]
-# REPLAY: Verified: cached_offset [backend=z3] [cache=[[RM:[1-9][0-9]*]]/[[RM]]]
+# REPLAY: Proved obligations: cached_identity (dependencies not checked in replay) [backend=z3] [cache=[[RN:[1-9][0-9]*]]/[[RN]]]
+# REPLAY: Proved obligations: cached_offset (dependencies not checked in replay) [backend=z3] [cache=[[RM:[1-9][0-9]*]]/[[RM]]]
 
 # FAILED-FIRST: error: verification failed: parallel_failure
 # FAILED-FIRST-SAME: [cache=0/4]

diff --git a/clang/test/Verify/suite/collections.cpp b/clang/test/Verify/suite/collections.cpp
@@ -115,8 +115,8 @@ int count_equal(const int *a, int n, int x)
 }
 // CHECK-DAG: Verified: count_equal
 
-// REPLAY-DAG: Verified: sets
-// REPLAY-DAG: Verified: count_equal
+// REPLAY-DAG: Proved obligations: sets (dependencies not checked in replay)
+// REPLAY-DAG: Proved obligations: count_equal (dependencies not checked in replay)
 // REPLAY-DAG: error: verification failed: map_wrong
 
 // VC-LABEL: vc sets

diff --git a/clang/test/Verify/suite/heap_reading_spec.cpp b/clang/test/Verify/suite/heap_reading_spec.cpp
@@ -44,7 +44,7 @@ int total(const int *p, int n)
 }
 // LOOP-DAG: Verified: total
 // CVC5-DAG: {{Verified|Unresolved}}: total
-// REPLAY-DAG: Verified: total
+// REPLAY-DAG: Proved obligations: total (dependencies not checked in replay)
 // VC: features {{.*}}heap-functions
 
 int skip_first(const int *p, int n)
@@ -79,7 +79,7 @@ void clear_first(int *p)
   p[0] = 0;
 }
 // CHECK-DAG: Verified: clear_first
-// REPLAY-DAG: Verified: clear_first
+// REPLAY-DAG: Proved obligations: clear_first (dependencies not checked in replay)
 
 void clear_first_unchanged(int *p)
   cppverify::pre(valid(p, 2))

diff --git a/clang/test/Verify/suite/obligation_archive.test b/clang/test/Verify/suite/obligation_archive.test
@@ -91,19 +91,19 @@
 # RUN: not %cpp-verify --obligation-in=%t.bad-binder-sort 2>&1 | FileCheck %s --check-prefix=BAD-BINDER-SORT
 # RUN: %cpp-verify --lower-only --dump-ir=3 %S/heap_memcpy_pass.cpp -- 2>&1 | grep -B1 '__quant_.* : int' | FileCheck %s --check-prefix=QUANTIFIED-INDEX
 
-# REPLAY: Verified: canonical_obligations [backend=z3] [semantic-hash=sha256:{{[0-9a-f]+}}]
+# REPLAY: Proved obligations: canonical_obligations (dependencies not checked in replay) [backend=z3] [semantic-hash=sha256:{{[0-9a-f]+}}]
 # LOWER: vc canonical_obligations
 # LOWER: schema cppverify.obligation/2
 # LOWER: (let
 # LOWER: Lowered: canonical_obligations [backend=z3] [semantic-hash=sha256:{{[0-9a-f]+}}]
 # LEAN: Exported: lean obligation: canonical_obligations [backend=lean]
 # LEAN-FILE: theorem cppverify_canonical_obligations_
-# MULTI-COUNT-2: Verified: canonical_obligations
+# MULTI-COUNT-2: Proved obligations: canonical_obligations (dependencies not checked in replay)
 # BAD-MAGIC: error: invalid obligation archive: invalid obligation archive magic
 # TRUNCATED: error: invalid obligation archive: truncated obligation archive
 # VERSION: error: invalid obligation archive: unsupported obligation archive version
 # SCHEMA-V1: error: invalid obligation archive: invalid obligation kind in obligation archive
-# SCHEMA-V1-KINDS: Verified: canonical_obligations [backend=z3]
+# SCHEMA-V1-KINDS: Proved obligations: canonical_obligations (dependencies not checked in replay) [backend=z3]
 # KIND: error: invalid obligation archive: invalid expression kind in obligation archive
 # FEATURES: error: invalid obligation archive: obligation archive feature declaration does not match contents
 # DUPLICATE-ID: error: invalid obligation archive: obligation module has an empty or duplicate obligation identity
@@ -118,15 +118,15 @@
 # SYMBOL-SORT: error: invalid obligation archive: logical variable has inconsistent sorts:
 # TRACE-SORT: error: invalid obligation archive: obligation module has invalid diagnostic trace value
 # INVALID-UTF8: "function":"{{.*}}anonical_obligations"
-# INVALID-UTF8-SAME: "status":"verified"
+# INVALID-UTF8-SAME: "status":"proved-obligations"
 # DUPLICATE-FUNCTION: error: invalid obligation archive: duplicate logical function in obligation archive
 # BAD-BINDER-SORT: error: invalid obligation archive: quantifier binder occurrence is not a mathematical integer
 # QUANTIFIED-INDEX: * : int
 # QUANTIFIED-INDEX-NEXT: __quant_{{[0-9]+}}_{{.*}} : int
 # BMC: error: BMC cannot replay an untransformed backend-neutral archive
-# BMC-REPLAY-DAG: Verified: zero_iterations [backend=bmc, bound=0]
+# BMC-REPLAY-DAG: Proved obligations: zero_iterations (dependencies not checked in replay) [backend=bmc, bound=0]
 # BMC-REPLAY-DAG: cov_loop_unroll_zero.cpp:22:3: BoundedSafe: one_step_may_run (unwinding bound 0 is insufficient for a complete proof) [backend=bmc, bound=0]
 # BMC-BOUND: error: requested BMC bound 1 does not match archived bound 0
 # BMC-LOWER: transform bmc-unroll 0
-# BMC-DECREASES: Verified: dec.decreases [backend=bmc, bound=2]
+# BMC-DECREASES: Proved obligations: dec.decreases (dependencies not checked in replay) [backend=bmc, bound=2]
 # FAIL: obligation_archive_fail.cpp:2:37: error: verification failed: archived_failure
diff --git a/clang/test/Verify/suite/replay_dependencies.cpp b/clang/test/Verify/suite/replay_dependencies.cpp
@@ -0,0 +1,66 @@
+// RUN: rm -f %t.cpv
+// RUN: not %cpp-verify --obligation-out=%t.cpv %s -- 2>&1 | FileCheck %s --check-prefix=SOURCE
+// RUN: not %cpp-verify --obligation-in=%t.cpv 2>&1 \
+// RUN:   | FileCheck %s --check-prefix=REPLAY --implicit-check-not=Verified
+// RUN: not %cpp-verify --obligation-in=%t.cpv --diagnostics-format=json 2>&1 \
+// RUN:   | FileCheck %s --check-prefix=JSON --implicit-check-not='"status":"verified"'
+//
+// Replay proves each archived module alone. A source verdict also rests on
+// callee contracts, trust, termination, and vacuity, which replay does not
+// check, so a replayed proof is never reported as verified.
+
+// caller's proof rests on the contract of bad_callee, which is false.
+int bad_callee(int x)
+  cppverify::post(cppverify::result > 0)
+{
+  return x;
+}
+
+int caller(int x)
+  cppverify::post(cppverify::result > 0)
+{
+  return bad_callee(x);
+}
+
+int vac(int x)
+  cppverify::pre(x > 0 && x < 0)
+  cppverify::post(cppverify::result == 42)
+{
+  return 0;
+}
+
+[[cppverify::trusted]] int tr(int x)
+  cppverify::post(cppverify::result > 100);
+
+int uses_tr(int x)
+  cppverify::post(cppverify::result > 100)
+{
+  return tr(x);
+}
+
+int loop_star(int n)
+  cppverify::post(cppverify::result == 7)
+{
+  while (true)
+    cppverify::invariant(true)
+    cppverify::decreases(*)
+  {
+    if (n == 3)
+      return 7;
+  }
+}
+
+// SOURCE-DAG: error: verification failed: bad_callee
+// SOURCE-DAG: Unresolved: caller [backend=z3] [reason=callee.contract]
+// SOURCE-DAG: Verified: vac [backend=z3] [vacuous]
+// SOURCE-DAG: Verified: uses_tr [backend=z3] [trusts=tr]
+// SOURCE-DAG: Verified: loop_star [backend=z3] [partial]
+
+// REPLAY-DAG: error: verification failed: bad_callee
+// REPLAY-DAG: Proved obligations: caller (dependencies not checked in replay) [backend=z3]
+// REPLAY-DAG: Proved obligations: vac (dependencies not checked in replay) [backend=z3]
+// REPLAY-DAG: Proved obligations: uses_tr (dependencies not checked in replay) [backend=z3]
+// REPLAY-DAG: Proved obligations: loop_star (dependencies not checked in replay) [backend=z3]
+
+// JSON-DAG: "function":"bad_callee"{{.*}}"status":"failed"
+// JSON-DAG: "function":"caller","message":"dependencies not checked in replay"{{.*}}"status":"proved-obligations"
diff --git a/clang/test/Verify/suite/sequences.cpp b/clang/test/Verify/suite/sequences.cpp
@@ -178,9 +178,9 @@ void ghost_loop_wrong(int n)
 }
 // CHECK-DAG: error: verification failed: ghost_loop_wrong [{{.*}}::assertion@[[@LINE-2]]:3] (counterexample: {{.*}}s [ssa=s_2] [type=seq] = [{{-?[0-9]+}}]{{.*}}) [backend=z3] [reason=counterexample]
 
-// REPLAY-DAG: Verified: basics
-// REPLAY-DAG: Verified: reverse_index
-// REPLAY-DAG: Verified: count_positive
+// REPLAY-DAG: Proved obligations: basics (dependencies not checked in replay)
+// REPLAY-DAG: Proved obligations: reverse_index (dependencies not checked in replay)
+// REPLAY-DAG: Proved obligations: count_positive (dependencies not checked in replay)
 // REPLAY-DAG: error: verification failed: elements_differ
 // REPLAY-DAG: error: verification failed: ghost_loop_wrong
 

diff --git a/clang/test/Verify/suite/solver_portfolio.cpp b/clang/test/Verify/suite/solver_portfolio.cpp
@@ -116,9 +116,9 @@ int invalid_spec_arithmetic()
 // LOWER-DAG: Lowered: unsafe_add
 // LOWER-NOT: Verified:
 
-// REPLAY-DAG: Verified: valid_spec_arithmetic [backend=portfolio]
-// REPLAY-DAG: Verified: valid_zero_arity_spec [backend=portfolio]
-// REPLAY-DAG: Verified: write_pointer [backend=portfolio]
+// REPLAY-DAG: Proved obligations: valid_spec_arithmetic (dependencies not checked in replay) [backend=portfolio]
+// REPLAY-DAG: Proved obligations: valid_zero_arity_spec (dependencies not checked in replay) [backend=portfolio]
+// REPLAY-DAG: Proved obligations: write_pointer (dependencies not checked in replay) [backend=portfolio]
 // REPLAY-DAG: error: verification failed: unsafe_add
 // REPLAY-DAG: error: verification failed: invalid_unsigned
 // REPLAY-DAG: error: verification failed: invalid_spec_arithmetic
diff --git a/clang/test/Verify/suite/solver_race.cpp b/clang/test/Verify/suite/solver_race.cpp
@@ -25,7 +25,7 @@ int add_one(int x)
 // CHECK-DAG: Verified: add_one [backend={{z3|cvc5|z3\+cvc5}}]
 // LOWER-DAG: Lowered: add_one
 // LOWER-NOT: Verified:
-// REPLAY-DAG: Verified: {{.*}}add_one{{.*}} [backend={{z3|cvc5|z3\+cvc5}}]
+// REPLAY-DAG: Proved obligations: {{.*}}add_one{{.*}} (dependencies not checked in replay) [backend={{z3|cvc5|z3\+cvc5}}]
 
 int wrong_bound(int x)
   cppverify::pre(x >= 0 && x < 10)

diff --git a/clang/test/Verify/suite/spec_reads.cpp b/clang/test/Verify/suite/spec_reads.cpp
@@ -33,7 +33,7 @@ void write_after(int *p, int n)
 }
 // CHECK-DAG: Verified: write_after
 // The frames are ordinary assumptions of the archived query.
-// REPLAY-DAG: Verified: write_after
+// REPLAY-DAG: Proved obligations: write_after (dependencies not checked in replay)
 
 // Each store is framed separately, through both branches.
 void write_around(int *p, int n, bool front)

diff --git a/clang/tools/cpp-verify/Main.cpp b/clang/tools/cpp-verify/Main.cpp
@@ -361,12 +361,17 @@ class VerifyAction : public ASTFrontendAction {
   }
 };
 
+// Replay proves each module alone: the contracts and spec facts its proof
+// rests on, its qualifiers, and its vacuity belong to the source run.
+static constexpr const char ReplayProofNote[] =
+    "dependencies not checked in replay";
+
 static llvm::StringRef replayStatusCode(verify::VerifyStatus Status) {
   switch (Status) {
   case verify::VerifyStatus::Lowered:
     return "lowered";
   case verify::VerifyStatus::Verified:
-    return "verified";
+    return "proved-obligations";
   case verify::VerifyStatus::Failed:
     return "failed";
   case verify::VerifyStatus::Unresolved:
@@ -414,7 +419,9 @@ static void printReplayJSON(const verify::ObligationModule &Module,
                            ? "error"
                            : "note";
   Record["function"] = jsonText(Module.FunctionName);
-  Record["message"] = jsonText(Result.Message);
+  Record["message"] = Result.Status == verify::VerifyStatus::Verified
+                          ? ReplayProofNote
+                          : jsonText(Result.Message);
   Record["semantic_hash"] = ("sha256:" + SemanticHash).str();
   if (!Result.BackendName.empty())
     Record["backend"] = Result.BackendName;
@@ -691,7 +698,8 @@ static int replayObligationArchive() {
       llvm::outs() << "Lowered: " << Module.FunctionName << Suffix << "\n";
       break;
     case verify::VerifyStatus::Verified:
-      llvm::outs() << "Verified: " << Module.FunctionName << Suffix << "\n";
+      llvm::outs() << "Proved obligations: " << Module.FunctionName << " ("
+                   << ReplayProofNote << ")" << Suffix << "\n";
       break;
     case verify::VerifyStatus::Exported:
       llvm::outs() << "Exported: lean obligation: " << Module.FunctionName

diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md
@@ -578,6 +578,13 @@ reach any adapter. Semantically equivalent records that differ only by
 supported constant structure or unreachable logical declarations therefore
 converge to the same backend module and semantic identity.
 
+Replay settles each module alone. What a source verdict also rests on (callee
+and trusted contracts, spec facts, partiality) and the vacuity checks are not
+archived, so a module whose obligations all hold reports `Proved obligations:
+f (dependencies not checked in replay)` (JSON status `proved-obligations`),
+never `Verified`. A counterexample is still a failure: postconditions are not
+archived either, so replay certifies it by the definitions alone.
+
 BMC-produced modules retain the unroll bound as semantic transform provenance.
 Replay aggregates those modules with BMC unwinding semantics even when Z3 is
 the selected solver, so an exhausted frontier remains `BoundedSafe(N)` rather

diff --git a/docs/DESIGN.md b/docs/DESIGN.md
@@ -1645,7 +1645,10 @@ diagnostic identities advanced it to v3, and excluding diagnostic kinds
 advances it to v4.
 `--obligation-in=FILE` validates and replays the records through Z3, cvc5,
 strict Z3+cvc5 portfolio, lower-only/Layer 3-4 dumps, or Lean scratch export
-without reparsing C++.
+without reparsing C++. Each module is replayed alone, without the contracts,
+spec facts, partiality, and vacuity checks its source verdict rests on, so a
+module whose obligations hold reports `Proved obligations` (JSON
+`proved-obligations`), never `Verified`.
 BMC-produced records carry their unroll bound in semantics and replay through
 the BMC result aggregator; untransformed records cannot acquire BMC semantics
 after this boundary. Lean scratch replay of bounded records is rejected.

diff --git a/website/source/book/part-ii/ch15-toolchain-and-flags.rst b/website/source/book/part-ii/ch15-toolchain-and-flags.rst
@@ -90,7 +90,8 @@ Other flags
   obligation records with semantic hashes
 - ``cpp-verify --obligation-in=FILE`` — validate and replay records through Z3,
   lower-only dumps, or Lean scratch export without reparsing C++; records made
-  by BMC retain and enforce their archived unroll bound
+  by BMC retain and enforce their archived unroll bound. A proof is reported
+  as ``Proved obligations``, since what a verdict rests on is not archived
 
 IR layers
 ---------

diff --git a/website/source/book/part-ii/ch17-backends-modular-calls.rst b/website/source/book/part-ii/ch17-backends-modular-calls.rst
@@ -209,6 +209,14 @@ ill-scoped variables, and contradictory complete/ordered goals fail closed.
 Different records may request different reveal fuel for one logical function,
 but its shared parameter/result signature must remain compatible.
 
+Replay proves each module's obligations alone. What a source verdict also
+rests on is not archived: the callee and trusted contracts and spec facts it
+uses, ``[partial]``, and the vacuity checks. Where the source run reports
+``Verified``, replay therefore reports ``Proved obligations: f (dependencies
+not checked in replay)``, with JSON status ``proved-obligations``. A
+counterexample is checked against the definitions alone and is still a
+failure.
+
 Source-built and replayed records pass through the same conservative
 canonicalizer before hashing and dispatch. It folds only trivial Boolean
 structure and reflexive equality/inequality, removes transitively unreachable

diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst
@@ -200,9 +200,11 @@ Backends
        produced after BMC unrolling retain their bound and replay with BMC
        unwinding semantics; applying BMC to an untransformed archive is
        rejected because unrolling must run before obligation lowering.
-       Each module is replayed on its own: a module that relies on a spec's
-       termination, ``cppverify::reads``, or ``cppverify::post`` is not demoted when that spec's own
-       module fails, which the replay reports separately.
+       Each module is replayed on its own, without the callee and trusted
+       contracts, spec facts, partiality, and vacuity its source verdict
+       rests on: a module whose obligations all hold reports ``Proved
+       obligations: f (dependencies not checked in replay)`` (JSON
+       ``"status":"proved-obligations"``), never ``Verified``.
 
 ``--lower-only`` is deliberately different from compiler ``-fno-verify``.
 ``-fno-verify`` stops after Clang syntax and contract semantic checks;