# Proven Properties Catalog

> All theorems link to their source modules in the [API Reference](../Hale.html).

**Total: 257 compile-time verified theorems across 52 files**

All theorems are checked by the Lean 4 kernel at compile time. The codebase
is completely `sorry`-free — every proof obligation is fully discharged.

## Algebraic Laws

### Monoid/Semigroup Associativity (8, in `Base/Data/Newtype.lean`)
| Theorem | Module |
|---------|--------|
| `Dual.append_assoc` | Base/Data/Newtype |
| `Endo.append_assoc` | Base/Data/Newtype |
| `First.append_assoc` | Base/Data/Newtype |
| `Last.append_assoc` | Base/Data/Newtype |
| `Sum.append_assoc` | Base/Data/Newtype |
| `Product.append_assoc` | Base/Data/Newtype |
| `All.append_assoc` | Base/Data/Newtype |
| `Any.append_assoc` | Base/Data/Newtype |

### Functor Laws (14)
| Theorem | Module |
|---------|--------|
| `Identity.map_id` | Base/Data/Functor/Identity |
| `Identity.map_comp` | Base/Data/Functor/Identity |
| `Const.map_id` | Base/Data/Functor/Const |
| `Const.map_comp` | Base/Data/Functor/Const |
| `Const.map_val` | Base/Data/Functor/Const |
| `Proxy.map_id` | Base/Data/Proxy |
| `Proxy.map_comp` | Base/Data/Proxy |
| `Either.map_id` | Base/Data/Either |
| `Either.map_comp` | Base/Data/Either |
| `Compose.map_id` | Base/Data/Functor/Compose |
| `Compose.map_comp` | Base/Data/Functor/Compose |
| `Product.map_id` | Base/Data/Functor/Product |
| `Product.map_comp` | Base/Data/Functor/Product |
| `Sum.map_id` | Base/Data/Functor/Sum |
| `Sum.map_comp` | Base/Data/Functor/Sum |

### Monad Laws (9)
| Theorem | Module |
|---------|--------|
| `Identity.pure_bind` | Base/Data/Functor/Identity |
| `Identity.bind_pure` | Base/Data/Functor/Identity |
| `Identity.bind_assoc` | Base/Data/Functor/Identity |
| `Proxy.pure_bind` | Base/Data/Proxy |
| `Proxy.bind_pure` | Base/Data/Proxy |
| `Proxy.bind_assoc` | Base/Data/Proxy |
| `Either.pure_bind` | Base/Data/Either |
| `Either.bind_pure` | Base/Data/Either |
| `Either.bind_assoc` | Base/Data/Either |

### Monad Combinators (1)
| Theorem | Module |
|---------|--------|
| `join_pure` | Base/Control/Monad |

## Data Structure Properties

### Either (3)
| Theorem | Module |
|---------|--------|
| `swap_swap` | Base/Data/Either |
| `isLeft_not_isRight` | Base/Data/Either |
| `partitionEithers_length` | Base/Data/Either |

### Maybe/Option (8)
| Theorem | Module |
|---------|--------|
| `maybe_none` | Base/Data/Maybe |
| `maybe_some` | Base/Data/Maybe |
| `fromMaybe_none` | Base/Data/Maybe |
| `fromMaybe_some` | Base/Data/Maybe |
| `catMaybes_nil` | Base/Data/Maybe |
| `mapMaybe_nil` | Base/Data/Maybe |
| `maybeToList_listToMaybe` | Base/Data/Maybe |
| `catMaybes_eq_mapMaybe_id` | Base/Data/Maybe |

### Tuple (7)
| Theorem | Module |
|---------|--------|
| `swap_swap` | Base/Data/Tuple |
| `curry_uncurry` | Base/Data/Tuple |
| `uncurry_curry` | Base/Data/Tuple |
| `bimap_id` | Base/Data/Tuple |
| `bimap_comp` | Base/Data/Tuple |
| `mapFst_eq_bimap` | Base/Data/Tuple |
| `mapSnd_eq_bimap` | Base/Data/Tuple |

### List (4)
| Theorem | Module |
|---------|--------|
| `tails_length` | Base/Data/List |
| `inits_length` | Base/Data/List |
| `tails_nil` | Base/Data/List |
| `inits_nil` | Base/Data/List |

### NonEmpty (4)
| Theorem | Module |
|---------|--------|
| `toList_ne_nil` | Base/Data/List/NonEmpty |
| `reverse_length` | Base/Data/List/NonEmpty |
| `toList_length` | Base/Data/List/NonEmpty |
| `map_length` | Base/Data/List/NonEmpty |

