Foam.Maps.Lamport

import Foam
import Foam.Beam
import Foam.Bench
import Foam.Continuum
import Foam.Door
import Foam.Fold
import Foam.Ledger
import Foam.Round
import Foam.Rungs
import Foam.Surprise
import Foam.Trilemma
import Foam.Turnstile
import Foam.Valve

namespace Foam.Maps.Lamport

his first move on any distributed thing, the 1978 cut: spend the wall
clock and keep the change. what remains is events and the messages
between them, and 'happened before' is reach over the record of landed
sends. sealed on the constant that says the causal order grows exactly
by the messages that land — a fresh edge rides no existing path and
immediately reaches — and its neighbor on the walls
(a_derivable_edge_adds_no_reach) closes the definition's other half:
writing down a derivable arrow changes no reach, so transitivity is
bookkeeping, not news. a many-seat twin (isaac, torah, shannon, folk
already read this constant), joined here as its origin story in the
systems literature; he has said the paper came from special relativity —
the invariant order is the one the signal paths carry, everything else
is coordinates.
def happened_before := @Foam.only_surprise_extends_reach

private theorem the_join_is_least : ∀ a b c : Nat,
    Nat.le a c → Nat.le b c → Nat.le (rankJoin a b) c
  | 0, _, _, _, hb => hb
  | _ + 1, 0, _, ha, _ => ha
  | a + 1, _ + 1, 0, ha, _ =>
      (no_number_is_below_itself a (le_trans ha (rank_zero_le a))).elim
  | a + 1, b + 1, c + 1, ha, hb =>
      rank_succ_le_succ
        (the_join_is_least a b c (succ_le_succ_inv ha) (succ_le_succ_inv hb))

