elicit_ui

Formally verified UI construction with compile-time WCAG 2.2 compliance guarantees, built on AccessKit as a universal intermediate representation.

Overview

elicit_ui models UI construction as a proof-carrying pipeline. Every interactive element is built through a factory trait that performs a WCAG runtime check and, on success, returns both the constructed element and a typed proof token — an Established<P> — that records what was verified. Proof tokens compose upward through section aggregates into a final Established<WcagLevelAAValid>, which is the only legal way to assert that a surface is WCAG 2.2 Level AA compliant.

The compiler enforces this chain. There is no way to produce Established<WcagLevelAAValid> without assembling all the leaf proofs from which it is derived.

Architecture

  ┌─────────────────────────────────────────────────────────────────┐
  │                     WCAG Factory Traits                         │
  │  WcagContrastFactory · WcagLabelFactory · WcagFocusFactory      │
  │  WcagKeyboardFactory · WcagTimingFactory · WcagTargetFactory     │
  │  WcagStructureFactory · WcagMediaFactory · WcagLanguageFactory   │
  │  WcagErrorFactory                                               │
  └────────────────────────────┬────────────────────────────────────┘
                               │ each method returns (Element, Established<Leaf>)
                               ▼
  ┌─────────────────────────────────────────────────────────────────┐
  │               Section Aggregate Factories                        │
  │   WcagPerceivedFactory   →  Established<WcagPerceivedValid>     │
  │   WcagOperableFactory    →  Established<WcagOperableValid>      │
  │   WcagUnderstandableFactory → Established<WcagUnderstandableValid>│
  │   WcagRobustFactory      →  Established<WcagRobustValid>        │
  └────────────────────────────┬────────────────────────────────────┘
                               │ assemble LevelAaEvidence
                               ▼
  ┌─────────────────────────────────────────────────────────────────┐
  │                     WcagBackend supertrait                       │
  │      build_level_aa(evidence) → Established<WcagLevelAAValid>   │
  └────────────────────────────┬────────────────────────────────────┘
                               │
               ┌───────────────┼───────────────┐
               ▼               ▼               ▼
         elicit_egui     elicit_ratatui   elicit_leptos
       (AccessKit IR)   (Ratatui cells)  (Leptos SSR/WASM)

The reference implementation of all factory traits is AccessKitUiBackend, which builds AccessKit Node trees and issues proof tokens. Renderer crates receive proof tokens through the IR but cannot forge them.

Proof Architecture

Proposition types

Every verifiable WCAG invariant has a corresponding Rust type — a proposition — that implements elicitation::contracts::Prop. These types are zero-cost phantoms that exist only at the type level.

pub struct WcagContrastMinimumNormalText;  // SC 1.4.3, normal text ≥ 4.5:1
pub struct WcagFocusVisibleKeyboard;       // SC 2.4.7
pub struct WcagLevelAAValid;               // the full Level AA composite

Proof tokens

Established<P> is the proof that proposition P holds. It is a zero-sized type that carries no runtime data — only type-level evidence.

The ProvableFrom<C> trait

The credential-gated minting path is Established::prove:

impl Established<P> {
    pub fn prove<C>(_: &C) -> Self  where P: ProvableFrom<C> { … }
}

ProvableFrom<C> declares "credential C proves proposition P". The 46 impls live in elicit_ui::contracts::wcag_proofs:

impl ProvableFrom<NormalTextContrastVerified> for WcagContrastMinimumNormalText {}
impl ProvableFrom<FocusVisibleVerified>       for WcagFocusVisibleKeyboard {}
// … 44 more

Credential types

Each credential is a pub(crate) ZST in proof_credentials. External code cannot construct one:

// pub(crate) — only factory methods inside elicit_ui can build this
pub(crate) struct NormalTextContrastVerified;

The factory method constructs the credential after performing the runtime check, then passes it to prove:

fn build_contrast_minimum(&self, input: ContrastDescriptor)
    -> UiResult<(ContrastPair, Established<WcagContrastMinimumNormalText>)>
{
    let ratio = contrast_ratio(&input.foreground, &input.background);
    if ratio < 4.5 {
        return Err(UiError::new(UiErrorKind::InsufficientContrast(…)));
    }
    let pair = ContrastPair { … };
    Ok((pair, Established::prove(&NormalTextContrastVerified)))
    //                                  ^^^^^^^^^^^^^^^^^^^
    //  credential constructed here, after the check, and nowhere else
}

Why this is a compile-time guarantee

• NormalTextContrastVerified is pub(crate) — external crates cannot write Established::prove(&NormalTextContrastVerified).
• ProvableFrom<NormalTextContrastVerified> is only implemented for WcagContrastMinimumNormalText — no other proposition can be proved with that credential.
• Established::assert() remains pub as a general escape hatch, but any call to assert() on a WCAG proposition is immediately visible in code review and audit tooling as an explicit bypass.

WCAG 2.2 Contract Parity

Leaf propositions (41)

Section propositions (5)

Section factories accept evidence bundles — structs whose fields are Established<LeafProposition> tokens. They compose leaf proofs into a section-level proof and pass it upward.

Proof Composition

Proofs compose bottom-up. The compiler rejects any gap in the chain.

// 1. Leaf proofs — each factory method returns (Element, Established<LeafProp>)
let (_, contrast_proof) = backend
    .build_contrast_minimum(ContrastDescriptor { foreground, background })?;
let (_, focus_proof) = backend
    .build_focus_visible(FocusDescriptor { … })?;

// 2. Assemble a section evidence bundle — all fields are required proof tokens
let perceived_evidence = PerceivedEvidence {
    contrast_normal:   contrast_proof,
    non_text_contrast: non_text_proof,
    focus_contrast:    focus_contrast_proof,
    color_not_sole:    color_proof,
};

// 3. Section factory consumes the bundle, produces a section proof
let (_, perceived_proof) = backend.build_perceivable(perceived_evidence);

// 4. Repeat for all four WCAG principles, then assemble the top-level bundle
let level_aa_evidence = LevelAaEvidence {
    perceived:      perceived_proof,
    operable:       operable_proof,
    understandable: understandable_proof,
    robust:         robust_proof,
};

// 5. Mint the composite Level AA proof
let level_aa_proof: Established<WcagLevelAAValid> =
    backend.build_level_aa(level_aa_evidence);

If any leaf is missing the evidence bundle struct literal will not compile — there is no API to skip a field.

Trait Interface

Factory traits (leaf level)

pub trait WcagContrastFactory: Send + Sync {
    fn build_contrast_minimum(&self, input: ContrastDescriptor)
        -> UiResult<(ContrastPair, Established<WcagContrastMinimumNormalText>)>;

    fn build_contrast_minimum_large(&self, input: ContrastDescriptor)
        -> UiResult<(ContrastPair, Established<WcagContrastMinimumLargeText>)>;

    fn build_contrast_enhanced(&self, input: ContrastDescriptor)
        -> UiResult<(ContrastPair, Established<WcagContrastEnhancedNormalText>)>;

    fn build_contrast_enhanced_large(&self, input: ContrastDescriptor)
        -> UiResult<(ContrastPair, Established<WcagContrastEnhancedLargeText>)>;

    fn build_non_text_contrast(&self, input: ContrastDescriptor)
        -> UiResult<(ContrastPair, Established<WcagNonTextContrastMinimum>)>;
}
// … WcagLabelFactory, WcagFocusFactory, WcagKeyboardFactory,
//   WcagTimingFactory, WcagTargetFactory, WcagStructureFactory,
//   WcagMediaFactory, WcagLanguageFactory, WcagErrorFactory

Section aggregate traits

pub trait WcagPerceivedFactory: Send + Sync {
    fn build_perceivable(&self, evidence: PerceivedEvidence)
        -> (PerceivedSection, Established<WcagPerceivedValid>);
}