### Ord/Down (2)
| Theorem | Module |
|---------|--------|
| `get_mk` | Base/Data/Ord |
| `compare_reverse` | Base/Data/Ord |

### Bool (5)
| Theorem | Module |
|---------|--------|
| `bool_false` | Base/Data/Bool |
| `bool_true` | Base/Data/Bool |
| `guard'_true` | Base/Data/Bool |
| `guard'_false` | Base/Data/Bool |
| `bool_ite` | Base/Data/Bool |

### Void (1)
| Theorem | Module |
|---------|--------|
| `eq_absurd` | Base/Data/Void |

### Function (5)
| Theorem | Module |
|---------|--------|
| `on_apply` | Base/Data/Function |
| `applyTo_apply` | Base/Data/Function |
| `const_apply` | Base/Data/Function |
| `flip_flip` | Base/Data/Function |
| `flip_apply` | Base/Data/Function |

### Foldable (2)
| Theorem | Module |
|---------|--------|
| `foldr_nil` | Base/Data/Foldable |
| `foldl_nil` | Base/Data/Foldable |

### String (1)
| Theorem | Module |
|---------|--------|
| `unwords_nil` | Base/Data/String |

### Char (3)
| Theorem | Module |
|---------|--------|
| `isAlphaNum_iff` | Base/Data/Char |
| `isSpace_eq_isWhitespace` | Base/Data/Char |
| `ord_eq_toNat` | Base/Data/Char |

### Ix (1)
| Theorem | Module |
|---------|--------|
| `Ix.inRange_iff_index_isSome_nat` | Base/Data/Ix |

### ExitCode (2)
| Theorem | Module |
|---------|--------|
| `success_toUInt32` | Base/System/Exit |
| `isSuccess_iff` | Base/System/Exit |

## Numeric Type Properties

### Complex (2)
| Theorem | Module |
|---------|--------|
| `conjugate_conjugate` | Base/Data/Complex |
| `add_comm'` | Base/Data/Complex |

### Fixed-Point (5)
| Theorem | Module |
|---------|--------|
| `scale_pos` | Base/Data/Fixed |
| `add_exact` | Base/Data/Fixed |
| `sub_exact` | Base/Data/Fixed |
| `neg_neg` | Base/Data/Fixed |
| `fromInt_zero` | Base/Data/Fixed |

### Time (2)
| Theorem | Module |
|---------|--------|
| `fromSeconds_toSeconds` | Time/Data/Time/Clock |
| `diffUTCTime_self` | Time/Data/Time/Clock |

## Protocol Correctness

### HTTP Method Properties (21, in `HttpTypes/Network/HTTP/Types/Method.lean`)
| Theorem | What it proves |
|---------|---------------|
| `parseMethod_GET` | Parsing "GET" yields `.standard .GET` |
| `parseMethod_POST` | Parsing "POST" yields `.standard .POST` |
| `parseMethod_HEAD` | Parsing "HEAD" yields `.standard .HEAD` |
| `parseMethod_PUT` | Parsing "PUT" yields `.standard .PUT` |
| `parseMethod_DELETE` | Parsing "DELETE" yields `.standard .DELETE` |
| `parseMethod_TRACE` | Parsing "TRACE" yields `.standard .TRACE` |
| `parseMethod_CONNECT` | Parsing "CONNECT" yields `.standard .CONNECT` |
| `parseMethod_OPTIONS` | Parsing "OPTIONS" yields `.standard .OPTIONS` |
| `parseMethod_PATCH` | Parsing "PATCH" yields `.standard .PATCH` |
| `parseMethod_custom` | Non-standard strings yield `.custom` |
| `Method.get_is_safe` | GET is a safe method |
| `Method.head_is_safe` | HEAD is a safe method |
| `Method.options_is_safe` | OPTIONS is a safe method |
| `Method.trace_is_safe` | TRACE is a safe method |
| `Method.post_not_safe` | POST is not safe |
| `Method.patch_not_safe` | PATCH is not safe |
| `Method.put_is_idempotent` | PUT is idempotent |
| `Method.delete_is_idempotent` | DELETE is idempotent |
| `Method.post_not_idempotent` | POST is not idempotent |
| `Method.patch_not_idempotent` | PATCH is not idempotent |
| `Method.safe_implies_idempotent` | All safe methods are idempotent |

