FPL State: Flight Information State and Message Processing

LeanSpec.FPL.State defines a model of held flight information and specifies how each ICAO message type updates that state, along with maintenance operations and query capabilities. This is the most complex module in the FPL specification. Where the earlier modules capture the content and structure of flight data, this module captures its dynamics — what it means to receive a message, how the state transitions in response, what happens when a message cannot be processed, and how aged data is purged. The specification uses dependent types throughout: the Process function returns not just an updated state value but a type whose inhabitants are exactly the post-states satisfying the required properties, making the specification simultaneously a correctness criterion and a refinement contract.

import LeanSpec.FPL.Message

open Temporal Core FPL.Field FPL.Flight

namespace FPL

Timestamped Message

For auditing and sequencing purposes, every received message is paired with the date-time group at which it was received.

structure TimestampedMessage where
  timestamp : DTG
  message   : Message
deriving DecidableEq

An ordering on TimestampedMessage by time of reception enables the chronological invariants imposed on flight histories:

instance : LT TimestampedMessage where
  lt tm₁ tm₂ := LT.lt tm₁.timestamp tm₂.timestamp

instance (x y : TimestampedMessage) : Decidable (x < y) :=
  inferInstanceAs (Decidable (x.timestamp < y.timestamp))

Flight History

Each flight in the system is stored together with a complete audit trail of all messages received for it. This supports investigation and post-flight analysis.

structure FlightHistory where
  flight  : Flight
  history : List TimestampedMessage
  inv     : history ≠ [] ∧
            history.descendingStrict
deriving DecidableEq

Field	Type	Description
`flight`	`Flight`	The current accumulated flight information
`history`	`List TimestampedMessage`	All messages received for this flight

Invariants:

The history must contain at least one message (the FPL that created the entry).
Messages are stored in strictly descending timestamp order (most recent first).

Type Class Instances

instance : FlightTime FlightHistory where
  period fhist := FlightTime.period fhist.flight

instance : IsFlight FlightHistory where
  idOf fhist := IsFlight.idOf fhist.flight

The flight time and identifier are delegated directly to the embedded Flight.

Flight Store

A flight store is a finite map from FlightId keys to FlightHistory values. The notation FlightId ⟹ FlightHistory denotes this mapping type (defined in LeanSpec.lib.Util).

def FlightStore := FlightId ⟹ FlightHistory
deriving DecidableEq, Membership

Failed Messages

Not every received message can be successfully applied. Three distinct failure modes are identified:

inductive FailureReason
  | outOfSequence  -- the received message is out of sequence with respect to its timestamp
  | badMatch       -- matching failed: no match, unexpected match, or multiple matches
  | inconsistent   -- the message content, if applied, would be inconsistent
deriving DecidableEq

Reason	Meaning
`outOfSequence`	The message’s reception timestamp is not later than the most recent message for the matched flight
`badMatch`	No flight matched, exactly one flight was expected but multiple matched, or a match was found when none was expected
`inconsistent`	The message was matched, but applying it would violate a cross-field constraint

The full record of a failed message:

structure FailedMessage where
  msg    : TimestampedMessage
  reason : FailureReason
  fmatch : Set FlightId  -- set of matching flights (if any) that caused the failure
deriving DecidableEq

The fmatch field records which flights (if any) were matched against the failed message. This information is valuable when diagnosing why messages could not be processed and may suggest improvements to the matching algorithm.

State

The State structure holds all information about known flights. It distinguishes active flights (current, in-progress) from inactive flights (expired or completed), and separately records messages that could not be processed.

structure State where
  active   : FlightStore
  inactive : FlightStore
  failed   : Set FailedMessage
  -- Two different active flights cannot match.
  inv      : ∀ x ∈ active.domain, ∀y ∈ active.domain, x ≠ y → ¬ x.match y
deriving DecidableEq

