First slice: the NTP packet (RFC 5905, RFC 7822), read, written and proved (bar v2)

.github/workflows/bar.yml

@@ -0,0 +1,21 @@
+name: verified bar
+
+on:
+  push:
+  pull_request:
+  # Rerun when the spec reviewer approves, or an approval is dismissed.
+  pull_request_review:
+    types: [submitted, dismissed]
+
+jobs:
+  bar:
+    # pull-requests: read lets the check confirm the spec approval on GitHub.
+    permissions:
+      contents: read
+      pull-requests: read
+    # Both lines pin the same commit of Proven-Commons/mission: bar v2, as
+    # proposed in its pull request #2. Move both to a release tag once
+    # mission publishes one.
+    uses: Proven-Commons/mission/.github/workflows/verified-bar.yml@6ba85c27abaaf07905c9316aa96dc29f7b5847a2
+    with:
+      bar-ref: 6ba85c27abaaf07905c9316aa96dc29f7b5847a2

.gitignore

@@ -1 +1,3 @@
 .lake/
+__pycache__/
+tests/ntpd-rs/target/

Main.lean

@@ -0,0 +1,171 @@
+/-
+  Command line front end.
+
+    ntp serve
+
+  answers requests on standard input, one per line, for the
+  differential tests. Octets are lower-case hex digits, two per octet,
+  and an empty list of octets is written `-`. Numbers are decimal, and
+  a signed one may start with `-`.
+
+    decode HEX          prints  OK and the packet, or FAIL      (decode)
+    encode PACKET       prints  OK and the hex of the octets that
+                                `encode` writes for the packet, when
+                                `decode` reads the packet back from
+                                them, or FAIL                   (encode, decode)
+    unix ERA RAW        prints  OK, the seconds and the fraction of
+                                the Unix time of the timestamp RAW in
+                                era ERA, or FAIL                (toUnix)
+    fromunix S F        prints  OK, the era and the timestamp of the
+                                Unix time S + F / 2^32 seconds,
+                                or FAIL                         (fromUnix)
+
+  A packet is written as 15 fields, separated by spaces:
+    - LI, VN, Mode, Stratum, Poll, Precision, Root Delay, Root
+      Dispersion, Reference ID, and the Reference, Origin, Receive and
+      Transmit Timestamps, in decimal: Poll and Precision as signed
+      numbers, the others as the unsigned number their bits hold;
+    - the extension fields: `-` when there are none, or else each one
+      as its Field Type in decimal, `:` and the hex of its Value and
+      Padding (`-` when empty), separated by commas;
+    - the hex of the MAC, or `-` when there is none.
+  `decode` prints a packet this way, and `encode` reads one. By
+  `Spec.decode_encode`, `encode` prints OK exactly when the packet it
+  is given is valid.
+
+  A malformed request prints `error`: an unknown operation, the wrong
+  number of fields, hex digits that are not in pairs or not lower case,
+  or a number that is not decimal. A request line may end in LF or
+  CR LF.
+
+  Every answer comes from the proved functions in `Ntp/`. The hex
+  coding, the output and the request handling here are covered by the
+  tests, not by a proof.
+-/
+
+import Ntp
+
+open Ntp Spec
+
+def hexValue (c : Char) : Option Nat :=
+  if '0' ≤ c ∧ c ≤ '9' then some (c.toNat - '0'.toNat)
+  else if 'a' ≤ c ∧ c ≤ 'f' then some (c.toNat - 'a'.toNat + 10)
+  else none
+
+/-- Octets from hex digits in pairs. Tail recursive, so that long
+    inputs do not use the stack. -/
+def hexBytes (cs : List Char) (acc : Array UInt8) : Option (Array UInt8) :=
+  match cs with
+  | [] => some acc
+  | a :: b :: rest =>
+    match hexValue a, hexValue b with
+    | some hi, some lo => hexBytes rest (acc.push (hi * 16 + lo).toUInt8)
+    | _, _ => none
+  | [_] => none
+
+/-- The octets a field gives: `-` for none, else hex digits in pairs. -/
+def fromHex (f : String) : Option (List UInt8) :=
+  if f = "-" then some [] else if f.isEmpty then none else (hexBytes f.toList #[]).map (·.toList)
+
+def hexDigit (n : Nat) : Char :=
+  if n < 10 then Char.ofNat ('0'.toNat + n) else Char.ofNat ('a'.toNat + n - 10)
+
+/-- A field for a list of octets: `-` when it is empty. -/
+def toHex (bs : List UInt8) : String :=
+  if bs.isEmpty then "-"
+  else String.ofList (bs.flatMap fun b => [hexDigit (b.toNat / 16), hexDigit (b.toNat % 16)])
+
+/-- A decimal number, without sign or leading `+`. -/
+def decimal (s : String) : Option Nat :=
+  if !s.isEmpty && s.all Char.isDigit then s.toNat? else none
+
+/-- A decimal number, with `-` in front when it is negative. -/
+def integer (s : String) : Option Int :=
+  match s.toList with
+  | '-' :: cs => (decimal (String.ofList cs)).map fun n => -(n : Int)
+  | _ => (decimal s).map fun n => (n : Int)
+
+def showField (e : ExtField) : String := s!"{e.type}:{toHex e.body}"
+
+def showPacket (p : Packet) : String :=
+  let h := p.header
+  let exts := if p.exts.isEmpty then "-" else ",".intercalate (p.exts.map showField)
+  " ".intercalate [toString h.leap, toString h.version, toString h.mode, toString h.stratum,
+    toString h.poll, toString h.precision, toString h.rootDelay, toString h.rootDispersion,
+    toString h.refId, toString h.reference, toString h.origin, toString h.receive,
+    toString h.transmit, exts, toHex p.mac]
+
+def readField (s : String) : Option ExtField :=
+  match s.splitOn ":" with
+  | [t, b] => do
+    let type ← decimal t
+    let body ← fromHex b
+    pure { type, body }
+  | _ => none
+
+def readFieldList (s : String) : Option (List ExtField) :=
+  if s = "-" then some [] else (s.splitOn ",").mapM readField
+
+/-- A packet written as `showPacket` writes one. -/
+def readPacket : List String → Option Packet
+  | [l, v, m, st, po, pr, rd, rs, ri, rt, ot, vt, xt, es, mac] => do
+    let header : Header :=
+      { leap := ← decimal l, version := ← decimal v, mode := ← decimal m,
+        stratum := ← decimal st, poll := ← integer po, precision := ← integer pr,
+        rootDelay := ← decimal rd, rootDispersion := ← decimal rs, refId := ← decimal ri,
+        reference := ← decimal rt, origin := ← decimal ot, receive := ← decimal vt,
+        transmit := ← decimal xt }
+    let exts ← readFieldList es
+    let mac ← fromHex mac
+    pure { header, exts, mac }
+  | _ => none
+
+/-- The answer to one request line, or `none` when it is malformed. -/
+def request (line : String) : Option String :=
+  match line.splitOn " " with
+  | ["decode", h] => do
+    let b ← fromHex h
+    pure (match decode b with
+      | some p => s!"OK {showPacket p}"
+      | none => "FAIL")
+  | "encode" :: fields => do
+    let p ← readPacket fields
+    let b := encode p
+    pure (if decode b = some p then s!"OK {toHex b}" else "FAIL")
+  | ["unix", e, r] => do
+    let era ← integer e
+    let raw ← decimal r
+    pure (match toUnix era raw with
+      | some (s, f) => s!"OK {s} {f}"
+      | none => "FAIL")
+  | ["fromunix", s, f] => do
+    let seconds ← integer s
+    let fraction ← decimal f
+    pure (match fromUnix seconds fraction with
+      | some (era, raw) => s!"OK {era} {raw}"
+      | none => "FAIL")
+  | _ => none
+
+/-- A request line without its line ending, LF or CR LF. -/
+def chomp (line : String) : String :=
+  let cs := line.toList
+  if cs.getLast? = some '\n' then
+    let cs := cs.dropLast
+    String.ofList (if cs.getLast? = some '\r' then cs.dropLast else cs)
+  else line
+
+def serve : IO Unit := do
+  let stdin ← IO.getStdin
+  let stdout ← IO.getStdout
+  repeat
+    let line ← stdin.getLine
+    if line.isEmpty then break
+    stdout.putStrLn ((request (chomp line)).getD "error")
+    stdout.flush
+
+def usage : String := "usage: ntp serve"
+
+def main (args : List String) : IO UInt32 := do
+  match args with
+  | ["serve"] => serve; return 0
+  | _ => IO.eprintln usage; return 2

Ntp.lean

@@ -0,0 +1,2 @@
+import Ntp.Packet
+import Ntp.Time

Ntp/Packet.lean

@@ -0,0 +1,130 @@
+/-
+  Reading and writing the NTP packet: the 48-octet header of RFC 5905,
+  then extension fields (RFC 7822) and a MAC. The structures the reader
+  gives back are those of `Spec/Defs.lean`; the functions here are the
+  code under proof, and share nothing else with the specification.
+-/
+
+import Spec.Defs
+
+namespace Ntp
+
+open Spec (Header ExtField Packet)
+
+/-! ## Octets -/
+
+/-- Splits off the first `w` octets, if there are that many. Looks at
+    no more than those `w`. -/
+def take? (w : Nat) (b : List UInt8) : Option (List UInt8 × List UInt8) :=
+  let c := b.take w
+  if c.length = w then some (c, b.drop w) else none
+
+/-- The octets as a big-endian unsigned integer. -/
+def bigEndian (bs : List UInt8) : Nat :=
+  bs.foldl (fun n b => n * 256 + b.toNat) 0
+
+/-- A `w`-octet big-endian integer at the start of the input, and the
+    rest. -/
+def readBE (w : Nat) (b : List UInt8) : Option (Nat × List UInt8) :=
+  (take? w b).map fun (c, r) => (bigEndian c, r)
+
+/-- `n` as `w` octets, most significant first. -/
+def writeBE : Nat → Nat → List UInt8
+  | 0, _ => []
+  | w + 1, n => writeBE w (n / 256) ++ [(n % 256).toUInt8]
+
+/-- An octet read as an 8-bit two's complement integer. -/
+def toSigned (n : Nat) : Int :=
+  if n < 128 then n else (n : Int) - 256
+
+/-- An 8-bit two's complement integer as an octet. -/
+def ofSigned (z : Int) : Nat :=
+  if z < 0 then (z + 256).toNat else z.toNat
+
+/-- Whether the list has more than `n` elements. Looks at no more than
+    `n + 1` of them. -/
+def longer : Nat → List UInt8 → Bool
+  | _, [] => false
+  | 0, _ :: _ => true
+  | n + 1, _ :: t => longer n t
+
+/-! ## Reading -/
+
+/-- The 48-octet header at the start of the input, and the rest. The
+    first octet holds LI in its top two bits, then VN in three, then
+    Mode in three. Only versions 3 and 4 and modes 1 to 5 are read. -/
+def readHeader (b : List UInt8) : Option (Header × List UInt8) := do
+  let (lvm, r) ← readBE 1 b
+  let version := lvm / 8 % 8
+  let mode := lvm % 8
+  guard ((version == 3 || version == 4) && 1 ≤ mode && mode ≤ 5)
+  let (stratum, r) ← readBE 1 r
+  let (poll, r) ← readBE 1 r
+  let (precision, r) ← readBE 1 r
+  let (rootDelay, r) ← readBE 4 r
+  let (rootDispersion, r) ← readBE 4 r
+  let (refId, r) ← readBE 4 r
+  let (reference, r) ← readBE 8 r
+  let (origin, r) ← readBE 8 r
+  let (receive, r) ← readBE 8 r
+  let (transmit, r) ← readBE 8 r
+  pure ({ leap := lvm / 64, version, mode, stratum, poll := toSigned poll,
+          precision := toSigned precision, rootDelay, rootDispersion, refId, reference,
+          origin, receive, transmit }, r)
+
+/-- Whether what is left after the header and the extension fields is
+    no MAC, or a MAC of a 4-octet key identifier and a 16- or 20-octet
+    digest. -/
+def macLength (t : List UInt8) : Bool :=
+  t.length == 0 || t.length == 20 || t.length == 24
+
+/-- The extension fields of a version 4 packet and its MAC, from the
+    octets after the header. While more than 24 octets are left, they
+    start with a field: a 16-bit Field Type, a 16-bit Length that counts
+    the whole field, at least 16 and a multiple of 4, then the rest of
+    the field. What is left after the last field is the MAC. `fuel`
+    bounds the number of fields. -/
+def readFields : Nat → List UInt8 → Option (List ExtField × List UInt8)
+  | 0, _ => none
+  | fuel + 1, t =>
+    if longer 24 t then do
+      let (type, r) ← readBE 2 t
+      let (len, r) ← readBE 2 r
+      guard (16 ≤ len && len % 4 == 0)
+      let (body, r) ← take? (len - 4) r
+      let (fields, mac) ← readFields fuel r
+      pure ({ type, body } :: fields, mac)
+    else if macLength t then some ([], t) else none
+
+/-- The extension fields and the MAC after the header. Four zero octets
+    are a crypto-NAK. Otherwise a version 4 packet has fields and then a
+    MAC, and a version 3 packet a MAC only. -/
+def readTail (version : Nat) (t : List UInt8) : Option (List ExtField × List UInt8) :=
+  if t = [0, 0, 0, 0] then some ([], t)
+  else if version = 4 then readFields (t.length + 1) t
+  else if macLength t then some ([], t)
+  else none
+
+/-- The packet in one UDP payload, or `none` when the payload is not a
+    packet this reader accepts. -/
+def decode (b : List UInt8) : Option Packet := do
+  let (header, t) ← readHeader b
+  let (exts, mac) ← readTail header.version t
+  pure { header, exts, mac }
+
+/-! ## Writing -/
+
+/-- An extension field as its octets. -/
+def writeField (e : ExtField) : List UInt8 :=
+  writeBE 2 e.type ++ writeBE 2 (e.body.length + 4) ++ e.body
+
+/-- A packet as its octets. -/
+def encode (p : Packet) : List UInt8 :=
+  let h := p.header
+  writeBE 1 (h.leap * 64 + h.version * 8 + h.mode) ++ writeBE 1 h.stratum ++
+  writeBE 1 (ofSigned h.poll) ++ writeBE 1 (ofSigned h.precision) ++
+  writeBE 4 h.rootDelay ++ writeBE 4 h.rootDispersion ++ writeBE 4 h.refId ++
+  writeBE 8 h.reference ++ writeBE 8 h.origin ++ writeBE 8 h.receive ++ writeBE 8 h.transmit ++
+  p.exts.flatMap writeField ++ p.mac
+
+end Ntp

Ntp/Time.lean

@@ -0,0 +1,29 @@
+/-
+  NTP timestamps and Unix time. A timestamp is 32 bits of seconds and 32
+  bits of fraction since the start of its era (RFC 5905 section 6); the
+  era is not in the packet, so it is an argument here.
+-/
+
+namespace Ntp
+
+/-- The Unix time of the 64-bit timestamp `raw` in era `era`, as whole
+    seconds and a fraction in units of 2^-32 seconds; `none` for the raw
+    value 0, which means unknown, and for a value of more than 64 bits.
+    The seconds are `era * 2^32` plus the seconds field, less the
+    2,208,988,800 seconds from 1900 to 1970. -/
+def toUnix (era : Int) (raw : Nat) : Option (Int × Nat) :=
+  if raw = 0 ∨ 18446744073709551616 ≤ raw then none
+  else some (era * 4294967296 + (raw / 4294967296 : Nat) - 2208988800, raw % 4294967296)
+
+/-- The era and the 64-bit timestamp of a Unix time, given as whole
+    seconds and a fraction in units of 2^-32 seconds; `none` when the
+    fraction is not below 2^32, and at the first instant of an era,
+    whose timestamp would be 0, the value that means unknown. -/
+def fromUnix (seconds : Int) (fraction : Nat) : Option (Int × Nat) :=
+  if 4294967296 ≤ fraction then none
+  else
+    let s := seconds + 2208988800
+    let raw := (s % 4294967296).toNat * 4294967296 + fraction
+    if raw = 0 then none else some (s / 4294967296, raw)
+
+end Ntp

Proofs.lean

@@ -0,0 +1,6 @@
+import Proofs.Bytes
+import Proofs.Header
+import Proofs.Tail
+import Proofs.Packet
+import Proofs.Time
+import Proofs.Main