[cjen1-msft]

Motivation

Each safety theorem in the Lean Properties.lean files is followed by a witness lemma that repeats its variables and hypotheses under exists.
The repetition is review overhead, and nothing checks that the two copies stay in step.

Implementation summary

• Add CCF.Witnessed to the common package: witnessed% forall xs, { pre := p, post := q, witness := w } is the proposition Witnessed (forall xs, p -> q) (exists xs, p /\ w), a named And with .safety and .witness projections.
  The braces are an ordinary Witnessed.Spec structure instance; witness is optional.
  CCF.Tests.Witnessed records the produced statements and errors with #guard_msgs.

Before:

theorem rejected_gossip_stutters
    : forall (config : Model.Config),
      forall localStep : LocalStep,
      forall (source : Location) (txid : TxID),
        ((Model.protocol config).ValidStep localStep
          /\ localStep.action = .receiveGossip source txid .rejected)
        -> localStep.after = localStep.before
            /\ .rejected "quote-or-certificate" ∈ localStep.effects.notifications := by
  exact Proofs.Local.rejected_gossip_stutters

theorem rejected_gossip_stutters_witness
    : forall (config : ValidConfig),
        exists localStep : LocalStep,
        exists (source : Location) (txid : TxID),
          (Model.protocol config).ValidStep localStep
          /\ localStep.action = .receiveGossip source txid .rejected := by
  exact Proofs.Witnesses.rejected_gossip_stutters_witness

After:

theorem rejected_gossip_stutters
    : forall (config : Model.Config),
        config.Valid
        -> witnessed% forall (localStep : LocalStep) (source : Location) (txid : TxID),
                        {
                          pre :=
                            (Model.protocol config).ValidStep localStep
                            /\ localStep.action = .receiveGossip source txid .rejected
                          post :=
                            localStep.after = localStep.before
                            /\ .rejected "quote-or-certificate"
                                ∈ localStep.effects.notifications
                        } := by
  exact Proofs.Claims.rejected_gossip_stutters

A conjunct that only the witness satisfies goes in an optional witness := ... field, for example witness := rs ≠ [] in kv.

• Convert 54 claim/witness pairs: 4 in consensus, 6 in disaster recovery, 28 in kv and 16 in consistency.
  Each Properties.lean proof is a one-line exact Proofs.Claims.<name>; the glue that assembles the existing safety and witness proofs lives in a new Proofs/Claims.lean per package.
• Consistency claims bind the pair components that were previously destructured inside the conclusion as separate variables.
• Pairs that do not fit stay written out: the deadlock_free theorems, full_gossip_preserves_commit (its witness assumes more than its claim), all_received_is_first_sent, and the kv point-read and publication claims, whose witnesses fix type parameters.
• Remove CCF.Nonvacuous, and update lean/AGENT.md and the package READMEs.

Safety and compatibility

No runtime change.
The converted disaster-recovery and consensus safety theorems now assume config.Valid and config.Nonempty respectively, which their witnesses already required; the unconditional theorems under Proofs/ are unchanged.
Some kv witnesses now quantify over variables of their claim that they previously omitted.
lake check runs only in CI and has not been run on this change.

[Copilot]

🔵 Needs a closer look

The new Lean elaborator rewrites 53 safety/witness statements, but lake check has not been run, so human review must confirm elaboration, independent kernel checks, and import checks across all five affected packages.

No open issues 🎉

What changed in this PR

This PR adds witnessed% to CCF’s shared Lean library, allowing safety claims and their existential witnesses to share variables and premises.
It reduces duplicated statements across the formal models without changing runtime behavior.

Changes:

• Add CCF.Witnessed, .safety and .witness projections, and elaboration checks.
• Convert 53 claim/witness pairs across consensus, disaster recovery, consistency, and KV, with proof assembly in new Proofs/Claims.lean modules.
• Update recovery callers and documentation, including the new config.Valid assumption on converted recovery claims; retain separate witnesses where needed.

Custom instructions used

• CCF repository review guidance supplied with the request.
• lean/AGENT.md — supplied excerpt covering witnessed claims and proof organization.

File	Description
lean/​kv/​README.md	Document combined claims and standalone witnesses.
lean/​kv/​Kv/​Properties.lean	Convert 28 KV claims to witnessed statements.
lean/​kv/​Kv/​Proofs/​Claims.lean	Assemble KV safety proofs and witnesses.
lean/​kv/​Kv.lean	Export the new claims module.
lean/​disaster-recovery/​README.md	Explain witnessed claims and configuration validity assumptions.
lean/​disaster-recovery/​DisasterRecovery/​Tests/​Witnesses.lean	Adapt witness checks to the new projections.
lean/​disaster-recovery/​DisasterRecovery/​Tests/​Trace.lean	Supply configuration validity when applying safety projections.
lean/​disaster-recovery/​DisasterRecovery/​Properties.lean	Convert six recovery claims to witnessed statements.
lean/​disaster-recovery/​DisasterRecovery/​Proofs/​Claims.lean	Combine recovery proofs with valid-configuration witnesses.
lean/​disaster-recovery/​DisasterRecovery.lean	Export the new claims module.
lean/​consistency/​consistency/​Properties.lean	Convert 16 consistency claims and explicitly bind tuple components.
lean/​consistency/​consistency/​Proofs/​Claims.lean	Assemble consistency claims from existing proofs and witnesses.
lean/​consensus/​Consensus/​Properties.lean	Convert three consensus claims, retaining witness-only conditions.
lean/​consensus/​Consensus/​Proofs/​Claims.lean	Assemble consensus safety proofs and witnesses.
lean/​common/​README.md	Explain notation, quantifier scope, and projections.
lean/​common/​CCF/​Witnessed.lean	Define witnessed propositions, specifications, and elaboration.
lean/​common/​CCF/​Tests/​Witnessed.lean	Check generated statements and unsupported-input diagnostics.
lean/​common/​CCF.lean	Export witnessed definitions and import their checks.
lean/​AGENT.md	Update contributor guidance for witnessed safety claims.

_{Review effort: Balanced}

[Copilot]

🟡 Changes recommended

The witness description misleadingly suggests two distinct primaries, although both participant positions use the same primary and the safety projection proves they must be equal.

1 open issue

• Describe one primary serving both participant positions · New

_{Review effort: Balanced}