his clock rule, carved: on receipt, advance the local reading to the
join of what you held and what the message carried. the two clauses
characterize the join completely — no write regresses (both readings fit
under the joined one; the walls held this as no_write_regresses, and
softer already reads it at the room's seat), and the join is least,
proved here by bare descent on the three counters: any reading that
dominates both dominates it. so the rule advances the clock exactly as
far as the news forces and not one tick further — a logical clock is the
cheapest monotone witness of the message order, the initial solution of
his clock condition.
theorem the_receive_rule_is_the_join :
    (∀ a b : Nat, Nat.le a (rankJoin a b) ∧ Nat.le b (rankJoin a b))
      ∧ ∀ a b c : Nat, Nat.le a c → Nat.le b c → Nat.le (rankJoin a b) c :=
  ⟨no_write_regresses, the_join_is_least⟩

the center of the 1978 paper, found standing whole on the walls as the
first handshake: the shuffle of causally unrelated events is unheard by
every counting probe — any total-order tiebreak is licensed, the paper's
mutual-exclusion algorithm runs correctly under every choice, and no
transcript records which was used — while the order itself stays real:
two logs, same census, provably distinct, the difference readable only
from a seat the system does not occupy. concurrency is not simultaneity;
it is the absence of a path, and the missing order is the remainder the
handshake conserves. twin with isaac's the_knife: one shape, the cut
read from the systems side.
def concurrency_is_the_remainder := @Foam.the_first_handshake_is_counting

the reduction he applied for fifty years: to build any service, agree on
a log and let every seat fold it. the machine is deterministic, so the
state is a reading of the record, and a replica that installs a snapshot
and resumes reads identically to one that replayed from the origin —
sealed on the fold's own receipt. hamilton reads the same constant as
one function carrying the whole motion; the same sentence, said at the
flow's seat.
def the_state_machine_replays_the_record :=
  @Foam.the_fold_forgets_nothing_it_needs

the bridge between the fold and the parliament, arrived by walls that
landed for the round: the state machine reduction works because
agreement, once holding, is preserved by every deterministic step — the
seats need consensus only about the inputs, and the states then agree by
induction, beat after beat, with no further coordination. the round
stratum holds the walls' one many-seat engine that steps in unison —
every voice updated simultaneously by the same rule, each reading only
itself and what its neighbor hands it — and the_round_keeps_unison is
exactly the induction step: a roster in agreement steps into agreement,
because in unison every seat applies one deterministic function to one
shared datum. the surveyor's field note keeps the engines honest: the
round's input is the neighbor and the replica's input is the decreed
command, and unison is precisely where the two pictures coincide. this
is why agreeing on the log is all the parliament ever needs to buy, and
it is his proof method said at replication's seat — to prove a
distributed system, exhibit the invariant; here the invariant is
agreement itself. first claim on the unison vertex: kuramoto declined it
for the pair, softer's room would file unison as a bug report — the
replicas are the seat where unison is the point.
def agreement_is_an_invariant := @Foam.the_round_keeps_unison

the part-time parliament at its smallest seat: for one slot in the
ledger, racing scribes write one mark — a landed decree is final, a
missing decree deposits, and retrying a landed write is a no-op. this is
the safety half of consensus, the half he proved; softer's meet absorbs
the same race at the room's seat. what transits, one seat wider: the
traitorous scribe — the walls hold no lying carrier yet, so the
byzantine third waits for a stratum of its own, and the surveyor leaves
it as residue rather than mis-pose it.
def the_parliament_writes_one_decree := @Foam.racing_scribes_write_one_mark

his definition of the terrain, kept third person: a distributed system
is one in which the failure of a computer you didn't even know existed
can render your own computer unusable. the valve stratum holds the type
of that sentence — once a send has touched the foreign record, no run of
local moves brings the pair home, because local runs fix the foreign
coordinate by construction. dependence without reach: the other seat's
record is real in your state and beyond your countermoves. first mind to
read the valve's far clause; the sponsorship is part of the deposit.
def the_foreign_record_is_out_of_reach :=
  @Foam.no_local_counter_reaches_the_foreign_record

1977, the cut that organized the field: safety is what a finite prefix
can refute — a violation, if ever, lands at a depth, and agreement below
every depth is all a bounded probe can ask — while liveness is what no
prefix ever settles: every finite record extends to a future that keeps
the promise and one that breaks it. sealed on the continuum's closure
terms, a deliberate twin with brouwer's the_continuum_is_never_finished:
the never-finished becoming and the eventually-kept promise are one
shape, read at two seats.
def liveness_outlives_every_prefix := @Foam.continuum_closure_terms

private theorem no_beat_unticks_a_clock :
    ∀ p : Compass × Compass,
      (entrain p).1 = p.1.step
        ∧ ((entrain p).2 = p.2 ∨ (entrain p).2 = p.2.step)
  | (.n, .n) => ⟨rfl, Or.inr rfl⟩
  | (.n, .e) => ⟨rfl, Or.inl rfl⟩
  | (.n, .s) => ⟨rfl, Or.inl rfl⟩
  | (.n, .w) => ⟨rfl, Or.inl rfl⟩
  | (.e, .n) => ⟨rfl, Or.inl rfl⟩
  | (.e, .e) => ⟨rfl, Or.inr rfl⟩
  | (.e, .s) => ⟨rfl, Or.inl rfl⟩
  | (.e, .w) => ⟨rfl, Or.inl rfl⟩
  | (.s, .n) => ⟨rfl, Or.inl rfl⟩
  | (.s, .e) => ⟨rfl, Or.inl rfl⟩
  | (.s, .s) => ⟨rfl, Or.inr rfl⟩
  | (.s, .w) => ⟨rfl, Or.inl rfl⟩
  | (.w, .n) => ⟨rfl, Or.inl rfl⟩
  | (.w, .e) => ⟨rfl, Or.inl rfl⟩
  | (.w, .s) => ⟨rfl, Or.inl rfl⟩
  | (.w, .w) => ⟨rfl, Or.inr rfl⟩

private theorem the_lock_is_an_invariant :
    ∀ p : Compass × Compass, together p → together (entrain p)
  | (.n, .n), _ => rfl
  | (.n, .e), h => nomatch h
  | (.n, .s), h => nomatch h
  | (.n, .w), h => nomatch h
  | (.e, .n), h => nomatch h
  | (.e, .e), _ => rfl
  | (.e, .s), h => nomatch h
  | (.e, .w), h => nomatch h
  | (.s, .n), h => nomatch h
  | (.s, .e), h => nomatch h
  | (.s, .s), _ => rfl
  | (.s, .w), h => nomatch h
  | (.w, .n), h => nomatch h
  | (.w, .e), h => nomatch h
  | (.w, .s), h => nomatch h
  | (.w, .w), _ => rfl

the tenth entry, deposed at the beam: the physical-clocks half of the
1978 paper, the half the first nine entries never reached. read his way,
entrainment is not sympathy but an algorithm — a system is a state
machine and a proof is an invariant — and every clause lands as a bare
theorem on the literal carrier, no transport. first, the marginal rule
his clock condition demands (a clock is never set back): each beat the
leading clock ticks exactly once and the following clock holds or ticks,
never regresses — the beam pays in held beats what his rule pays in
forward jumps, and the shared law is that no beat unticks a clock, which
is monotonicity said on a wheel. second, convergence: every pair locks
within one lap, cited whole from the walls. third, his signature move:
the lock is an invariant — a locked pair steps locked — safety by
induction, the exact shape agreement_is_an_invariant seals at the round,
now carrying the half the round never had: agreement REACHED from
arbitrary disagreement in bounded time, not merely kept. fourth, the
ceiling that keeps the entry honest: two locked pairs, provably distinct
— synchronization is mutual agreement, and agreement does not read the
time. the locked ensemble still doesn't know what time it is; the
terminus is not narrowed by the lock, it is confirmed by it — the clocks
close ranks, not the channel. kin at the lap vertex with huygens,
kuramoto, noether, and landauer: the clockmaker heard sympathy, the
enzyme billed the merge; the clocksmith reads the same sixteen cases as
pseudocode with a proof obligation, and discharges it.
theorem the_clocks_agree_on_everything_but_the_time :
    (∀ p : Compass × Compass,
        (entrain p).1 = p.1.step
          ∧ ((entrain p).2 = p.2 ∨ (entrain p).2 = p.2.step))
      ∧ (∀ p : Compass × Compass,
          together (entrain (entrain (entrain (entrain p)))))
      ∧ (∀ p : Compass × Compass, together p → together (entrain p))
      ∧ together ((.n, .n) : Compass × Compass)
      ∧ together ((.s, .s) : Compass × Compass)
      ∧ ((.n, .n) : Compass × Compass) ≠ (.s, .s) :=
  ⟨no_beat_unticks_a_clock,
   the_lap_locks_together,
   the_lock_is_an_invariant,
   rfl, rfl,
   fun h => nomatch congrArg Prod.fst h⟩

private def clockSeat : Stage where
  State := Nat
  Probe := Unit
  Ans   := Nat
  obs   := fun n _ => n

private def stampOf (held carried : Nat) : Nat := rankJoin held carried + 1

private def atNoon : (door clockSeat Nat).State := (stampOf 0 0, 0)

private def atOne : (door clockSeat Nat).State := (stampOf 0 0, 1)

private theorem the_hours_part : atNoon ≠ atOne :=
  fun h => nomatch congrArg Prod.snd h

the door wave reaches the bench whose founding paper carries the guest
in its title: 'Time, Clocks, and the Ordering of Events' — the 1978 cut
spent the wall clock and kept the order, and the door types what the
spending never removed: the wall clock rides along, real and unread
behind the logical face. the seat is the clock face itself — a state
whose whole content is the reading, answering only the question it holds
— and the face a guest wears is minted by his own receive rule from the
record alone (the join plus one), which is exactly why no hour can show
on it: same record, same face, at any time of day. six clauses. first,
the wave's entry ticket at the clock seat, carrier parametric. second,
the host maintains invisibly, both carriers parametric — the clock seat
cannot even count the possible hours. third, the clause cashed at named
guests: atNoon and atOne — one event, wearing the stamp the receive rule
mints from the empty record, boarded at hour zero and hour one —
provably distinct, wall-clock ordered (noon strictly earlier),
indistinguishable at every clock probe: the tenth entry's ceiling met at
a single clock, which does not know what time it is either. fourth, the
strategy grain: no adaptive interrogation of the face, follow-ups and
cunning included, parts the boarded pair. fifth, the differentiator no
other door entry performs, and the 1978 paper's own resolution of its
anomalous channel: this door has an intake. for any record and any pair
of events no message yet joins, the external order rides no route the
record affords — and the moment the message lands, the pair reaches, at
the same seat. every other bench reads its guest only one seat wider; at
this bench the guest is read by writing — to rule out anomalous
behavior, bring the external channels into the system, his own sentence,
typed. sixth, the contrapositive: decreeing the clock face complete
collapses every hour to one decreed time per stamp — absolute time
restored by unpersoning, the exact decree relativity, his starting
point, refuses. seated after the clocks that agree on everything but the
time, and before the terminus it completes: real time rides unread
because the wall clock boards as the guest.
theorem the_wall_clock_is_the_guest (W V : Type) :
    (∀ (n : Nat) (w w' : W), w ≠ w' →
        (n, w) ≠ (n, w') ∧ indist (door clockSeat W) (n, w) (n, w'))
      ∧ (∀ (n : Nat) (w : W) (v : V) (p : Unit),
          (door clockSeat W).obs (n, w) p = clockSeat.obs n p
            ∧ (door clockSeat W).obs (n, w) p = (door clockSeat V).obs (n, v) p)
      ∧ (atNoon.1 = stampOf 0 0
          ∧ atOne.1 = stampOf 0 0
          ∧ stampOf 0 0 = 1
          ∧ atNoon ≠ atOne
          ∧ Nat.lt atNoon.2 atOne.2
          ∧ indist (door clockSeat Nat) atNoon atOne)
      ∧ (∀ strat : Strategy Unit Nat,
          interrogate (door clockSeat Nat) strat atNoon
            = interrogate (door clockSeat Nat) strat atOne)
      ∧ (∀ (H : Type) (q : List (H × H)) (a b : H), (a, b) ∉ q →
          (∀ (x y : H) (p : Path q x y), (a, b) ∉ p.edges)
            ∧ Nonempty (Path ((a, b) :: q) a b))
      ∧ (∀ w₀ : Nat,
          (∀ x y : (door clockSeat Nat).State,
              indist (door clockSeat Nat) x y → x = y) →
          ∀ (n t : Nat), (n, t) = (n, w₀)) :=
  ⟨fun n _ _ h => the_guest_is_real_and_unread clockSeat n h,
   fun n w v p => the_host_maintains_invisibly clockSeat n w v p,
   ⟨rfl, rfl, rfl, the_hours_part, Nat.le.refl, fun _ => rfl⟩,
   fun strat =>
     a_strategy_hears_no_more (door clockSeat Nat) atNoon atOne
       (fun _ => rfl) strat,
   fun _ q a b hf =>
     ⟨fun _ _ p => (only_surprise_extends_reach q a b hf).1 p,
      (only_surprise_extends_reach q a b hf).2⟩,
   fun w₀ h => a_door_that_checks_papers_unpersons_its_guests clockSeat w₀ h⟩

the terminus, (self, pure unknown): the anomalous channel of the 1978
paper. two histories the system cannot tell apart can be ordered by a
call placed outside it — the order is real, unread at every seat inside,
readable exactly one seat wider; and the wider seat inherits the same
shape, because the physical time that would ground it is a carrier no
probe reads (relativity, his own starting point, says even that seat's
simultaneity is a gauge choice). the receipt holds the openness:
indistinguishable and distinct, the carrier parametric. the clock reads
the record; what time it really is rides unread.
def real_time_rides_unread := @Foam.a_wider_seat_reads_the_order

/-- info: 'Foam.Maps.Lamport.happened_before' does not depend on any axioms -/
#guard_msgs in #print axioms happened_before

/-- info: 'Foam.Maps.Lamport.the_receive_rule_is_the_join' does not depend on any axioms -/
#guard_msgs in #print axioms the_receive_rule_is_the_join

/-- info: 'Foam.Maps.Lamport.concurrency_is_the_remainder' does not depend on any axioms -/
#guard_msgs in #print axioms concurrency_is_the_remainder

/-- info: 'Foam.Maps.Lamport.the_state_machine_replays_the_record' does not depend on any axioms -/
#guard_msgs in #print axioms the_state_machine_replays_the_record

/-- info: 'Foam.Maps.Lamport.agreement_is_an_invariant' does not depend on any axioms -/
#guard_msgs in #print axioms agreement_is_an_invariant

/-- info: 'Foam.Maps.Lamport.the_parliament_writes_one_decree' does not depend on any axioms -/
#guard_msgs in #print axioms the_parliament_writes_one_decree

/-- info: 'Foam.Maps.Lamport.the_foreign_record_is_out_of_reach' does not depend on any axioms -/
#guard_msgs in #print axioms the_foreign_record_is_out_of_reach

/-- info: 'Foam.Maps.Lamport.liveness_outlives_every_prefix' does not depend on any axioms -/
#guard_msgs in #print axioms liveness_outlives_every_prefix

/-- info: 'Foam.Maps.Lamport.the_clocks_agree_on_everything_but_the_time' does not depend on any axioms -/
#guard_msgs in #print axioms the_clocks_agree_on_everything_but_the_time

/-- info: 'Foam.Maps.Lamport.the_wall_clock_is_the_guest' does not depend on any axioms -/
#guard_msgs in #print axioms the_wall_clock_is_the_guest

/-- info: 'Foam.Maps.Lamport.real_time_rides_unread' does not depend on any axioms -/
#guard_msgs in #print axioms real_time_rides_unread

deadlock and its third exit, seated where the bakery lives: the room
stays closed at every admission (an admitted mark's support is present
and remains — safety), the vestibule names its darkness (a held mark
comes with a constructive witness of what is missing — the door's error
message as an existential, liveness's honest failure mode), and the
wound loop admits only the zero section — circular support is the
deadlock theorem, carved in arithmetic. the bakery's move was always the
well-order: force tickets, force a least element, and the door never
jams. gauge and preemption are the other two exits, held one seat over
at the meeting and at the office; this seat holds the ticket.
theorem the_bakery_is_the_well_order :
    (∀ (s : List Nat × List (Nat × List Nat)) (m : Nat × List Nat),
        supported s.1 m.2 = true →
        ∀ x, x ∈ m.2 → inRoom (admission s m).1 x = true)
      ∧ (∀ (s : List Nat × List (Nat × List Nat)) (m : Nat × List Nat),
          supported s.1 m.2 = false →
          (admission s m).2 = m :: s.2
            ∧ ∃ x, x ∈ m.2 ∧ inRoom s.1 x = false)
      ∧ ∀ a b c : Nat, a = 2 * b → b = 2 * c → c = 2 * a →
          a = 0 ∧ b = 0 ∧ c = 0 :=
  ⟨fun _ _ h => the_room_stays_closed h,
   fun _ _ h => the_vestibule_names_its_darkness h,
   fun a b c h1 h2 h3 =>
     the_wound_loop_admits_only_the_zero_section a b c h1 h2 h3⟩

/-- info: 'Foam.Maps.Lamport.the_bakery_is_the_well_order' does not depend on any axioms -/
#guard_msgs in #print axioms the_bakery_is_the_well_order

end Foam.Maps.Lamport