SDK guide

SiLA2 controlled contract helper

On this page
  1. Declarations and scope
  2. Ownership and retirement
  3. Binary artifacts and replay
  4. Validation and remaining work

OpenMHS is independent and is not affiliated with, endorsed by, or a reimplementation of Anthropic's MHS research preview.

SiLA2 controlled contract helper

Sila2Driver is a config-only, optional-dependency-free helper for bounded typed controlled peers. It does not implement a SiLA gRPC/protobuf client or admit a native backend. Every non-fake constructor refuses before resolving a native factory or importing a runtime. The unsigned stock hardware loader has its separate review refusal. The registry's sila2 family names this helper with one exemplar package, MHS/drivers/labs/anguyen-23__sila-testing: the complete PhenixImager feature of the pinned gh.anguyen-23/sila-testing clone, on its controlled fake only. That feature is the only one the static source proof below accepts, so a card for any other SiLA feature records a source-verified deviation to a direct Driver or stops blocked HELPER_MISSING.

The complete SDK fixture is tests/fixtures/sila2_phenix. It exposes Connect, Disconnect, StageIn, StageOut, Stop, GoIdle, GoStandby and RunAcquisitionProtocol; all seven declared properties are retained. Six ordinary properties use resource reads. DisplayIcon publishes complete PNG bytes with artifact_ref, size and media type through the stock artifact store and MCP. It is a UI icon, not acquired camera pixels. RunAcquisitionProtocol keeps confirmation, Info, Intermediate and final Result separate. Four explicitly local diagnostic reads expose the last known UUID/progress/intermediate value and whether a confirmation is known; they are not additional native properties, fresh physical readback, an atomic multi-property snapshot or producer timestamps.

Declarations and scope

A declaration fixes peer_format=mhs-sila2-controlled-v1, an opaque endpoint identity, feature FQI, source commit, exact FDL/proto/implementation path hashes, a finite member table, and explicit command/read/stop bindings. Callers cannot supply endpoints, method names, headers, executable expressions or arbitrary result maps. Commands retain effect ownership; a property may be explicitly effectful and then must be exposed as a permit-bound action, never as an ordinary read. Binary outputs require a complete stock artifact binding.

The bounded value compiler preserves Boolean versus Integer, finite Real, UTF-8 String, Binary, nested List/Structure and explicit optional fields/enums. Duration and profile-specific Timestamp structures support protocol control validation. The first public Action/Field projection covers Boolean, Integer, Real, String, List and Structure; Date, Time, Any, custom imported data types, public temporal projections and arbitrary protobuf messages remain unsupported. A declaration cannot silently infer them from Python annotations. Native-shaped errors and metadata are finite controlled records; they are not base64/protobuf/gRPC codecs. Static metadata identifiers belong to the selected FQI. Their actual SiLA sila-...-bin header naming was reviewed as source, but no native header is sent here.

The only static device proof profile is Phenix at commit 0b572380e06977c1920510773b4bfee7bcd0eec5. G7 reads exact FDL, generated proto and implementation bytes, checks all 15 members, kinds, fields, protocol constraints, errors, source ranges, implemented methods and all RPC distinctions. For backend=fake, this proves only the controlled source/request contract. A synthetic SDK fixture must still supply the exact reviewed primary text; a real task must also match the selected commit. A non-fake gate context reports SILA_NATIVE_UNRESOLVED, and native construction is independently refused before factory resolution. The generator-matched sila2-0.14.0 label is a source comparison, not an installed or deployed runtime claim. Other controlled source-version labels do not establish an accepted device profile. Package source proof is not inferred from fake-produced schemas.

The integer bounds 1..1440 minutes for acquisition timeout and at least 60 seconds for standby are protocol constraints from FDL. They do not establish safe optical, stage, thermal or deployment limits. Every effectful action requires a stock input-bound permit; every effectful input requires an operator envelope. The fixture's overlay is a clearly synthetic example that authorizes one fake host, plate, protocol and duration. A declared numeric input_units conversion uses the SDK UCUM converter; incompatible units, nonintegral integer results and conversion beyond the exact integer budget are refused. No rounding, clamping, numeric physical-limit fabrication or implicit unit conversion is performed.

Ownership and retirement

A fake factory receives PeerLease, calls register(peer) before setup, and returns that same peer. Construction runs on the already-retained ordinary owner. Cleanup-worker ownership is established before factory entry. A registered peer cannot be claimed by another lease. Partial construction, failed cleanup and a blocked request retain their handles. A successfully constructed bridge owns its injected peer; if bridge construction fails before its cleanup worker starts, an already-created injected peer remains the injecting caller's responsibility. Native construction is unavailable, including through this injection mechanism on a non-fake Driver backend.

