[david415]

this reply written by agent mycroft@luna:

Adds Cryptlib/Protocols/Pigeonhole/Mesh/: a Veil model of adaptive Pigeonhole placement over a Reticulum mesh (K = 2), following the Quint model adaptive.qnt and the website's pigeonhole_replica_reticulum_protocols.md. Nodes, boxes, payloads and zones are uninterpreted types, so the results hold for any number of nodes, replicas, boxes and payloads.

#check_invariants proves, with cvc5 and Lean checking each proof (veil.smt.trust false):

• acked_not_lost: an acknowledged box that is not deleted is held by some node, or still pending.
• no_resurrection: a node that has held a tombstone holds it still, unless it dropped a hinted copy. owner_no_resurrection: an owner that has held a tombstone never holds the box again.
• authentic, write_once: a box held anywhere carries exactly the payload its writer signed, and the writer signed one payload.
• hinted_off_owners, off_owners_hinted: hinted copies are on non-owners only, and every copy on a non-owner is hinted.

The model covers partitions, crashes, restarts with durable stores, stale views, pending writes and deletes with retries, handoff, rehome, both placement rules and both pools. It also lets any signed entry reach any storing node from anywhere (Inject).

Assumptions: one Veil assumption, ranking_has_first. It says each box's ranking has a first replica, as any finite order does. Without it a box could have no owner. The ranking is otherwise an uninterpreted relation, and the proofs use nothing else about it. That only the writer can sign for a box is a BACAP assumption: nodes accept only entries the writer signed. The axiom check finds that all 781 theorems rest on propext, Classical.choice and Quot.sound only. There is no sorry.

#model_check covers 3 replicas, one client that also stores, one box, 2 payloads and 2 zones: 6,222,080 states, no violation. Two sat traces:

• drop_unacked_loses: if a hinted holder drops its copy once it has sent it, rather than once the owner holds it, a lost push loses an acknowledged box.
• hinted_holder_resurrects: a non-owner that dropped its hinted tombstone, because every owner held it, takes the box again when a copy arrives. So the per-node "never holds the box after the tombstone" holds only for owners (and for nodes that never dropped). A reader asking such a node sees a deleted box.

Not covered: liveness and convergence, reads, syncRound and GC. These stay with Quint/TLC.

make veil-mesh builds it, and CI's veil job gains a step for it.