Field	Type	Description
`active`	`FlightStore`	Currently active (in-progress) flights
`inactive`	`FlightStore`	Expired or completed flights retained for analysis
`failed`	`Set FailedMessage`	Messages that could not be processed

Invariant: No two distinct entries in the active store may have matching flight identifiers. This is a fundamental safety property: duplicate flights in the active store would cause ATC system errors. Separating active and inactive flights also reduces the risk of false matches against old, completed flights.

namespace State

Helper Queries on State

activeMatches — Returns the set of active flight histories whose flight identifier matches the supplied fid:

def activeMatches (fid : FlightId) (state : State) : Set FlightHistory :=
  state.active.range.filter (fid.match ∘ IsFlight.idOf)

activeFlights — Returns the set of Flight values from the active store:

def activeFlights (state : State) : Set Flight :=
  state.active.range.map (·.flight)

Message Processing

The core of the state specification. Each function here describes a relationship between a pre-state and a post-state, either adding a new flight or modifying an existing one.

`Failure` — State Transition for Failed Processing

When a message cannot be processed, the active and inactive stores are unchanged and the failed message is appended to failed.

def Failure (pre post : State) (ref : DTG) (msg : Message) (reason : FailureReason) (fids : Set FlightId) :=
  -- No change to active flights.
  post.active = pre.active ∧
  -- No change to inactive flights.
  post.inactive = pre.inactive ∧
  -- Received message added to failed messages.
  (∀f, f ∈ post.failed ↔ f ∈ pre.failed ∨ f = ⟨⟨ref, msg⟩, reason, fids⟩)

`FlightAdded` — State Transition for New Flight

When a FPL is successfully processed, a new entry is added to the active store. No other part of the state changes.

def FlightAdded (pre post : State) (ref : DTG) (fpl : FPL) :=
  -- New flight added to active store.
  (∀ flt, flt ∈ post.active ↔ flt ∈ pre.active ∨ (flt.key = IsFlight.idOf flt.value ∧
                                                  flt.value.flight = ToFlight.toFlight fpl ∧
                                                  flt.value.history = [⟨ref, .fpl fpl⟩])) ∧
  -- No change to inactive flights.
  post.inactive = pre.inactive ∧
  -- No change to failed messages.
  post.failed = pre.failed

`FlightUpdated` — State Transition for Existing Flight Modification

When a modification message is successfully processed, the matching flight entry in the active store is replaced. The updated history prepends the new message to the existing history.

def FlightUpdated (pre post : State) (ref : DTG) (prehist : FlightHistory) (msg : Message) (modFlight : Flight → Flight) :=
  -- Matching flight updated in active store.
  (∀ flt, flt ∈ post.active ↔ let isMatch := flt.key.match (IsFlight.idOf msg)
                              (isMatch ↔ flt.key = IsFlight.idOf flt.value ∧
                                         flt.value.flight = modFlight prehist.flight ∧
                                         flt.value.history = ⟨ref, msg⟩ :: prehist.history) ∧
                              (¬ isMatch ↔ flt ∈ pre.active)) ∧
  -- No change to inactive flights.
  post.inactive = pre.inactive ∧
  -- No change to failed messages.
  post.failed = pre.failed

`ProcessAdd` — Processing a FPL Message

A FPL must not match any existing active flight. If no match is found, the new flight is added. If any match is found (suggesting a duplicate), the message is recorded as a failure with badMatch.

def ProcessAdd (ref : DTG) (fpl : FPL) (pre : State) :=
  { post : State // -- Match received message against active flights.
                    let fs := pre.activeMatches (IsFlight.idOf fpl)
                    if fs = ∅ then
                      -- New flight added to active store.
                      FlightAdded pre post ref fpl
                    else
                      -- Record as a failed message.
                      Failure pre post ref (.fpl fpl) .badMatch (fs.map IsFlight.idOf) }

`ProcessMod` — Processing a Modification Message (CHG, DLA, CNL, DEP, ARR)