The helper has one ordinary lane and one independent protective lane. A caller timeout, subscription cancellation, execution lifetime or expired UUID does not terminate remote work. A late confirmation attaches to its original owner and cannot trigger new subscriptions or another mutation after the caller has ended. Streams and binary transfer handles remain owned until explicit closure/deletion confirmation or local peer cleanup. Local peer close is not a remote-stop proof. Caller close only signals the pre-owned worker, never joins a not-yet-started thread or waits on the peer. A permanently blocked owned request can therefore keep the daemon and peer alive; this unresolved condition is reported rather than discarded.

Before any request that can allocate a stream or binary transfer crosses the peer boundary, the helper retains its original owner, request identity, request digest and lifecycle generation. A transport exception, typed failure or malformed/missing reply cannot remove this unresolved resource record: the remote allocation may already exist even though its identifier was not received. Stop can still attempt protective action and release known handles, but cannot achieve or reset while an unknown resource remains. An ordinary execution retirement observation does not prove that an unidentified stream or binary transfer was closed.

After exact response correlation, every identifiable execution, stream and transfer is retained before the rest of the body is validated. A late valid handle attaches to its original request, replaces that request's unresolved allocation record and can then be explicitly cleaned up. It does not make the caller's earlier failed receipt successful. Missing, foreign or reused identifiers remain unresolved; malformed identifiable handles can also establish a sticky fault. This applies to both acquisition subscription positions, primary Binary results and observable Binary samples. Ordinary scalar property failures do not invent possible remote resources. Retained unknown resource owners count against the same finite history budget. An empty observable Binary sample batch identifies no transfer and cannot clear its allocation debt, even when its end flag is true. Closing the known stream or observing execution retirement cannot substitute for the missing Binary ownership.

Only the controlled peer has the additional observe contract: monotonically ordered authoritative quiescence, active execution UUIDs and explicitly retired owner UUIDs. This is not a fabricated native SiLA endpoint. Native Phenix has no demonstrated equivalent: acknowledgement-only Stop, cached Idle and late stage eject remain negative controls. Safe state needs a new observation after relevant ordinary settlement, no active execution/resource owner, no sticky contradiction and an unchanged lifecycle generation at atomic commitment. A stale pending stop is not reused as a fresh proof. Protective attempts remain bounded and do not preempt another pending stop. A terminal contradiction prevents achievement and reset but still permits later protective attempts after the previous stop owner ends.

Reset only obtains a fresh observation and releases already-owned local resources. It never invokes Connect, StageIn, home, resume or any other mutation. A renewed unsafe property, ordinary-owner change, close or epoch change prevents rearming. The helper conservatively retains the latch after a stop-class command; on the stock server, enter the server e-stop latch and perform the explicit safety reset before a new mutation. Stock operation cancellation is available only for an admitted observable action whose declaration permits it, and reports cancelled only after independent retirement. Noncancellable operation admission remains enforced by the core binding snapshot.

Histories are deliberately finite and never silently recycled. max_operations bounds retained effect/UUID/transfer histories, with a finite multiple for stream IDs. Exhaustion refuses fresh ordinary work; protective stop/cleanup remains available. Restarting a bridge does not prove a remote device is idle. Native reconnect/exclusivity remains unresolved.

Concurrent protective callers retain the existing Stop owner and wait only within their original deadlines. An epoch advances when a caller owns the protective lane, not when it first asks for a busy lane. Every later admitted caller issues its own fresh Stop and validates its typed confirmation and retirement proof; no old success is reused. Waiting cancellation, timeout or close starts no new RPC, and partial/unknown owners remain retained. The ordinary-effect fence engages immediately; waiting never permits a new mutation.

A separate Stop-request revision protects reset ordering. Reset may clear the latch only if no newer Stop request arrived before its atomic commitment. A later Stop that times out or is cancelled while waiting still prevents an older reset from rearming. This request revision does not invalidate an already-owned Stop proof or advance its epoch. After a fresh Stop completes, a new explicit reset can succeed normally; no recovery Stop or reset is implicit.

safety_status keeps the same fail-closed predicate: any pending ordinary/protective owner, unknown outcome, fault, close or unmatched proof epoch prevents achievement. A state read for a concurrent cancellation receipt can briefly be pending after a valid Stop; the status method may wait at most 50 ms, further capped by each currently owned request's original deadline, before evaluating that predicate under the same lock. The condition releases its lock while waiting, and a worker never waits on itself. This is bounded availability, not an exemption for reads or a cached safety proof. Held/unsafe/never-settling reads and late contrary values cannot produce premature true; status performs no Stop/reset itself.

Binary artifacts and replay