### HTTP Status Properties (13, in `HttpTypes/Network/HTTP/Types/Status.lean`)
| Theorem | What it proves |
|---------|---------------|
| `status200_valid` | 200 is in valid range [100, 599] |
| `status404_valid` | 404 is in valid range |
| `status500_valid` | 500 is in valid range |
| `status100_valid` | 100 is in valid range |
| `status301_valid` | 301 is in valid range |
| `status100_no_body` | 100 must not have body |
| `status101_no_body` | 101 must not have body |
| `status204_no_body` | 204 must not have body |
| `status304_no_body` | 304 must not have body |
| `status200_may_have_body` | 200 may have body |
| `status201_may_have_body` | 201 may have body |
| `status404_may_have_body` | 404 may have body |
| `status500_may_have_body` | 500 may have body |

### HTTP Version Properties (4, in `HttpTypes/Network/HTTP/Types/Version.lean`)
| Theorem | What it proves |
|---------|---------------|
| `http09_valid` | HTTP/0.9 has major=0, minor=9 |
| `http10_valid` | HTTP/1.0 has major=1, minor=0 |
| `http11_valid` | HTTP/1.1 has major=1, minor=1 |
| `http20_valid` | HTTP/2.0 has major=2, minor=0 |

### Transport Security (3, in `Warp/Types.lean`)
| Theorem | What it proves |
|---------|---------------|
| `tcp_not_secure` | TCP is not encrypted |
| `tls_is_secure` | TLS is always encrypted |
| `quic_is_secure` | QUIC is always encrypted |

### Keep-Alive Semantics (2, in `Warp/Run.lean`)
| Theorem | What it proves |
|---------|---------------|
| `connAction_http10_default` | HTTP/1.0 defaults to close |
| `connAction_http11_default` | HTTP/1.1 defaults to keep-alive |

### HTTP Version Parsing (5, in `Warp/Request.lean`)
| Theorem | What it proves |
|---------|---------------|
| `parseHttpVersion_http11` | "HTTP/1.1" -> http11 |
| `parseHttpVersion_http10` | "HTTP/1.0" -> http10 |
| `parseHttpVersion_http09` | "HTTP/0.9" -> http09 |
| `parseHttpVersion_http20` | "HTTP/2.0" -> http20 |
| `parseRequestLine_empty` | "" -> none |

### Warp Settings (1, in `Warp/Settings.lean`)
| Theorem | What it proves |
|---------|---------------|
| `defaultSettings_valid` | Default timeout > 0 and backlog > 0 |

## Encoding/Decoding Roundtrips

### HTTP/2 Frame Types (10, in `Http2/Network/HTTP2/Frame/Types.lean`)
| Theorem | Frame Type |
|---------|-----------|
| `fromUInt8_toUInt8_data` | DATA |
| `fromUInt8_toUInt8_headers` | HEADERS |
| `fromUInt8_toUInt8_priority` | PRIORITY |
| `fromUInt8_toUInt8_rstStream` | RST_STREAM |
| `fromUInt8_toUInt8_settings` | SETTINGS |
| `fromUInt8_toUInt8_pushPromise` | PUSH_PROMISE |
| `fromUInt8_toUInt8_ping` | PING |
| `fromUInt8_toUInt8_goaway` | GOAWAY |
| `fromUInt8_toUInt8_windowUpdate` | WINDOW_UPDATE |
| `fromUInt8_toUInt8_continuation` | CONTINUATION |

### HTTP/3 Frame Types (7, in `Http3/Network/HTTP3/Frame.lean`)
| Theorem | Frame Type |
|---------|-----------|
| `FrameType.roundtrip_data` | DATA |
| `FrameType.roundtrip_headers` | HEADERS |
| `FrameType.roundtrip_cancelPush` | CANCEL_PUSH |
| `FrameType.roundtrip_settings` | SETTINGS |
| `FrameType.roundtrip_pushPromise` | PUSH_PROMISE |
| `FrameType.roundtrip_goaway` | GOAWAY |
| `FrameType.roundtrip_maxPushId` | MAX_PUSH_ID |

