Documentation Index
Fetch the complete documentation index at: https://mintlify.com/paulch42/lean-spec/llms.txt
Use this file to discover all available pages before exploring further.
LeanSpec.FPL.Flight defines the central data entity capturing all information about a flight, with invariants that enforce consistency between related fields using dependent types. A flight is not merely a record — it is a proof-carrying structure: constructing a Flight value requires simultaneously discharging all the cross-field constraints that ensure the data is internally coherent. This module also introduces the infrastructure for flight identification and matching (used to correlate incoming messages with stored flights), flight time estimation, and a set of type classes that abstract over flight-like entities throughout the specification.
import LeanSpec.FPL.Field
open Temporal Core FPL.Field
namespace FPL
Flight Identification
FlightId
The flight identifier is the key used to match received flight information against already-known flights. It is derived from three pieces of information:
acid — the aircraft identification (call sign) from Field 7a.adep — the departure aerodrome from Field 13a.period — a time interval computed from the departure time (Field 13b) and the estimated flight duration (Field 16b).
structure FlightId where
acid : AircraftIdentification
adep : Option ADep
period : Interval
deriving DecidableEq
def FlightId.match : FlightId → FlightId → Bool
| ⟨a₁,d₁,p₁⟩, ⟨a₂,d₂,p₂⟩ => a₁ = a₂ ∧ d₁ = d₂ ∧ p₁ ∩ p₂ ≠ ∅
Type Classes for Flight-Like Entities
FlightTime
Any type that has an identifiable flight time period implements this class. The method period maps a value to the Interval representing the flight’s duration on a timeline.
class FlightTime (α: Type) where
period : α → Interval
IsFlight
Any type from which a FlightId can be derived implements IsFlight. This requires a prior FlightTime instance — flight identification presupposes a knowable time period.
class IsFlight (α : Type) [FlightTime α] where
idOf : α → FlightId
ToFlight
Any type from which a full Flight can be generated implements ToFlight. This is used by message types (particularly FPL) to produce the initial flight record when a new flight is added to the state.
class ToFlight (α : Type) where
toFlight : α → Flight
Flight Time Estimation
When full flight information is not yet available, the flight period must be estimated conservatively to ensure messages are not incorrectly discarded.
maxFlightTime
The default maximum flight duration used when the estimated elapsed time is unknown. Set to 20 hours.
def maxFlightTime := Duration.oneHour * 20
maxRoundTripTime
For flights where the departure and destination aerodromes are the same (round trips), a shorter default maximum is used. Set to 6 hours.
def maxRoundTripTime := Duration.oneHour * 6
adepAdesFlightTime
Computes an estimated flight time interval from the departure time, the estimated flight duration (if known), and whether departure equals destination. The calculation doubles the TEET for non-round-trip flights (to allow for late arrivals) and caps against the appropriate maximum.
def adepAdesFlightTime (f13a : Field13a) (f13b : DTG) (f16a : Field16a) : Option Duration → Interval
| none => -- flight duration not known
.intervalOf f13b (if adepIsAdes f13a f16a then maxRoundTripTime else maxFlightTime)
| some teet => -- flight duration known
if adepIsAdes f13a f16a then
.intervalOf f13b (min teet maxRoundTripTime)
else
.intervalOf f13b (min (teet * 2) maxFlightTime)
Flight Status
A flight progresses through a lifecycle, and its current position in that lifecycle is recorded as a status value.
inductive FlightStatus
| filed -- flight plan received and accepted
| airborne -- departure confirmed
| cancelled -- flight plan cancelled
| completed -- arrival confirmed
deriving DecidableEq
| Constructor | Meaning |
|---|
filed | A FPL message has been received and the flight is stored |
airborne | A DEP message has been received confirming departure |
cancelled | A CNL message has been received |
completed | An ARR message has been received confirming arrival |
The Flight Structure
The Flight structure is the central entity of the specification. It accumulates all fields received across the sequence of messages for a flight, plus a lifecycle status. Field 22 is excluded: its sole purpose is to communicate changes, and those changes are incorporated into the other fields when a CHG message is processed.
structure Flight where
status : FlightStatus
f7 : Field7
f8 : Field8
f9 : Field9
f10 : Field10
f13 : Field13
f15 : Field15
f16 : Field16
f17 : Option Field17
f18 : Option Field18
inv : F8F15Level f8 f15 ∧
F8F15Rule f8 f15 ∧
F9F18Typ f9 f18 ∧
F10F18Sts f10 f18 ∧
F10F18Pbn f10 f18 ∧
F10F18Z f10 f18 ∧
F13F18Dep f13 f18 ∧
F15F18Dle f15 f18 ∧
F16F18Dest f16 f18 ∧
F16F18Altn f16 f18 ∧
F16F18Eet f16 f18 ∧
F16F18Dle f16 f18 ∧
F16F17Dest f16.f16a f17 ∧
-- Field 17 is populated if and only if the flight is completed.
f17.isSome ↔ status = .completed
deriving DecidableEq
Fields
| Field | Type | Description |
|---|
status | FlightStatus | Current lifecycle status |
f7 | Field7 | Aircraft identification and optional SSR code |
f8 | Field8 | Flight rules and type of flight |
f9 | Field9 | Aircraft type, formation count, and wake turbulence |
f10 | Field10 | Equipment and capability codes |
f13 | Field13 | Departure aerodrome and time |
f15 | Field15 | Route: initial speed, level, and route elements |
f16 | Field16 | Destination, TEET, and alternate aerodromes |
f17 | Option Field17 | Actual arrival aerodrome and time (present only when status = .completed) |
f18 | Option Field18 | Other information (equipment details, EET, PBN codes, etc.) |
Invariants
The inv field is a conjunction of all cross-field consistency constraints. A value of type Flight is only well-formed when all of the following hold simultaneously:
| Invariant | Constraint |
|---|
F8F15Level | If Field 15 level is absent (VFR), Field 8 rules must be v or z |
F8F15Rule | In-route rule changes in Field 15 are consistent with Field 8 initial rules |
F9F18Typ | Field 9b designator present ↔ Field 18 TYP absent |
F10F18Sts | RVSM capable (w) and NONRVSM status cannot coexist |
F10F18Pbn | PBN capable (r) ↔ Field 18 PBN non-empty |
F10F18Z | z in Field 10a ↔ at least one of Field 18 COM/NAV/DAT populated |
F13F18Dep | Field 13a departure coding consistent with Field 18 DEP |
F15F18Dle | Delay points in Field 18 DLE are named waypoints in the Field 15 route |
F16F18Dest | Field 16a destination coding consistent with Field 18 DEST |
F16F18Altn | ZZZZ entries in Field 16c alternates matched by Field 18 ALTN entries |
F16F18Eet | All EET durations less than total flight duration (Field 16b) |
F16F18Dle | Sum of delay durations less than total flight duration |
F16F17Dest | Planned destination (Field 16a) differs from actual arrival (Field 17a) |
f17 ↔ completed | Field 17 is present if and only if the flight status is completed |
Type Class Instances for Flight
FlightTime Flight
The flight time period for a Flight is computed from the departure point, departure time, destination, and TEET using adepAdesFlightTime.
instance : FlightTime Flight where
period flt := adepAdesFlightTime flt.f13.f13a flt.f13.f13b flt.f16.f16a flt.f16.f16b
IsFlight Flight
The FlightId for a Flight is assembled from the aircraft identification, the departure aerodrome, and the computed flight time period.
instance : IsFlight Flight where
idOf flight := ⟨flight.f7.f7a, flight.f13.f13a, FlightTime.period flight⟩
end FPL
