Formal methods review: properties soundness audit

properties_review.md

A) Properties Verdict: Unsound.
The \section{Properties} claims do not align with the Lean formalization on key assumptions (notably type preservation and progress), and the Lean liveness theorem (eventualDelivery) is not semantically tied to actual transition steps. There are also logic-mode inconsistencies (constructive vs classical) and rule-faithfulness mismatches (notably payload wrapping/mediation).

B) Properties Findings (severity-ordered)

Extracted claims and Lean mapping:

1. Well-typedness implies “no orphaned messages” and spawn pairing (main.tex:2043, main.tex:2048) → spawnPairing exists (formalization/MailboxActors/MailboxActors/System/WellTyped.lean:59), but no Lean theorem for no-orphaned-messages.
2. Proposition Type Preservation (main.tex:2051) → typePreservation (formalization/MailboxActors/MailboxActors/Properties/TypePreservation.lean:18).
3. Proposition Progress (main.tex:2079) → progress (formalization/MailboxActors/MailboxActors/Properties/Progress.lean:211) + hasProductiveWork (formalization/MailboxActors/MailboxActors/Properties/Progress.lean:31).
4. Proposition Effect Determinism (main.tex:2108) → effectDeterminism (formalization/MailboxActors/MailboxActors/Properties/Determinism.lean:39).
5. Proposition Mailbox Isolation (main.tex:2124) → MailboxIsolation (formalization/MailboxActors/MailboxActors/System/WellTyped.lean:48) + preservation theorem mailboxIsolation (formalization/MailboxActors/MailboxActors/Properties/Isolation.lean:20).
6. Lemma Mailbox Persistence (main.tex:2140) → mailboxPersistence (formalization/MailboxActors/MailboxActors/Properties/Isolation.lean:113) and existence form mailboxSurvivesClean (formalization/MailboxActors/MailboxActors/Properties/Isolation.lean:122).
7. Corollary Trace Invariants (main.tex:2161) → invariants_trace (formalization/MailboxActors/MailboxActors/Properties/Delivery.lean:47).
8. Proposition Eventual Delivery (main.tex:2171) → eventualDelivery (formalization/MailboxActors/MailboxActors/Properties/Delivery.lean:155) with StronglyFair (formalization/MailboxActors/MailboxActors/Properties/Delivery.lean:30) and EventuallyAccepts (formalization/MailboxActors/MailboxActors/Properties/Delivery.lean:67).
9. Remark Classical Reasoning (main.tex:2208) → by_contra in eventual delivery (formalization/MailboxActors/MailboxActors/Properties/Delivery.lean:176).
10. Remarks on causal delivery/invariant (main.tex:2226, main.tex:2239) → causalAction_preserves_invariant (formalization/MailboxActors/MailboxActors/Examples/CausalMailbox.lean:235) and causal_invariant_preserved (formalization/MailboxActors/MailboxActors/Examples/CausalTrace.lean:44).

Findings:

1. Critical: Eventual-delivery proof is disconnected from real transitions.
   Why: eventualDelivery defines predicate P as a state relation, but does not require OpStep.enqueue (or any OpStep) for P; fairness is over arbitrary predicates, so liveness can be forced without semantic transition linkage. IsExecution, WellTypedState, MailboxIsolation, and initial membership are introduced but unused in the theorem body.
   Refs: formalization/MailboxActors/MailboxActors/Properties/Delivery.lean:30, formalization/MailboxActors/MailboxActors/Properties/Delivery.lean:155, formalization/MailboxActors/MailboxActors/Properties/Delivery.lean:164, formalization/MailboxActors/MailboxActors/Properties/Delivery.lean:180, formalization/MailboxActors/MailboxActors/Properties/Delivery.lean:190, main.tex:2173.
   Classification: mismatch.

2. Critical: Progress statement in paper and Lean theorem are materially different.
   Why: paper claims progress from “messages nonempty OR busy OR terminated”; Lean requires stricter hasProductiveWork (message must target ready/accepting mailbox) and proves existence of a non-node step. Also, paper semantics has always-available S-Node, making paper statement weak/vacuous as written.
   Refs: main.tex:2080, main.tex:851, formalization/MailboxActors/MailboxActors/Properties/Progress.lean:31, formalization/MailboxActors/MailboxActors/Properties/Progress.lean:211.
   Classification: mismatch.

3. High: Type-preservation assumptions are stronger in Lean than in paper.
   Why: paper proposition assumes only well-typedness + one step; Lean theorem additionally requires pre-state mailbox isolation. This is a hidden strengthening relative to the published claim.
   Refs: main.tex:2052, formalization/MailboxActors/MailboxActors/Properties/TypePreservation.lean:18.
   Classification: mismatch.

4. High: “No orphaned messages follows from well-typedness” is not encoded in Lean well-typedness.
   Why: Lean messages_typed is conditional on target existence; it does not assert target existence for every in-transit message. Paper explicitly claims this structural consequence.
   Refs: main.tex:2044, formalization/MailboxActors/MailboxActors/System/WellTyped.lean:20.
   Classification: mismatch.

5. High: Payload/mediation rule faithfulness mismatch (Append vs unwrapped payload).
   Why: paper M-Send/E-Send wrap payload with append; Lean send rules append raw dependent pair payload and do not use Append in operational rules, changing the payload discipline stated in the paper.
   Refs: main.tex:1082, main.tex:1113, main.tex:1496, formalization/MailboxActors/MailboxActors/Semantics/Judgment.lean:203, formalization/MailboxActors/MailboxActors/Semantics/Judgment.lean:92, formalization/MailboxActors/MailboxActors/Engine/Message.lean:22.
   Classification: mismatch.