### HTTP/3 Error Codes (17, in `Http3/Network/HTTP3/Error.lean`)
| Theorem | Error Code |
|---------|-----------|
| `H3Error.roundtrip_noError` | H3_NO_ERROR |
| `H3Error.roundtrip_generalProtocolError` | H3_GENERAL_PROTOCOL_ERROR |
| `H3Error.roundtrip_internalError` | H3_INTERNAL_ERROR |
| `H3Error.roundtrip_streamCreationError` | H3_STREAM_CREATION_ERROR |
| `H3Error.roundtrip_closedCriticalStream` | H3_CLOSED_CRITICAL_STREAM |
| `H3Error.roundtrip_frameUnexpected` | H3_FRAME_UNEXPECTED |
| `H3Error.roundtrip_frameError` | H3_FRAME_ERROR |
| `H3Error.roundtrip_excessiveLoad` | H3_EXCESSIVE_LOAD |
| `H3Error.roundtrip_idError` | H3_ID_ERROR |
| `H3Error.roundtrip_settingsError` | H3_SETTINGS_ERROR |
| `H3Error.roundtrip_missingSettings` | H3_MISSING_SETTINGS |
| `H3Error.roundtrip_requestRejected` | H3_REQUEST_REJECTED |
| `H3Error.roundtrip_requestCancelled` | H3_REQUEST_CANCELLED |
| `H3Error.roundtrip_requestIncomplete` | H3_REQUEST_INCOMPLETE |
| `H3Error.roundtrip_messageError` | H3_MESSAGE_ERROR |
| `H3Error.roundtrip_connectError` | H3_CONNECT_ERROR |
| `H3Error.roundtrip_versionFallback` | H3_VERSION_FALLBACK |

### WebSocket Opcodes (6, in `WebSockets/Types.lean`)
| Theorem | Opcode |
|---------|--------|
| `opcode_roundtrip_text` | TEXT |
| `opcode_roundtrip_binary` | BINARY |
| `opcode_roundtrip_close` | CLOSE |
| `opcode_roundtrip_ping` | PING |
| `opcode_roundtrip_pong` | PONG |
| `opcode_roundtrip_continuation` | CONTINUATION |

## ByteString Properties

### ByteString Invariants (3, in `ByteString/Internal.lean`)
| Theorem | What it proves |
|---------|---------------|
| `take_valid` | `take` result has valid offset/length |
| `drop_valid` | `drop` result has valid offset/length |
| `null_iff_length_zero` | `null bs <-> length bs = 0` |

### Builder Monoid (3, in `ByteString/Builder.lean`)
| Theorem | What it proves |
|---------|---------------|
| `empty_append` | `empty ++ b = b` (left identity) |
| `append_empty` | `b ++ empty = b` (right identity) |
| `append_assoc` | `(a ++ b) ++ c = a ++ (b ++ c)` (associativity) |

### Short ByteString (1, in `ByteString/Short.lean`)
| Theorem | What it proves |
|---------|---------------|
| `length_toShort` | `toShort` preserves length |

## Word8 Properties (4, in `Word8/Data/Word8.lean`)
| Theorem | What it proves |
|---------|---------------|
| `toLower_idempotent` | `toLower . toLower = toLower` |
| `toUpper_idempotent` | `toUpper . toUpper = toUpper` |
| `isUpper_toLower` | Upper -> toLower -> isLower |
| `isLower_toUpper` | Lower -> toUpper -> isUpper |

## CaseInsensitive (1, in `CaseInsensitive/Data/CaseInsensitive.lean`)
| Theorem | What it proves |
|---------|---------------|
| `ci_eq_iff` | CI equality is by foldedCase |

## Socket State (11, in `Network/Socket/Types.lean`)
| Theorem | What it proves |
|---------|---------------|
| `SocketState.fresh_ne_bound` | fresh /= bound |
| `SocketState.fresh_ne_listening` | fresh /= listening |
| `SocketState.fresh_ne_connected` | fresh /= connected |
| `SocketState.fresh_ne_closed` | fresh /= closed |
| `SocketState.bound_ne_listening` | bound /= listening |
| `SocketState.bound_ne_connected` | bound /= connected |
| `SocketState.bound_ne_closed` | bound /= closed |
| `SocketState.listening_ne_connected` | listening /= connected |
| `SocketState.listening_ne_closed` | listening /= closed |
| `SocketState.connected_ne_closed` | connected /= closed |
| `SocketState.beq_refl` | s == s = true |

## Response Lifecycle (1, in `WAI/Network/Wai/Internal.lean`)
| Theorem | What it proves |
|---------|---------------|
| `ResponseState.pending_ne_sent` | pending /= sent |

## Path Safety (4, in `WaiAppStatic/Types.lean`)
| Theorem | What it proves |
|---------|---------------|
| `empty_piece_valid` | Empty string is a valid piece |
| `toPiece_rejects_dot` | Dotfiles rejected at construction |
| `toPiece_rejects_slash` | Path traversal rejected at construction |
| `toPiece_accepts_simple` | Normal filenames accepted |

