inductive PostgREST.Config.LogLevel : Type

Logging verbosity level, ordered from most critical to most verbose. $$\text{LogLevel} \in \{ \text{crit}, \text{error}, \text{warn}, \text{info}, \text{debug} \}$$

• crit : LogLevel
• error : LogLevel
• warn : LogLevel
• info : LogLevel
• debug : LogLevel

@[implicit_reducible]

instance PostgREST.Config.instBEqLogLevel : BEq LogLevel

Equations

• PostgREST.Config.instBEqLogLevel = { beq := PostgREST.Config.instBEqLogLevel.beq }

def PostgREST.Config.instBEqLogLevel.beq : LogLevel → LogLevel → Bool

Equations

• PostgREST.Config.instBEqLogLevel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def PostgREST.Config.instReprLogLevel.repr : LogLevel → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance PostgREST.Config.instReprLogLevel : Repr LogLevel

Equations

• PostgREST.Config.instReprLogLevel = { reprPrec := PostgREST.Config.instReprLogLevel.repr }

@[implicit_reducible]

instance PostgREST.Config.instInhabitedLogLevel : Inhabited LogLevel

Equations

• PostgREST.Config.instInhabitedLogLevel = { default := PostgREST.Config.instInhabitedLogLevel.default }

def PostgREST.Config.instInhabitedLogLevel.default : LogLevel

Equations

• PostgREST.Config.instInhabitedLogLevel.default = PostgREST.Config.LogLevel.crit

@[implicit_reducible]

instance PostgREST.Config.instDecidableEqLogLevel : DecidableEq LogLevel

Equations

• PostgREST.Config.instDecidableEqLogLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance PostgREST.Config.instToStringLogLevel : ToString LogLevel

Equations

• One or more equations did not get rendered due to their size.

def PostgREST.Config.LogLevel.parse (s : String) : Option LogLevel

Parse a log level from a string (case-insensitive).

Equations

• One or more equations did not get rendered due to their size.

inductive PostgREST.Config.OpenAPIMode : Type

OpenAPI specification generation mode. $$\text{OpenAPIMode} \in \{ \text{followPriv}, \text{ignorePriv}, \text{disabled}, \text{securityNone} \}$$

• followPriv: respect database privileges in the spec
• ignorePriv: expose all endpoints regardless of privileges
• disabled: do not serve the OpenAPI spec
• securityNone: serve spec with no security definitions

• followPriv : OpenAPIMode
• ignorePriv : OpenAPIMode
• disabled : OpenAPIMode
• securityNone : OpenAPIMode

def PostgREST.Config.instBEqOpenAPIMode.beq : OpenAPIMode → OpenAPIMode → Bool

Equations

• PostgREST.Config.instBEqOpenAPIMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance PostgREST.Config.instBEqOpenAPIMode : BEq OpenAPIMode

Equations

• PostgREST.Config.instBEqOpenAPIMode = { beq := PostgREST.Config.instBEqOpenAPIMode.beq }

def PostgREST.Config.instReprOpenAPIMode.repr : OpenAPIMode → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance PostgREST.Config.instReprOpenAPIMode : Repr OpenAPIMode

Equations

• PostgREST.Config.instReprOpenAPIMode = { reprPrec := PostgREST.Config.instReprOpenAPIMode.repr }

@[implicit_reducible]

instance PostgREST.Config.instDecidableEqOpenAPIMode : DecidableEq OpenAPIMode

Equations

• PostgREST.Config.instDecidableEqOpenAPIMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance PostgREST.Config.instToStringOpenAPIMode : ToString OpenAPIMode

Equations

• One or more equations did not get rendered due to their size.

def PostgREST.Config.OpenAPIMode.parse (s : String) : Option OpenAPIMode

Parse an OpenAPI mode from a string.

Equations

• One or more equations did not get rendered due to their size.

structure PostgREST.Config.Port : Type

A valid TCP/UDP port number: 1 through 65535. $$\text{Port} = \{ n : \mathbb{N} \mid 0 < n \land n \leq 65535 \}$$ The proof field is erased at runtime (zero cost).

• val : Nat

  The numeric port value.

• port_valid : 0 < self.val ∧ self.val ≤ 65535

  Proof that the port is in the valid range.

def PostgREST.Config.instReprPort.repr : Port → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance PostgREST.Config.instReprPort : Repr Port

Equations

• PostgREST.Config.instReprPort = { reprPrec := PostgREST.Config.instReprPort.repr }

@[implicit_reducible]

instance PostgREST.Config.instBEqPort : BEq Port

Equations

• PostgREST.Config.instBEqPort = { beq := fun (a b : PostgREST.Config.Port) => a.val == b.val }

@[implicit_reducible]

instance PostgREST.Config.instToStringPort : ToString Port

Equations

• PostgREST.Config.instToStringPort = { toString := fun (p : PostgREST.Config.Port) => toString p.val }

@[inline]

def PostgREST.Config.mkPort (n : Nat) (h : 0 < n ∧ n ≤ 65535 := by omega) : Port

Create a port from a literal. $$\text{mkPort} : \{ n : \mathbb{N} \mid 0 < n \leq 65535 \} \to \text{Port}$$

Equations

• PostgREST.Config.mkPort n h = { val := n, port_valid := h }

structure PostgREST.Config.AppConfig : Type

The main PostgREST application configuration. $$\text{AppConfig} = \{ \text{dbUri} : \text{String},\; \text{dbSchemas} : [\text{Schema}],\; \text{anonRole} : \text{String},\; \ldots \}$$