6. High: Logic-mode claim (“all other propositions constructive”) is false.
   Why: non-liveness properties use classical reasoning (Classical.em, by_contra) outside eventual delivery.
   Refs: main.tex:2223, formalization/MailboxActors/MailboxActors/Properties/Determinism.lean:49, formalization/MailboxActors/MailboxActors/Properties/TypePreservation.lean:70, formalization/MailboxActors/MailboxActors/Properties/Progress.lean:61.
   Classification: mismatch.

7. Medium: Mailbox-isolation proposition is stated as an absolute property in paper but formalized as inductive preservation under assumptions.
   Why: Lean theorem requires both WellTypedState and prior MailboxIsolation; this is not the same shape as the paper proposition text.
   Refs: main.tex:2125, formalization/MailboxActors/MailboxActors/Properties/Isolation.lean:20.
   Classification: mismatch.

8. Medium: Effect-rule semantics differ (partial-premise rules in paper vs totalized fallback in Lean).
   Why: Lean E-Send and E-Spawn include fallback branches (κ no-op / nextId += 2) when premises fail; paper presents premise-guarded rules without these fallback outcomes.
   Refs: main.tex:1468, main.tex:1575, formalization/MailboxActors/MailboxActors/Semantics/Judgment.lean:82, formalization/MailboxActors/MailboxActors/Semantics/Judgment.lean:118.
   Classification: mismatch.

C) Whole-Paper Findings (severity-ordered)

1. Critical: Mechanization completeness claim is not currently true (build failure in core file).
   Why: lake build fails in System/State.lean, so “machine-checked proofs / complete mechanization” claims are unsupported in current artifact state.
   Refs: formalization/MailboxActors/MailboxActors/System/State.lean:575, main.tex:98, main.tex:2356, main.tex:2366.
   Classification: mismatch.

2. High: Causal global-preservation overclaim; broker-safety remains an assumption.
   Why: paper says concrete instantiation discharges broker-safety, but theorem causal_invariant_preserved still assumes it and no discharge theorem is provided.
   Refs: main.tex:2256, main.tex:2376, formalization/MailboxActors/MailboxActors/Examples/CausalTrace.lean:52.
   Classification: mismatch.

3. High: causalAction_preserves_invariant theorem is weaker than prose implication.
   Why: theorem does not directly prove post-effect causal invariant over resulting mailbox state; it proves branch-local dependency facts.
   Refs: main.tex:2240, formalization/MailboxActors/MailboxActors/Examples/CausalMailbox.lean:235.
   Classification: mismatch.

4. Medium: Internal inconsistency on constructivity in conclusion.
   Why: conclusion says constructive proofs include eventual delivery, but Properties remark explicitly states eventual delivery uses classical contradiction.
   Refs: main.tex:2209, main.tex:2360.
   Classification: paper-only.

5. Medium: Judgment-form count mismatch.
   Why: intro says “eighteen rules grouped into four judgment forms,” but paper defines five forms.
   Refs: main.tex:107, main.tex:821.
   Classification: paper-only.

6. Medium: Well-typedness definition drift (freshness constraints).
   Why: paper freshness mentions node+engine identifiers; Lean nextId_fresh constrains engine addresses, and adds separate nodes_exist requirement not stated in paper definition.
   Refs: main.tex:2038, formalization/MailboxActors/MailboxActors/System/WellTyped.lean:35, formalization/MailboxActors/MailboxActors/System/WellTyped.lean:43.
   Classification: mismatch.

D) Potential False Positives

1. mailboxPersistence ignoring hterm in proof is acceptable: theorem is about removeEngineAt behavior at paired address, independent of termination status (formalization/MailboxActors/MailboxActors/Properties/Isolation.lean:113).
2. IsExecution being explicit in Lean eventual-delivery theorem is not inherently a mismatch; paper also quantifies over an execution trace (main.tex:2172, formalization/MailboxActors/MailboxActors/Properties/Delivery.lean:156).
3. Restricting S-Clean to processing engines in Lean is consistent with the paper’s intended mailbox-persistence narrative, even if rule text is brief (main.tex:1060, formalization/MailboxActors/MailboxActors/Semantics/Judgment.lean:190).

E) Fix Plan (ordered by impact/effort)

1. Fix artifact buildability first: repair System/State.lean errors at formalization/MailboxActors/MailboxActors/System/State.lean:575 and re-run full lake build.
2. Align theorem statements between paper and Lean: update main.tex Type Preservation/Progress/Mailbox Isolation statements to match Lean, or strengthen Lean to match paper.
3. Rework eventual-delivery formalization: define fairness over enabled OpStep transitions (or labeled actions), require/use IsExecution, and tie predicate P to OpStep.mEnqueue.
4. Resolve payload semantics drift: either update Lean rules to enforce Append mediation or revise paper rules/notation to the current dependent-pair payload model.
5. Correct logic-mode claims: remove “all other propositions constructive” unless proofs are refactored to avoid classical principles; fix conclusion contradiction.
6. Add missing formal links claimed in paper: no-orphaned-messages lemma from well-typedness, and theorem discharging broker-safety for the concrete causal instantiation.

F) Confidence: 87/100.
Evidence is from direct line-level inspection of main.tex and Lean source plus a concrete lake build failure. Confidence would increase with a successful full rebuild after System/State.lean repair and with access to the “extended version” proofs referenced at main.tex:2023.