Overview🔗

This section applies the principles from module 1 through semantic types, proof-bearing values, phantom tags, and abstract models. Each pattern states which distinctions or properties its types enforce, and which claims require additional proofs.

2.1 Semantic Types (Typed Decoding Boundaries)🔗

Pattern: Every semantic distinction claimed to be enforced by Lean MUST be represented in the types or constructors used by the interface. State whether the representation restricts the possible values or makes a particular cross-use ill-typed. Meaning that exists only in strings or other shared primitive values is not a type-level distinction.

Rationale: When two semantic domains use the same String type, Lean accepts either value wherever a String is expected. A decoder can distinguish them by returning a domain-specific type. An enumeration serves a different purpose: its constructors restrict the vocabulary, but remain values of the same type.

Implementation Strategy:

1. Identify the distinctions the interface claims to enforce.

2. Use an enumeration for a closed vocabulary; use distinct types, indices, or refinements when the interface must reject particular cross-use. The enumeration alone does not establish that an operation is authorized.

3. Use smart constructors where validation is needed.

4. Decode raw strings into the semantic type at admission, and require that type downstream. Treat the decoder as the place where you establish validation. A result type alone does not specify how the decoder interprets, rejects, or normalizes input; claimed behavior needs a contract about that decoder (§3.7).

Example - Entity Roles:

All four constructors have type EntityRole. The type restricts role values to that vocabulary; the functions compute permission decisions. An operation requiring permission must either enforce that decision or require corresponding proof evidence. The enumeration alone does not prevent an unauthorized operation.

Anti-Pattern to Avoid when the interface claims role distinctions are type-enforced (this implementation elaborates, but its behavior depends on an unconstrained String rather than the closed EntityRole constructors, so the claimed type boundary does not exist):

2.2 Dependent Types for Invariants🔗

Pattern: Use dependent types, including Subtype (written {x : T // P x}), to bundle values with proofs. A subtype adds the predicate P to the underlying type T. Every value supplies evidence of that predicate, and the interface should state when later use depends on that evidence.

Rationale: Every value of {p : Rat // 0 ≤ p ∧ p ≤ 1} supplies a rational number and a proof of its bounds. Further properties may follow from those bounds, but reachability through a particular process or consistency with other quantities requires evidence of the corresponding relation. Documentation explains the predicate’s intended meaning and limits; it does not replace the proof (module 0: non-vacuity).

Implementation Strategy:

1. Identify unary properties that must hold for every admitted value.

2. Use Lean's subtype notation {x : T // P x} to create refined types.

3. For complex invariants, use structures with proof fields.

4. Provide smart constructors that bundle values with their proofs.

5. Ensure admission and every update return refined types. Justified raw internal representations follow the verified-boundary alternative in §1.1. State and prove transition or history claims separately. Include initialization, preservation, and composition obligations where the claim requires them. A predicate about one admitted state alone does not establish those relations.

Example - Core Refinement Patterns (shared Time type: import Audit.DocPrelude, defined in module 4 §4.1):

The rational Probability above is exact rational arithmetic, not a real interval: a real-valued probability reuses Mathlib's unitInterval, whose symmetry supplies the complement, and is checked as MathlibModels.Probability in the Mathlib integration package.

The shared glossary deliberately makes Time nominal while ResourceAmount reuses the canonical subtype of non-negative rationals. Although both expose non-negative rational values, direct cross-use is rejected:

Application type mismatch: The argument
  t
has type
  Glossary.Time
but is expected to have type
  Glossary.ResourceAmount
in the application
  consume t

2.3 Phantom Types for Disambiguation🔗

Pattern: Parameterize a wrapper by a type tag that does not occur in its stored fields. Different tags distinguish otherwise similar types during type checking. The tag carries no runtime value; this does not by itself specify the wrapper’s compiled representation.

Rationale: A function requiring TaggedId UserTag rejects a TaggedId ProposalTag argument. This prevents direct cross-use of those types. Public payload access and constructors still permit explicit rewrapping under another tag. It does not prove that the wrapped string identifies an existing user or proposal.

Implementation Strategy:

1. Define a generic wrapper type parameterized by a phantom tag.

2. Create tag types that are not definitionally equal; different names for the same type do not suffice. Empty inductive types suffice because no tag value is stored.

3. Define type aliases using the wrapper with specific tags.

4. Verify representative wrong-tag applications fail by type mismatch.

Example - Type-Safe Identifiers:

Boundary of enforcement: Phantom tags make swapped types an elaboration error. Quantity Seconds and Quantity Meters are distinct types. Rational division is total: velocity of a zero Duration produces a well-defined Velocity with value 0. No type error or exception occurs. See module 3 §3.2.1 for totalized operations and encoding a nonzero domain when required.

Application type mismatch: The argument
  { value := 1 }
has type
  Qty Seconds
but is expected to have type
  Distance
in the application
  ratio { value := 1 }

2.4 Abstract Mathematical Models🔗

Pattern: Define system concepts using abstract mathematical types when the claim does not depend on a concrete representation — and define them against the concrete executable types when it does. Abstraction is a tool for claim precision, not a universal exclusion of executable representations.

Rationale: An abstract model omits representation details that the claim does not need. Its proofs establish properties of that model. Transferring a result to an executable Lean definition MUST use a checked theorem relating the two under the required hypotheses. Claims about external execution additionally identify the compiler, runtime, and external-world assumptions that connect the formal objects to execution (module 1 §1.3).

Implementation Strategy:

1. Use mathematical types (ℝ, ℕ, Set α) when the claim is representation-independent

2. Keep representations abstract by parameterizing structures over the content type. A type parameter is quantified and introduces no project logical axiom. An implemented opaque package can instead expose selected operations over a hidden representation (module 6 §6.5.1).

3. Specify behavior through mathematical properties when abstraction serves the claim; specify executable behavior against the executable definition itself when it does not

4. Transfer a model claim to an executable definition only through a proved refinement theorem whose hypotheses name the exact machine conditions — bounds, overflow freedom, domain restrictions — under which the correspondence holds

5. Let implementations choose appropriate concrete representations

Example - Abstract Content Storage:

The stored_of_retrievable field proves that retrieved content satisfies Stored; it does not require retrieving any content. The eq_of_verifies field proves content uniqueness for each verifying identifier; it does not require any identifier to verify anything. An always-false relation satisfies either condition. Existence, retrieval completeness, or a decision procedure requires separate evidence when claimed.

Example - A Checked Refinement Relation:

When the claim transfers from a model to a machine implementation, the transfer theorem carries the machine's exact semantics in its statement and its hypotheses:

Without h, the unconditional refinement statement is false, as the boundary example shows. The checked relation and its hypotheses justify the transfer. UInt32.toNat_add is the exact machine semantics — wrapping modulo 2 ^ 32 — stated by the core library and used by the proof.

Stateful refinement for finite-prefix safety relates transition systems as well as state representations. Relate concrete and abstract states, prove initialization and forward simulation into a precisely defined finite abstract closure, and derive invariant transfer over every finite concrete path. Module 3 §3.9 works through the actual limiter: occupied and free slots are different representations, refusal can stutter, and one reset can match several abstract releases. The proved Lean relation is part of the formal development, distinct from an unproved external adapter.

Anti-Pattern - Unsupported Claims About a Representation: A byte array, hash function, or binary tree is a valid subject for a Lean specification. The defect is claiming properties that its definition and proofs do not establish. A tree representation alone proves no hash-collision or authentication property, and a theorem about an abstract verification relation does not establish the behavior of an unrelated implementation. State the required property and prove it about the chosen representation, or provide the checked correspondence needed to transfer it.