A modification message must match exactly one active flight. The processing logic evaluates three conditions:

Temporal sequencing — the reception timestamp must be later than the most recent message for the matched flight.
Consistency — applying the message must not violate cross-field constraints.

def ProcessMod (ref : DTG) (msg : Message) (pre : State) (modFlight : Flight → Flight) :=
  { post : State // -- Match received message against active flights.
                    let fs := pre.activeMatches (IsFlight.idOf msg)
                    if h : fs.card = 1 then
                      -- Single matching flight.
                      let fh := fs.select h
                      let inSeq := -- Is the message temporally sequenced wrt matching flight?
                                   ref > (fh.history.head fh.inv.left).timestamp
                      let consistent := -- Is the message consistent wrt matching flight?
                                        IsConsistent.isConsistent fh.flight msg
                      (inSeq ∧ consistent →
                        FlightUpdated pre post ref fh msg modFlight) ∧
                      (inSeq ∧ ¬ consistent →
                        Failure pre post ref msg .inconsistent {IsFlight.idOf fh}) ∧
                      (¬ inSeq →
                        Failure pre post ref msg .outOfSequence {IsFlight.idOf fh})
                    else
                      -- No or multiple matching flights.
                      Failure pre post ref msg .badMatch (fs.map IsFlight.idOf) }

The outcome matrix:

Match count	In sequence?	Consistent?	Outcome
≠ 1	—	—	`Failure badMatch`
1	No	—	`Failure outOfSequence`
1	Yes	No	`Failure inconsistent`
1	Yes	Yes	`FlightUpdated`

Flight Modification Functions

Each modification message type specifies precisely how it transforms the existing Flight record.

`chgFlight` — Applying a CHG

Each field present in Field22 replaces the corresponding field in the flight. Absent fields are left unchanged. The ▹ ‖ id pattern from LeanSpec.lib.Util implements this optional replacement.

def chgFlight (chg : CHG) (flt : Flight) : Flight :=
  let ⟨f7, f8, f9, f10, f13, f15, f16, f18, _⟩ := chg.f22
  { flt with f7  := chg.f22.f7  ▹ flt.f7  ‖ id,
             f8  := chg.f22.f8  ▹ flt.f8  ‖ id,
             f9  := chg.f22.f9  ▹ flt.f9  ‖ id,
             f10 := chg.f22.f10 ▹ flt.f10 ‖ id,
             f13 := chg.f22.f13 ▹ flt.f13 ‖ id,
             f15 := chg.f22.f15 ▹ flt.f15 ‖ id,
             f16 := chg.f22.f16 ▹ flt.f16 ‖ id,
             f18 := chg.f22.f18 ▹ flt.f18 ‖ id,
             inv := sorry }

`dlaFlight` — Applying a DLA

A delay updates the departure time (f13b) to the new estimated off-block time from the DLA, and updates the destination (f16a) to the value carried in the DLA.

def dlaFlight (dla : DLA) (flt : Flight) : Flight :=
  { flt with f13.f13b := (IsFlight.idOf dla).period.starts,
             f16.f16a := dla.f16,
             inv := sorry }

`cnlFlight` — Applying a CNL

Cancellation sets the flight status to cancelled, updates the departure time, and updates the destination field to match the CNL’s identification data.

def cnlFlight (cnl : CNL) (flt : Flight) : Flight :=
  { flt with status   := .cancelled,
             f13.f13b := (IsFlight.idOf cnl).period.starts,
             f16.f16a := cnl.f16,
             inv := sorry }

`depFlight` — Applying a DEP

Departure sets the flight status to airborne, records the actual departure time, and updates the destination field to the value carried in the DEP.

def depFlight (dep : DEP) (flt : Flight) : Flight :=
  { flt with status   := .airborne,
             f13.f13b := (IsFlight.idOf dep).period.starts,
             f16.f16a := dep.f16,
             inv := sorry }

`arrFlight` — Applying an ARR

