/-
QSSLProofs.TLSRecord
TLS record layer properties for qssl.
qssl adds a standard TLS record layer (not present in qssh).
Key results:
- record_header_size — 5-byte header
- max_record_size — 16384 = 2^14
- record_types_distinct — all RecordType values are unique
- record_fits_tcp — full wire record fits TCP segment
Mirrors: transport/mod.rs RecordHeader, RecordType.
Tier 3 verification (Kani → Verus → **Lean 4**).
-/
import Mathlib.Tactic.NormNum
import Mathlib.Data.Fintype.Card
namespace QSSLProofs.TLSRecord
/-! ## Constants -/
/-- TLS record header size: type(1) + version(2) + length(2) = 5 bytes. -/
def HEADER_SIZE : ℕ := 5
/-- Maximum TLS record payload size: 2^14 = 16384 bytes. -/
def MAX_RECORD_SIZE : ℕ := 16384
/-- Maximum TLS handshake message size: 2^16 = 65536 bytes. -/
def MAX_HANDSHAKE_SIZE : ℕ := 65536
/-- qssl protocol version identifier. -/
def QSSL_PROTOCOL_VERSION : ℕ := 0x5110
/-- AES-GCM authentication tag size. -/
def GCM_TAG_SIZE : ℕ := 16
/-- AES-GCM nonce/IV size. -/
def GCM_NONCE_SIZE : ℕ := 12
/-! ## Header structure -/
/-- Record header is exactly 5 bytes. -/
theorem record_header_size : HEADER_SIZE = 5 := by rfl
/-- Header decomposes into type(1) + version(2) + length(2). -/
theorem header_decomposition : HEADER_SIZE = 1 + 2 + 2 := by
norm_num [HEADER_SIZE]
/-! ## Record size properties -/
/-- MAX_RECORD_SIZE is exactly 2^14. -/
theorem max_record_size : MAX_RECORD_SIZE = 2 ^ 14 := by
norm_num [MAX_RECORD_SIZE]
/-- MAX_HANDSHAKE_SIZE is exactly 2^16. -/
theorem max_handshake_size : MAX_HANDSHAKE_SIZE = 2 ^ 16 := by
norm_num [MAX_HANDSHAKE_SIZE]
/-- Record length fits in u16: MAX_RECORD_SIZE < 2^16. -/
theorem record_length_fits_u16 : MAX_RECORD_SIZE < 2 ^ 16 := by
norm_num [MAX_RECORD_SIZE]
/-- Maximum handshake fragmentation: MAX_HANDSHAKE_SIZE / MAX_RECORD_SIZE = 4. -/
theorem handshake_needs_records : MAX_HANDSHAKE_SIZE / MAX_RECORD_SIZE = 4 := by
norm_num [MAX_HANDSHAKE_SIZE, MAX_RECORD_SIZE]
/-- Full wire record size: header + payload = 5 + 16384 = 16389. -/
theorem record_with_header : HEADER_SIZE + MAX_RECORD_SIZE = 16389 := by
norm_num [HEADER_SIZE, MAX_RECORD_SIZE]
/-- Full wire record fits TCP segment: 5 + 16384 < 65536. -/
theorem record_fits_tcp : HEADER_SIZE + MAX_RECORD_SIZE < 65536 := by
norm_num [HEADER_SIZE, MAX_RECORD_SIZE]
/-! ## Protocol version -/
/-- qssl protocol version = 0x5110 = 20752. -/
theorem protocol_version : QSSL_PROTOCOL_VERSION = 20752 := by
norm_num [QSSL_PROTOCOL_VERSION]
/-! ## Record type enumeration -/
/-- The four TLS record types used by qssl. -/
inductive RecordType where
| ChangeCipherSpec -- 0x14
| Alert -- 0x15
| Handshake -- 0x16
| ApplicationData -- 0x17
deriving DecidableEq
/-- Numeric code for each record type (standard TLS values). -/
def record_type_code : RecordType → ℕ
| .ChangeCipherSpec => 0x14
| .Alert => 0x15
| .Handshake => 0x16
| .ApplicationData => 0x17
/-- All record type codes are distinct (injective mapping). -/
theorem record_types_distinct : Function.Injective record_type_code := by
intro a b h
cases a <;> cases b <;> simp [record_type_code] at h <;> rfl
/-- There are exactly 4 record types. -/
instance : Fintype RecordType where
elems := {.ChangeCipherSpec, .Alert, .Handshake, .ApplicationData}
complete := by intro x; cases x <;> simp
theorem record_type_count : Fintype.card RecordType = 4 := by
native_decide
/-- Handshake record type = 0x16 = 22. -/
theorem handshake_type_value : record_type_code .Handshake = 22 := by
norm_num [record_type_code]
end QSSLProofs.TLSRecord