Each field corresponds to a PostgREST configuration option (e.g., PGRST_DB_URI, PGRST_DB_SCHEMAS).

Typing guarantees

• configServerPort is a valid TCP port (1-65535) by construction
• configDbPoolSize is positive by proof field
• configDbSchemas is non-empty by proof field

• configDbUri : String

  PostgreSQL connection URI (e.g., postgresql://user:pass@host/db).

• configDbSchemas : List SchemaCache.Identifiers.Schema

  Schemas to expose via the API (e.g., ["public"]).

• configDbSchemas_nonempty : self.configDbSchemas.length > 0

  Proof that at least one schema is configured. A PostgREST instance with no schemas cannot serve any requests.

• configDbExtraSearchPath : List SchemaCache.Identifiers.Schema

  Additional schemas to add to the search path.

• configDbAnonRole : String

  The PostgreSQL role for unauthenticated requests.

• configDbPreparedStatements : Bool

  Whether to use prepared statements for queries.

• configDbMaxRows : Option Nat

  Maximum number of rows returned by any request (none = unlimited).

• configDbPreRequest : Option SchemaCache.Identifiers.QualifiedIdentifier

  A function to call before every request (for row-level security setup).

• configDbRootSpec : Option SchemaCache.Identifiers.QualifiedIdentifier

  Root spec: a function that serves as the API root (/).

• configDbTxAllowOverride : Bool

  Whether clients can override the transaction mode via headers.

• configDbTxRollbackAll : Bool

  Whether to rollback all transactions (useful for testing).

• configDbPoolSize : Nat

  Connection pool size.

• configDbPoolSize_pos : self.configDbPoolSize > 0

  Proof that the pool size is positive (a zero-size pool is useless).

• configDbPoolMaxIdleTime : Nat

  Maximum idle time (seconds) before a pooled connection is closed.

• configDbPoolMaxLifetime : Nat

  Maximum lifetime (seconds) for a pooled connection.

• configJwtSecret : Option String

  JWT secret for token verification.

• configJwtSecretIsBase64 : Bool

  Whether the JWT secret is base64-encoded.

• configJwtAudience : Option String

  Expected JWT audience claim.

• configJwtRoleClaimKey : String

  JSON path to the role claim in the JWT (e.g., .role).

• configOpenApiMode : OpenAPIMode

  OpenAPI specification generation mode.

• configOpenApiServerProxyUri : Option String

  Proxy URI for the OpenAPI server URL.

• configServerHost : String

  Server bind address (!4 = all IPv4, !6 = all IPv6).

• configServerPort : Port

  Server listen port (valid TCP port: 1-65535).

• configServerUnixSocket : Option String

  Unix domain socket path (alternative to TCP).

• configServerUnixSocketMode : Nat

  File mode for the Unix domain socket.

• configAdminServerPort : Option Port

  Admin server port (for health checks and metrics).

• configLogLevel : LogLevel

  Logging verbosity level.

• configCorsAllowedOrigins : Option (List String)

  Allowed CORS origins (none = allow all).

• configRawMediaTypes : List String

  Additional raw media types to accept.

@[implicit_reducible]

instance PostgREST.Config.instReprAppConfig : Repr AppConfig

Equations

• PostgREST.Config.instReprAppConfig = { reprPrec := PostgREST.Config.instReprAppConfig.repr }

def PostgREST.Config.instReprAppConfig.repr : AppConfig → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def PostgREST.Config.AppConfig.default : AppConfig

A default configuration suitable for local development and testing. Uses postgresql://localhost/postgres with the public schema.

Equations

• One or more equations did not get rendered due to their size.

def PostgREST.Config.AppConfig.hasJwtSecret (c : AppConfig) : Bool

Whether JWT authentication is configured.

Equations

• c.hasJwtSecret = c.configJwtSecret.isSome

def PostgREST.Config.AppConfig.hasAdminServer (c : AppConfig) : Bool

Whether the admin server is enabled.

Equations

• c.hasAdminServer = c.configAdminServerPort.isSome

def PostgREST.Config.AppConfig.hasRootSpec (c : AppConfig) : Bool

Whether the API has a root spec function.

Equations

• c.hasRootSpec = c.configDbRootSpec.isSome

def PostgREST.Config.AppConfig.hasPreRequest (c : AppConfig) : Bool

Whether the API has a pre-request function.

Equations

• c.hasPreRequest = c.configDbPreRequest.isSome

def PostgREST.Config.AppConfig.mainSchema (c : AppConfig) : SchemaCache.Identifiers.Schema

The first schema in the exposed schemas list (used as default). Guaranteed to succeed because configDbSchemas is proven non-empty.

Equations

• c.mainSchema = match h : c.configDbSchemas with | s :: tail => s | [] => absurd ⋯ ⋯

theorem PostgREST.Config.LogLevel.parse_toString_roundtrip (l : LogLevel) : parse (toString l) = some l

LogLevel.parse roundtrips toString for every log level. $$\forall l,\; \text{LogLevel.parse}(\text{toString}(l)) = \text{some}\ l$$

theorem PostgREST.Config.OpenAPIMode.parse_toString_roundtrip (m : OpenAPIMode) : parse (toString m) = some m

OpenAPIMode.parse roundtrips toString for every mode. $$\forall m,\; \text{OpenAPIMode.parse}(\text{toString}(m)) = \text{some}\ m$$