Daybreak Terminal: a service workbench

One workbench, explicit run targets

The proposed app keeps three destinations: Playground for editing and observing a program; Services for checking a specific contract; Runs for reviewing artifacts and failures. A persistent target selector distinguishes Android/ShimKit, the Backstep loader, and a provisioned iOS guest. The selected device and runtime build remain visible while a run is active.

The interface is a proposal. It does not pretend that a browser animation is a connected Swift compiler or a device result.

A counter closes the loop only when it is observed

source revision
  → compiler exit + diagnostics
  → module hash + transfer receipt
  → module-load receipt on selected device
  → initial rendered value = 0
  → one supported input event
  → observed state value = 1
  → matching render revision / capture
  → saved run record

The current helper already compiles Swift on the Mac and transfers a library by ADB. The missing polished contract is a correlated run record across build, load, state, input, and display. Its shell pipelines suppress compiler exit status with || true, and its module naming uses second-resolution timestamps. A new workbench should retain compiler exit codes, use unique run IDs, and associate a load receipt with the exact module hash before calling the run successful.

An injected compile error should leave the last good module active and show the diagnostic. An absent or wrong device should prevent deployment. A failed state assertion should remain a failure even if the preview looks attractive.

Service readiness must name the tested contract

Use “not run” for missing evidence, “unsupported” for an explicitly rejected capability, “failed” for a violated assertion, and “passed” only for the named case. A cancellation can be a correctly handled result. The table is an implementation review, not a fresh device certification.

A share-sheet acceptance test

For the host path, prepare a unique text payload, request the chooser, select a known receiving test app, and verify exact payload equality there. Exercise cancellation without launching a recipient. For file sharing, verify content type, readable content, and the intended permission lifetime. Record the device and receiver build so the outcome is reproducible.

For a guest path, use the iOS service contract being claimed and capture the guest-side result. Do not substitute an Android chooser demonstration for a working guest activity service. This is where a service workbench is more useful than a broad percentage labeled “Swift support.”

Testing, checking invariants, and formal verification

The current loader suite and the teaching-model checks are executable tests. They cover concrete cases and can catch regressions. A formal claim would require a specified model, assumptions, and a proof or exhaustive model-checking result for a stated property. “All iOS services work for the most part” is neither a bounded proposition nor a testable coverage definition.

Good first formal targets would be narrow: no accepted frame combines resources from different sequences; an accepted identical retry does not invoke a second frame callback; a touch queue never emits a move without an active contact. Proving a model property must still be connected to the implementation and its assumptions.