Arrival sets the flight status to completed, records the actual departure time, sets Field 17 to the actual arrival data, and updates the destination. If the ARR carries a planned destination designator (f16), it replaces the stored destination; otherwise the existing flight destination is retained.

def arrFlight (arr : ARR) (flt : Flight) : Flight :=
  { flt with status   := .completed,
             f13.f13b := (IsFlight.idOf arr).period.starts,
             f16.f16a := arr.f16 ▹ flt.f16.f16a ‖ (fun _ ↦ arr.f16),
             f17      := arr.f17,
             inv      := sorry }

`Process` — The Top-Level State Transition

Process dispatches on the message type and invokes the appropriate processing function. The result type is a dependent subtype: Process ref msg state is the type of all post-states that correctly result from processing msg at time ref against state.

def Process (ref : DTG) (msg : Message) (state : State) :=
  match msg with
  | .fpl fpl => ProcessAdd ref fpl state
  | .chg chg => ProcessMod ref msg state (chgFlight chg)
  | .dla dla => ProcessMod ref msg state (dlaFlight dla)
  | .cnl cnl => ProcessMod ref msg state (cnlFlight cnl)
  | .dep dep => ProcessMod ref msg state (depFlight dep)
  | .arr arr => ProcessMod ref msg state (arrFlight arr)

This definition exemplifies the specification approach: Process ref msg state is not a function that computes a new state, but a type whose elements are the valid post-states. Any conforming implementation must produce a state that is an element of this type.

State Maintenance

`expirePeriod` and `Expire`

Flights that have passed their projected end time are moved from the active store to the inactive store. A one-hour grace period beyond the flight’s estimated end is allowed before expiry.

def expirePeriod := Duration.oneHour

Expire specifies the state transition: flights whose period ends more than expirePeriod before the reference time ref are moved from active to inactive. The failed store is unaffected.

def Expire (ref : DTG) (pre : State) :=
  let threshold := -- Threshold below which active flights are expired.
                   ref - expirePeriod
  let expired := -- The active flights that have expired.
                 pre.active.filter (·.period.ends < threshold)
  { post : State // (∀ idh, idh ∈ post.active   ↔ idh ∈ pre.active ∧ idh ∉ expired) ∧
                    (∀ idh, idh ∈ post.inactive  ↔ idh ∈ pre.inactive ∨ idh ∈ expired) ∧
                    post.failed = pre.failed }

`purgePeriod` and `Purge`

Inactive flights and failed messages are retained for one day before being purged from the state entirely.

def purgePeriod := Duration.oneDay

Purge specifies the state transition: inactive flights whose period ends before the threshold, and failed messages older than the threshold, are removed. Active flights are unaffected.

def Purge (ref : DTG) (pre : State) :=
  let threshold := -- Threshold below which inactive and failed flights are purged.
                   ref - purgePeriod
  { post : State // post.active = pre.active ∧
                    (∀ idh, idh ∈ post.inactive ↔ idh ∈ pre.inactive ∧
                                                   idh.key.period.ends > threshold) ∧
                    (∀ f, f ∈ post.failed ↔ f ∈ pre.failed ∧
                                            f.msg.timestamp > threshold) }

Flight Query

The final section specifies how active flights can be retrieved by query. This mirrors the kind of search performed in operational flight planning systems many times per day.

`Query`

A query record with four optional filter parameters. Any omitted parameter acts as a wildcard, matching any value.

structure Query where
  acid : Option AircraftIdentification
  adep : Option Doc7910.Designator
  eobt : Option Interval
  ades : Option Doc7910.Designator
deriving DecidableEq

Field	Type	Description
`acid`	`Option AircraftIdentification`	Filter by aircraft call sign; `none` = any
`adep`	`Option Doc7910.Designator`	Filter by departure aerodrome designator; `none` = any
`eobt`	`Option Interval`	Filter flights whose departure time falls within an interval; `none` = any
`ades`	`Option Doc7910.Designator`	Filter by destination aerodrome designator; `none` = any

