Executable K semantics

Executable formal semantics

Architecture claims are backed by executable K rewrite rules. The DKLS23 backend is modeled as transition rules over replicated state, local session state, peer ingress, conflicts, pending frontiers, and terminal evidence. The same K-based approach applies to other backends as they receive formal treatment.

executable semanticsK rewrite-rule witness layer

The formal claim is scoped to executable semantics: DVM is modeled as an executable K rewrite system. Product workflows lower into semantic sites, backend profiles define the concrete transition rules, and those rules determine when a site waits, completes, or aborts.

For DKLS23, the backend model uses content-addressed local handles for operation families such as share_mul, share_inv, share_ec_mul, open_to, keygen_vss, and complete_keyshare. PendingRemote, backend microtraces, abort evidence, and poisoned local sessions are explicit transitions. FROST and CGGMP24 bind to the same witness pattern through their executable semantics.

evalBackend(SITE, CTX, ShareMulBackendOt, [LC, RC])
  => materializePending(... shareMulSsotRound1 ...)
  => materializePending(... shareMulSsotRound2 ...)
  => commitDone(... backendMicroTrace("DKLs23/ShareMul/SoftSpoken", ...))
  => commitAbort(... poisonShareMulSession(...))

The scope is an executable semantics claim, distinct from formal verification: the architecture has rewrite-rule witnesses for pending frontiers, completion traces, terminal aborts, and local-state closure.

N-01

Executable semantics

The formal layer is operational. The executable witness for DKLS23 imports shared core semantics and defines content-addressed handles for keygen_vss, share_mul, share_inv, share_ec_mul, open_to, and complete_keyshare. These are rewrite rules that run and produce counterexamples. When an architecture claim contradicts the K model, the model is authoritative.

N-02

Claim to witness chain

The unit of review is a chain: architecture claim, formal spec layer, K rewrite witness, and runtime artifact. PendingRemote maps to materializePending. Evidence-bearing abort maps to commitAbort with poison transitions. Successful backend completion maps to commitDone, backendMicroTrace, consumeSession, and local scalar save. A reviewer can see exactly which rule class supports a given receipt and what artifact is expected when the path waits, completes, or aborts.

N-03

DKLS23 share_mul witness

For ShareMulBackendOt, the K model starts once local scalar operands exist and the resumable session slot is free. It materializes round1, waits for all round1 ingress, materializes round2, waits for all round2 ingress, enters rVOLE, and either commits a backend microtrace or aborts with poisoned local state.

Invalid continuations are explicit: round1 or round2 conflicts abort with IngressReject, and rVOLE state missing required round2 ingress aborts with Dkls23OtWitnessSerialization and poisons the ShareMul session.

N-04

The ideal-functionality registry

The 'executable formal model' that conformance testing runs against is anchored in a machine-readable registry of ideal functionalities: F_POLICY, F_DKG (with CompleteKeyshare, VSS1, and PublishPubkey refinements), F_DSG, F_REFRESH (with RefreshKeyshare and ReshareKeyshare refinements), F_SHARE_MUL, F_SHARE_INV, F_SHARE_EC_MUL, and F_OPEN_TO. Each entry fixes the functionality's inputs, internal state, outputs, admissible aborts, and — critically — its leakage budget in three classes: what is public by design, what an adversary gains per corrupted party, and what must remain secret. Each entry also fixes its plaintext-release boundary: who may ever see a plaintext result, and what crosses the public boundary (for F_SHARE_MUL, only the output-share content id — never a share).

Registry entries carry anchors into the implementation source, so a reviewer can walk from the security claim to the code that must uphold it. Where a functionality's production-cryptography proof is still open, the registry says so in a status field rather than leaving the scope implicit.

N-05

Machine-checked linkage: instruction schema to functionality

Every runtime instruction carries a static schema that declares, among its operand and binding contracts, a local secret-effect class — None, ReadsLocalSecret, CreatesLocalSecret, ReadsAndWritesLocalSecret, or SessionLifecycle — and a link to the ideal functionality it implements. A CI test rejects any schema that names an unregistered functionality, so the spec-to-code mapping cannot silently drift. Representative rows:

  • keygen — F_DKG — CreatesLocalSecret
  • complete_keyshare — F_DKG.CompleteKeyshare — ReadsAndWritesLocalSecret
  • dkg_share_secret_to — F_DKG.VSS1 — SessionLifecycle
  • publish_pubkey — F_DKG.PublishPubkey — ReadsLocalSecret
  • share_mul (OT-backed) — F_SHARE_MUL — SessionLifecycle
  • share_ec_mul — F_SHARE_EC_MUL — ReadsAndWritesLocalSecret
  • open_to — F_OPEN_TO — SessionLifecycle
  • freeze_presign — F_DSG — ReadsAndWritesLocalSecret
  • publish_sig — F_DSG — ReadsLocalSecret
  • refresh_keyshare — F_REFRESH.RefreshKeyshare — ReadsAndWritesLocalSecret
  • hash_to_scalar, xcoord, verify_sig_local — no functionality — None (no secret interaction)
N-06

Scope of the claim

The system provides executable formal semantics, distinct from formal verification. The model gives rewrite-rule witnesses and executable counterexamples for architecture claims; published proof artifacts are a separate evidence layer. For security review, the scope is precise: the semantics are concrete and inspectable, and the claim is bounded to what has been published.