Platform Predicates Specification

This chapter specifies predicates for static device access.

1. Predicate authority

A Clef predicate preserves a proposition, its declaration dependencies and its standing until a concrete use requires a decision. CCS owns that decision. Composer consumes the resulting evidence; it SHALL NOT reinterpret quotations or infer hardware capabilities from architecture names.

2. Source declaration

Fidelity.Platform.Contracts declares:

type ClefPredicate = {
    Name: string
    Condition: Expr<bool>
    Source: string
}

Condition SHALL be a typed Clef quotation. A quotation is compile-time syntax and has no runtime value (quoted expressions). Source identifies the requirement or provenance; its text is not proof evidence.

A relation may refer to immutable declaration values:

let pwmTicks: ClefPredicate = {
    Name = "whole-pwm-clock-ticks"
    Condition = <@ pwmInterruptHz > 0 && applicationIclkHz % pwmInterruptHz = 0 @>
    Source = "Application clock and SysTick plan"
}

The identifiers in this example must be declared in scope. The condition checks the relationship between those declarations. It does not measure a clock or prove the correctness of the code that establishes it.

3. Expression fragment

The evaluator supports integer and Boolean literals, immutable references, fields of declaration-only records, arithmetic, comparisons, same-kind equality, Boolean operators and conditional expressions. Integer arithmetic in this fragment is mathematical, with no host-width truncation.

Explicit fixed-width arithmetic, conversions, general function calls, mutable bindings and records accessible by runtime code are outside the fragment. Division by zero is undecided. A source type error in a dependency SHALL prevent a used condition from establishing access, even when the quotation is erased from executable reachability.

The implementation SHALL retain the declaring node, expression node, dependency nodes, source provenance and one of these states:

Pending SHALL NOT be interpreted as either Boolean value. An unused declaration may remain pending. A used binding that needs it SHALL be rejected until it can be established. A runtime guard SHALL NOT substitute for the required evidence.

4. Device access consumer

Contracts separates DeviceRegion, DeviceRegister, DeviceMapping, DeviceGrant and DeviceAccessPlan. Regions reference the actual BAREWire MemorySpace declarations in the selected platform. Availability of a register SHALL NOT imply a workload grant.

A selected plan closes raw-address MMIO construction for that workload. Mmio.bind8/16/32 grantName registerName selects a register within a named grant. The names SHALL be immutable static strings; they are erased from executable storage. The existing read/write accessors consume the resulting opaque handle.

Before lowering, CCS SHALL establish:

• Region containment, mapping/address extent, alignment and granularity.
• Agreement between the accessor width and declared hardware transaction.
• Both register and workload permissions for the requested operation.
• Full unsigned range coverage for a written value.
• Supported byte order and ordering semantics.
• The mapping establishment and lifetime requirements in this section.
• Every additional predicate required by the grant.

An additional condition, including <@ true @>, SHALL NOT waive these checks. Source integers and memory/transaction requirements remain distinct from the concrete Pointer width in the platform. Static MMIO bindings support 32-bit and 64-bit pointers with volatile 8/16/32-bit transactions.

Static MMIO bindings require nonzero static bases and image-lifetime mappings. reset-identity requires equal region/mapping bases and address-space names. boot-contract admits a CPU-visible placement supplied by an external boot contract. A missing base, runtime establishment or scoped lifetime remains pending when used. Unused declarations may retain these requirements or transaction widths outside the accessor set.

5. Evidence and trust boundary

CCS stores per-site MmioAccessEvidence in graph codata, including the resolved address, transaction, grant/declaration identities and predicate evidence. Composer lowers this established information. With intermediates enabled, it serializes the evidence to device-access.json.

Hardware documentation and boot mapping assertions SHALL be recorded separately as external premises. Arithmetic does not prove physical wiring, page tables, memory attributes, DMA visibility or lifetime of an external mapping. Grants also do not themselves establish MPU/MMU/TrustZone isolation. Assembly and foreign code remain explicit trust boundaries.

Closed-expression checks are compiler evidence, not an SMT solver certificate. Typed ObligationBody families and their proof dispatch are separate mechanisms.

6. Capability declarations

Capability consumers SHALL distinguish instruction availability, numeric representation, concurrency support and deployment permission. Neither a 64-bit word size nor an architecture name establishes vector extensions, atomicity, cache behavior or access to a particular device.

Managed-substrate requirements such as shared-memory availability and the exact integer envelope require a concrete host/platform declaration and consumer under width inference and behavior classification.

7. Diagnostics

Ordinary source type errors retain their original diagnostics. CCS8210 may also identify a source declaration error that would otherwise be hidden by erased reachability. CCS8066 continues to reject quotations used as runtime values. The diagnostic registry is error handling.

8. Implementation references

• Contracts and acceptance scope.
• Predicate evaluator.
• Device-access settlement.
• Composer F# regression runner.
• Platform bindings and numeric types.