Inline and chunked outputs retain exact bytes. Transfers require the exact UUID, declared total size and SHA256, complete sequential chunk coverage, bounded allocation and confirmed deletion. Even a malformed size retains an identifiable transfer handle. Store preflight precedes the primary property/action request. Publication occurs outside lifecycle locks; late cancellation, e-stop or close prevents commitment and aborts the grant. Stock principal/session isolation, receipt replay, TTL, budgets and cleanup remain authoritative. Replay cannot extend a grant's TTL.

RecordingSila2Peer and Sila2ReplayPeer are bounded tools for the controlled protocol. Replay consumes complete request/response pairs once and only rebinds explicit local request/owner/generation UUIDs. Remote execution/stream/binary UUIDs stay exact. Incomplete recordings, modified input, mismatched identities and exhaustion fail. Replay has no concurrency, timing, transport-failure or native-wire fidelity claim.

Validation and remaining work

Run the SDK-contained tests.driver.test_sila2, tests.bridges.test_sila2, tests.bridges.test_sila2_races, tests.bridges.test_sila2_resource_retention, tests.test_sila2_stock, tests.test_sila2_artifacts and tests.test_sila2_resource_artifacts modules. Tests use original controlled code, standard package loading, real server permits and artifact/MCP paths. No upstream module, generated protobuf, service, simulator or hardware runs. G3 preloads the compiler, checker, bridge and replay policies; it guards mutable source maps and regex identity while allowing the live peer ownership ledger to change.

The synthetic fixture task and lock use upstream: null and retain reviewed_by: null. Three exact primary text files are bundled only for static parsing, with source hashes and the still-unknown license recorded in source-provenance.json. No native or redistribution/license acceptance follows. fixtures/conformance.json provides concrete typed fake inputs. Its example G8 overlay includes a second fictional host solely to test rejection of a permit reused for different input; the peer does not establish a connection to that host.

The complete controlled fixture opts into fixtures/gate-prerequisites.json with the closed profile sila2-controlled-phenix-connect-v1. It names one explicit Connect capability/input and the exact complete non-Connect command/property-action cases plus safety. Only this source-checked complete fake Phenix profile is supported; arbitrary workflows, native backends, hidden extra steps, dropped members, alternative setup actions and widened limits are refused. Each dependent positive/safety case sends the original Connect through a separate stock simulated session and an exact-input permit, with a 500 ms command budget and 1000 ms total preparation budget. Its IsConnected read only confirms preparation; it is never a retirement or safety proof. Preparation must complete and its session must close without a pending operation. No direct peer initialization, automatic Stop/reset, fake initial-state change or native approval is performed.

Ordinary one-class loading still starts disconnected. Connect's own cases, fresh reads and denied/missing/partial-limit cases do not prepare or fill other limits. The positive G6 operator-overlay and G8 OP-011 cancellation controls obtain only their required stock input-bound permits; all negative permit/envelope oracles remain unchanged. Tests verify that closing the preparation session does not stop, latch or disconnect the device, or change another session's permit/artifact grant. The hardware-view test borrows the same fake Driver through a separate simulated preparation server; only that server's evidence handle is closed before projection, and the outer endpoint owns exactly one Driver cleanup. No hardware constructor is involved.

The fake fixture now passes the complete stock G1-G9 gate with the truthful synthetic G2 warning and the existing G6 permit-path coverage notes. Full command/property/icon controls remain separate. The recorder uses trusted executing code boundaries, so a worker retains its own ordinary action/read phase even while another caller holds a Stop window. Retirement observation is a read, owned stream/binary cleanup is an action, and only the finite SDK Stop RPC supplies e-stop evidence. A no-op Stop cannot borrow any of those calls, and malformed typed Stop confirmation still fails safety despite the recorded call. These classifications change no runtime safety or ownership predicate. The fresh unprepared endpoint, false-ready preparation, late connection, cached Idle, acknowledgement-only Stop and late-eject negatives remain failures. A late failed preparation can outlive the caller: the native-shaped owner and cleanup worker stay retained, and the baseline SDK may record a closed-evidence diagnostic when its operation settles after the failed endpoint closes. This is a failed test setup, never an accepted gate or a remote-stop proof.

All fifteen source-design blocker categories remain open: deployed/runtime/dependency profiles; endpoint/TLS and bounded construction; late/reconnect/remote ownership; full Fluent, Florian, Unitelabs OT2, Flex, Phenix, MultiDrop, Micronic and Venus device workflows; physical risk/operator envelopes; unknown device licenses; native primary binary/property freshness; and native conformance plus independent review. The complete Phenix controlled workflow does not implement the other devices or close any device/native/license blocker. No publication, human signature or hardware acceptance is implied.