## WAI Response Laws (11, in `WAI/Internal.lean`)
| Theorem | What it proves |
|---------|---------------|
| `status_responseBuilder` | Status accessor on builder |
| `status_responseFile` | Status accessor on file |
| `status_responseStream` | Status accessor on stream |
| `headers_responseBuilder` | Headers accessor on builder |
| `headers_responseFile` | Headers accessor on file |
| `mapResponseHeaders_id_responseBuilder` | `mapHeaders id` on builder = id |
| `mapResponseHeaders_id_responseFile` | `mapHeaders id` on file = id |
| `mapResponseHeaders_id_responseStream` | `mapHeaders id` on stream = id |
| `mapResponseStatus_id_responseBuilder` | `mapStatus id` on builder = id |
| `mapResponseStatus_id_responseFile` | `mapStatus id` on file = id |
| `mapResponseStatus_id_responseStream` | `mapStatus id` on stream = id |

## WAI Middleware Algebra (5, in `WAI/Wai.lean`)
| Theorem | What it proves |
|---------|---------------|
| `idMiddleware_comp_left` | `id . m = m` |
| `idMiddleware_comp_right` | `m . id = m` |
| `modifyRequest_id` | `modifyRequest id = id` |
| `modifyResponse_id` | `modifyResponse id = id` |
| `ifRequest_false` | `ifRequest (always false) m = id` |

## Middleware Properties (11)

### AddHeaders (3, in `WaiExtra/AddHeaders.lean`)
| Theorem | What it proves |
|---------|---------------|
| `addHeaders_nil_builder` | Empty headers on builder = identity |
| `addHeaders_nil_file` | Empty headers on file = identity |
| `addHeaders_nil_stream` | Empty headers on stream = identity |

### StripHeaders (3, in `WaiExtra/StripHeaders.lean`)
| Theorem | What it proves |
|---------|---------------|
| `stripHeaders_nil_builder` | Empty strip list on builder = identity |
| `stripHeaders_nil_file` | Empty strip list on file = identity |
| `stripHeaders_nil_stream` | Empty strip list on stream = identity |

### Select (1, in `WaiExtra/Select.lean`)
| Theorem | What it proves |
|---------|---------------|
| `select_none` | Always-none = identity |

### Routed (2, in `WaiExtra/Routed.lean`)
| Theorem | What it proves |
|---------|---------------|
| `routed_true` | Always-true = apply middleware |
| `routed_false` | Always-false = identity |

### ForceSSL (1, in `WaiExtra/ForceSSL.lean`)
| Theorem | What it proves |
|---------|---------------|
| `forceSSL_secure` | Secure requests pass through |

### HealthCheck (1, in `WaiExtra/HealthCheckEndpoint.lean`)
| Theorem | What it proves |
|---------|---------------|
| `healthCheck_passthrough` | Non-matching paths pass through |

## ResourceT (1, in `ResourceT/Resource.lean`)
| Theorem | What it proves |
|---------|---------------|
| `releaseKey_eq` | `a = b <-> a.id = b.id` |

## Involution/Self-Inverse Properties (Summary)
| Theorem | Module |
|---------|--------|
| `swap_swap` (Tuple) | Base/Data/Tuple |
| `swap_swap` (Either) | Base/Data/Either |
| `conjugate_conjugate` | Base/Data/Complex |
| `flip_flip` | Base/Data/Function |
| `curry_uncurry` | Base/Data/Tuple |
| `neg_neg` (Fixed) | Base/Data/Fixed |
| `toLower_idempotent` | Word8/Data/Word8 |
| `toUpper_idempotent` | Word8/Data/Word8 |

## Proof-Carrying Structures (Invariants by Construction)
These are not standalone theorems but proof fields embedded in structures,
enforced at construction time and erased at runtime:

| Structure | Proof Field | Invariant |
|-----------|-------------|-----------|
| `Ratio` | `den_pos` | Denominator > 0 |
| `Ratio` | `coprime` | Num and den are coprime |
| `Piece` | `no_dot` | No leading dot |
| `Piece` | `no_slash` | No embedded slash |
| `Settings` | `settingsTimeoutPos` | Timeout > 0 |
| `Settings` | `settingsBacklogPos` | Backlog > 0 |
| `Socket` | `state` (phantom) | Socket state machine |