Top-level supertrait

pub trait WcagBackend:
    WcagContrastFactory + WcagLabelFactory + WcagFocusFactory
    + WcagKeyboardFactory + WcagTimingFactory + WcagTargetFactory
    + WcagStructureFactory + WcagMediaFactory + WcagLanguageFactory
    + WcagErrorFactory + WcagPerceivedFactory + WcagOperableFactory
    + WcagUnderstandableFactory + WcagRobustFactory
    + Send + Sync
{
    fn build_level_aa(&self, evidence: LevelAaEvidence)
        -> Established<WcagLevelAAValid>;
}

AccessKitUiBackend implements WcagBackend and is the reference backend shipped with this crate. Other implementations must satisfy the same trait bounds — the factory signatures are the contract.

Compile-Time Guarantee Summary

Evidence Bundles

Evidence bundles are the bridges between proof layers. Each field must be filled with a token minted by the corresponding factory method.

pub struct PerceivedEvidence {
    /// Normal text meets SC 1.4.3 (≥ 4.5:1).
    pub contrast_normal:   Established<WcagContrastMinimumNormalText>,
    /// Non-text controls meet SC 1.4.11 (≥ 3:1).
    pub non_text_contrast: Established<WcagNonTextContrastMinimum>,
    /// Focus indicator meets SC 1.4.11 / 2.4.11 contrast.
    pub focus_contrast:    Established<WcagFocusIndicatorContrast>,
    /// Colour is not the sole means of conveying information (SC 1.4.1).
    pub color_not_sole:    Established<WcagColorNotSoleConveyor>,
}

pub struct LevelAaEvidence {
    pub perceived:      Established<WcagPerceivedValid>,
    pub operable:       Established<WcagOperableValid>,
    pub understandable: Established<WcagUnderstandableValid>,
    pub robust:         Established<WcagRobustValid>,
}

Implementing a Custom Backend

To implement WcagBackend for a new rendering target:

1. Implement all ten leaf factory traits (WcagContrastFactory through WcagErrorFactory). Each method must perform its runtime check, then call Established::prove(&Credential) only after the check passes.

2. Implement the four section factories. These accept evidence bundles and call prove with the evidence value as the credential.

3. Implement WcagBackend. The build_level_aa default impl composes the four section proofs into Established<WcagLevelAAValid> — override only if the backend needs additional logic.

Note for external backends: Credentials are pub(crate) inside elicit_ui. Implementations that live outside this crate can use Established::assert() at the leaf level — which is an explicit, auditable choice — or add their credential types and ProvableFrom impls inside elicit_ui as a new backend module.

Formal Verification

The proof architecture is designed for downstream formal verification. Each proposition type implements elicitation::contracts::Prop, which exposes a kani_proof() method for generating verification harnesses.

• Kani — bounded model checking on credential construction paths
• Creusot — deductive verification that factory bodies satisfy their WCAG postconditions before calling prove
• Verus — SMT-based proofs of composition totality

Crate Layout

src/
├── lib.rs                      pub use surface
├── accesskit_backend.rs        AccessKitUiBackend — reference WcagBackend impl
├── proof_credentials.rs        41 pub(crate) ZST credential types
├── contracts/
│   ├── mod.rs
│   ├── wcag_proofs.rs          46 ProvableFrom<C> for P impls
│   ├── node_roles.rs           AccessKit role proofs
│   └── ui.rs                   layout / navigation proofs
├── traits/
│   ├── wcag.rs                 14 factory traits + WcagBackend supertrait
│   └── renderer.rs             UiNodeBridge, UiLayoutManager, UiNavigationManager
├── wcag_types.rs               descriptor, element, evidence, section types
├── typestate.rs                Layout<Pending>, Layout<Verified>
├── constraints/                runtime WCAG constraint checking
├── color_contrast.rs           WCAG contrast ratio arithmetic
└── css_units.rs                CssLength, zoom invariance

License

Licensed under Apache-2.0 OR MIT.