T1-1: Formalize ExecutionContract and default simulation semantics

[rororowyourboat]

Problem

The core is time-agnostic (T0-4). Time models must enter at the DSL layer. But no mechanism exists for DSLs to declare their time model, and the framework has no formal statement of default execution semantics. Without this, DSLs make implicit timing assumptions that are unverifiable and potentially incompatible across compositions.

Type

[MATH] [DOC] [CODE]

Prioritization

• Criteria: C2 (Completeness), C4 (Leverage)
• Tier: 1 — High Priority
• Phase: 3 — Execution Semantics
• Dependencies: T0-1, T0-3, T0-4
• Blocks: T1-3, T2-1, T2-2, T2-3, T2-4

Current State

No ExecutionContract concept exists anywhere in the codebase. gds-sim implements Moore discrete-time semantics implicitly but doesn't declare or validate this.

Design

@dataclass(frozen=True)
class ExecutionContract:
    time_domain: Literal["discrete", "continuous", "event", "atemporal"]
    synchrony: Literal["synchronous", "asynchronous"] = "synchronous"
    observation_delay: int = 0   # 0 = Moore; discrete only
    update_ordering: Literal["Moore", "Mealy"] = "Moore"

Attached to GDSSpec as optional: execution_contract: ExecutionContract | None = None. Absent means valid for structural verification but not executable.

Moore Discrete-Time Default

d[t]   = g(x[t], u[t])         # policy map
x[t+1] = f(x[t], d[t])         # state update
y[t]   = C(x[t], d[t])         # output map (T0-3)

This is one instantiation of the ExecutionContract space, not a universal definition.

Steps

1. Define ExecutionContract dataclass in gds/execution.py
2. Attach to GDSSpec as optional field
3. Formally state Moore discrete-time semantics as the default for discrete + synchronous
4. SC-011: cross-composition contract compatibility check — incompatible contracts emit ERROR
5. G-007: algebraic loop check for discrete-time (verify if G-006 already covers this)
6. gds-sim validation gate — read ExecutionContract, validate discrete-time before running
7. Update all 7 DSL compilers to emit appropriate contracts:
   • stockflow/control: discrete, synchronous, Moore
   • games: atemporal
   • software: atemporal (most) or discrete (state machines)
   • business: varies by diagram type
8. Write docs/research/execution-semantics.md

Deliverables

• ExecutionContract dataclass in gds/execution.py
• GDSSpec.execution_contract optional field
• Moore discrete-time semantics formal statement
• SC-011: cross-composition contract compatibility check
• G-007: algebraic loop check for discrete-time (if not covered by G-006)
• gds-sim validation gate
• DSL compiler updates (all 7 DSLs)
• docs/research/execution-semantics.md
• Tests for all new code

---

Part of the GDS-Core Improvement Roadmap

Scientific Context

Evidence level: Level 2 (Semantic) — separates specification from simulation. A GDSSpec becomes a valid formal object without an execution model. This is a genuine contribution vs. frameworks where the execution model is built into the specification.

This means:

• Structural properties can be verified without committing to a time model
• Two systems with different time models but the same wiring topology can be compared
• The same spec can be simulated under different execution semantics

Verification Strategy

Cross-built equivalence. Build the same system two ways (DSL compiler with ExecutionContract emission vs. hand-built). Verify equivalence at every level: GDSSpec, CanonicalGDS, SystemIR, and ExecutionContract.

Contract compatibility testing. Construct pairs of specs with:

• Compatible contracts (both discrete/Moore) → SC-011 passes
• Incompatible contracts (discrete + continuous without interface) → SC-011 fails with ERROR
• One spec with contract, one without → composition is valid (absent = no commitment)

DSL compiler regression. After updating all 7 DSL compilers to emit contracts, verify all existing DSL tests still pass — the contract is additive, not breaking.

Showcase

The extended canonical spectrum table gains an ExecutionContract column. Every DSL now declares its time model explicitly. The table becomes a complete specification of the GDS design space.

[rororowyourboat]

Jamsheed's Math Review Feedback on T1-1

Jamsheed argues Mealy machines should be elevated as the general discrete-time framework, not just an option:

Discrete time models may not follow Moore machine structure — since in principle Mealy machines are also allowable time ordering frameworks under GDS, and Mealy machines include Moore machines as a subclass, if desired elevating Mealy machines to "the" discrete time framework would seem to be preferred — note that in this case the 'input' of a Mealy machine may be interpreted to mean the 'Input' of a GDS as described in the paper, providing a more natural interpretation of the state update map.

The current ExecutionContract design already supports this via update_ordering: Literal["Moore", "Mealy"]. The question is whether Mealy should be the default framing (with Moore as the constrained subcase) rather than Moore being the default with Mealy as an option.

This is primarily a documentation/framing decision, not a code change. Tracked as Decision 3 in #172.

See improvement-plans/review_synthesis.md for full context.