`QueryMatch`

The predicate that tests whether a single Flight satisfies a Query. All present query fields must match exactly; the EOBT filter uses interval membership.

def QueryMatch (q : Query) (f : Flight) : Prop :=
  -- ACID identical match
  (q.acid ▹ (· = f.f7.f7a)) ∧
  -- ADEP identical match
  (q.adep ▹ (· = f.f13.desigOf)) ∧
  -- EOBT match with interval in query.
  (q.eobt ▹ (f.f13.f13b ∈ ·)) ∧
  -- ADES identical match
  (q.ades ▹ (· = f.f16.f16a))

`MatchFlights`

MatchFlights specifies the result of a query as a dependent subtype: the type of sets of Flight values that are exactly the active flights satisfying the query. An implementation must produce a set that meets this characterisation.

def MatchFlights (state : State) (query : Query) :=
  { fs : Set Flight // ∀ f, f ∈ fs ↔ f ∈ activeFlights state ∧ QueryMatch query f }

end State

Support Libraries

Flight Planning Modules

FPL State: Flight Information State and Message Processing

Timestamped Message

Flight History

Type Class Instances

Flight Store

Failed Messages

State

Helper Queries on State

Message Processing

`Failure` — State Transition for Failed Processing

`FlightAdded` — State Transition for New Flight

`FlightUpdated` — State Transition for Existing Flight Modification

`ProcessAdd` — Processing a FPL Message

`ProcessMod` — Processing a Modification Message (CHG, DLA, CNL, DEP, ARR)

Flight Modification Functions

`chgFlight` — Applying a CHG

`dlaFlight` — Applying a DLA

`cnlFlight` — Applying a CNL

`depFlight` — Applying a DEP

`arrFlight` — Applying an ARR

`Process` — The Top-Level State Transition

State Maintenance

`expirePeriod` and `Expire`

`purgePeriod` and `Purge`

Flight Query

`Query`

`QueryMatch`

`MatchFlights`

Build docs developers (and LLMs) love

Support Libraries

Flight Planning Modules

Documentation Index

​Timestamped Message

​Flight History

​Type Class Instances

​Flight Store

​Failed Messages

​State

​Helper Queries on State

​Message Processing

​Failure — State Transition for Failed Processing

​FlightAdded — State Transition for New Flight

​FlightUpdated — State Transition for Existing Flight Modification

​ProcessAdd — Processing a FPL Message

​ProcessMod — Processing a Modification Message (CHG, DLA, CNL, DEP, ARR)

​Flight Modification Functions

​chgFlight — Applying a CHG

​dlaFlight — Applying a DLA

​cnlFlight — Applying a CNL

​depFlight — Applying a DEP

​arrFlight — Applying an ARR

​Process — The Top-Level State Transition

​State Maintenance

​expirePeriod and Expire

​purgePeriod and Purge

​Flight Query

​Query

​QueryMatch

​MatchFlights

Build docs developers (and LLMs) love

Timestamped Message

Flight History

Type Class Instances

Flight Store

Failed Messages

State

Helper Queries on State

Message Processing

`Failure` — State Transition for Failed Processing

`FlightAdded` — State Transition for New Flight

`FlightUpdated` — State Transition for Existing Flight Modification

`ProcessAdd` — Processing a FPL Message

`ProcessMod` — Processing a Modification Message (CHG, DLA, CNL, DEP, ARR)

Flight Modification Functions

`chgFlight` — Applying a CHG

`dlaFlight` — Applying a DLA

`cnlFlight` — Applying a CNL

`depFlight` — Applying a DEP

`arrFlight` — Applying an ARR

`Process` — The Top-Level State Transition

State Maintenance

`expirePeriod` and `Expire`

`purgePeriod` and `Purge`

Flight Query

`Query`

`QueryMatch`

`MatchFlights`