---
title: "Branch · Z1 Controller Review"
description: "Branch · Z1 Controller Review - URL: https://chatgpt.com/c/6a81e541-29c0-83ea-acc5-952ad1120539 - Created: 2026-08-16T16:28:49.910Z --- Review this implementation of the Z1 controller. There are mu…"
doc_version: 1
last_updated: 2026-10-15
canonical_url: "http://parc.yolo.scapegoat.dev/note/transcripts/2026/08/16/chatgpt-transcript-branch-z1-controller-review"
---
# Branch · Z1 Controller Review
Branch · Z1 Controller Review - URL: https://chatgpt.com/c/6a81e541-29c0-83ea-acc5-952ad1120539 - Created: 2026-08-16T16:28:49.910Z --- > Review this implementation of the Z1 controller. There are mu…
## Content
# Branch · Z1 Controller Review
- URL: https://chatgpt.com/c/6a81e541-29c0-83ea-acc5-952ad1120539
- Created: 2026-08-16T16:28:49.910Z
---
> Review this implementation of the Z1 controller. There are multiple axes to revie:
>
>
>
> - the machine control design
> - the algorithms and path design
> - the JS API + language design for the CAM design language
>
>
>
> Study it all, clone whatever git repos you need, be diligent.
>
>
>
> Write a markdown + pdf report.
```unknown
bash -lc cat /home/oai/skills/pdfs/SKILL.md && printf '\n---ZIP CONTENTS---\n' && unzip -l /mnt/data/dropcut-studio.zip | sed -n '1,220p'
```
I’ll map the project architecture, run available builds/tests, trace controller and CAM execution paths, and inspect linked upstream repositories. Then I’ll deliver a cited Markdown review and rendered PDF.
💭 Thinking
**Reviewing the repository**
I’m assessing the Z1 controller implementation across the CLI and studio components, starting with structure, tests, and module metadata. I’ll compare available upstream code where possible, then verify findings through focused checks.
**Reviewed the repository**
💭 Thinking
**Auditing the codebase**
I’m mapping the repository, measuring its scope, and checking available runtimes before running tests. I’ll inspect dependencies, the Go module relationship, and the frontend build so I can separate confirmed failures from design concerns.
**Audited the codebase**
**Inspected ZIP/PDF requirements, repository configuration, origins, and controller APIs**
💭 Thinking
**Searched 5 websites**
💭 Thinking
**Cloned CLI and reference repositories**
**Retrieved repository metadata and fetched the latest archive**
💭 Thinking
**Inspecting implementation details**
I’m narrowing the review to controller behavior, safety handling, command coverage, and documentation accuracy. I’ll trace key packages and line-level evidence, then run focused tests and static checks to distinguish real defects from stale notes.
**Inspected implementation details**
💭 Thinking
**Inspected Go and TypeScript projects, dependencies, tooling, and compiler errors**
**Planned machine analysis and inspected Carvera firmware repositories and commits**
💭 Thinking
**Evaluating geometry validation**
I’m checking whether path construction actually guarantees continuity and valid arcs. Early concerns include weak frame checks, unvalidated radii and axes, and polyline sampling that may permit unintended jumps despite the continuity claim.
💭 Thinking
**Assessing geometry validation**
I’m verifying whether path construction truly guarantees continuity and valid arcs. Current concerns include weak frame checks, unvalidated radii and axes, and polyline sampling that may allow unintended jumps despite continuity claims.
**Testing safety boundaries**
I’m examining command completion, decoder concurrency, simulation fidelity, and certificate construction. I’m also checking whether machine profiles and tool geometry reject invalid inputs or merely clamp them, since that can hide unsafe assumptions.
**Assessed geometry validation**
💭 Thinking
**Inspected codebase, validation, safety, motion, and control-flow implementations**
💭 Thinking
**Finalizing the review**
I’m consolidating the verified findings into a structured report, separating release-blocking safety issues from architectural and API concerns. I’ll include reproducible evidence, recommended fixes, test limitations, and clearly documented provenance.
💭 Thinking
**Inspected compiler, geometry, transport, documentation, and dependency code thoroughly**
💭 Thinking
**Checking in briefly**
Hello! I’m here and ready to help. I’m still organizing the repository review and identifying the relevant firmware pieces, but I haven’t completed the full analysis yet.
**Checked in briefly**
💭 Thinking
**Inspecting repositories, documentation, and architecture**
💭 Thinking
**Searched 7 websites**
💭 Thinking
**Checked candidate repository URLs**
💭 Thinking
**Searched 1 website**
💭 Thinking
**Preparing repository review**
I’m assessing whether the project can be inspected directly, compared with its public upstream state, and tested locally. I’ll first verify the available files and environment before deciding what checks are practical.
**Prepared repository review**
💭 Thinking
**Inspected repository code, dependencies, tests, tooling, configurations, and source files**
💭 Thinking
**Reviewing safety behavior**
I’m examining command classification, preflight enforcement, and reproducibility risks. A key concern is that direct cycle-start requests may resume motion without the same preflight checks enforced elsewhere, so I’m tracing those paths carefully.
**Reviewed safety behavior**
💭 Thinking
**Tracing command hazards**
I’m identifying two concrete risks: embedded newlines may allow multiple commands in one payload, and cycle-start appears to bypass preflight checks. I’m also separating API semantics, dry-run limitations, composite-motion behavior, and incomplete firmware-error handling.
**Traced command hazards**
💭 Thinking
**Assessing remote security**
I’m checking token exposure, plaintext transport, unauthenticated telemetry, origin validation, and browser protections. The main concerns are replayable URL credentials, remote traffic without encryption, and publicly reachable status or camera endpoints.
**Assessed remote security**
💭 Thinking
**Prioritizing report findings**
I’m consolidating the implementation review into a Markdown report and PDF, emphasizing the confirmed command-injection risk, missing preflight on cycle start, testing limits, and the broader CAM architecture.
💭 Thinking
**Researching compiler theory**
I’m identifying the project’s needs: intermediate representations, semantics, transformation passes, operational-research connections, and machine-checkable certificates. I’ll ground the explanation in established theory and tailor it to this compiler architecture.
**Researched compiler theory**
💭 Thinking
**Structuring the theory**
I’m connecting compiler pipelines, formal semantics, geometric reasoning, numerical guarantees, and certificate design. I’ll frame each pass as a contract-preserving refinement, with explicit invariants and checkable evidence.
**Structured the theory**
**Formalizing the compiler**
I’m modeling the pipeline with typed, state-aware intermediate representations, explicit units and frames, and semantics for motion, stock, tooling, and safety. I’m also defining conservative geometric certificates with numerical error bounds.
**Formalized the compiler**
**Gathering foundational sources**
I’m selecting primary references on semantics, verification, abstract interpretation, certified compilation, IR design, and planning. I’ll connect these foundations to CAM-specific scheduling, path linking, machine states, and evidence-producing transformations.
**Gathered foundational sources**
**Inspected project files, documentation, and compiler analysis sources**
💭 Thinking
**Inspected source files with line numbers**
💭 Thinking
**Searched 12 websites**
💭 Thinking
**Inspected compiler architecture, passes, planner, documentation, and APIs**
💭 Thinking
**Defining verified compilation**
I’m treating the system as a refinement pipeline, not merely a source-to-text compiler. I’m separating logical machine semantics, physical assumptions, numerical approximation, and certificates that preserve safety properties across passes.
**Defined verified compilation**
**Searched 1 website**
💭 Thinking
**Searched 8 websites**
💭 Thinking
**Inspected IR pipeline paths, validation, certificates, sandbox, and analysis checks**
💭 Thinking
**Planning textbook creation**
I’m preparing the requested Markdown and PDF by inspecting the existing project materials, researching the relevant theory, and organizing chapters with examples, exercises, diagrams, and technical explanations.
**Planned textbook creation**
💭 Thinking
**Building the textbook framework**
I’m shaping a self-contained textbook around compiler theory, intermediate representations, certified geometry, optimization, invariants, and assurance. I’ll connect those ideas to the project case study and include references, exercises, and examples.
**Built the textbook framework**
**Reviewed PDF requirements and inspected project archive and existing review**
💭 Thinking
**Organizing implementation details**
I’m organizing the material into theory, verified compilation, geometry, optimization, certification, runtime assurance, and a project-specific implementation section, while keeping the final textbook coherent and practical.
**Organized implementation details**
**Inspected Dropcut repository and key implementation files**
💭 Thinking
**Preparing final files**
I’m consolidating the case study, theory chapters, implementation guidance, exercises, and bibliography into the requested Markdown and PDF deliverables, then I’ll verify the rendered PDF before sharing links.
**Defining the textbook scope**
I’m covering semantics, layered IR, effectful machine state, compiler correctness, geometric certification, optimization, runtime assurance, and a Dropcut case study, supported by primary references and practical exercises.
**Prepared final files and defined textbook scope**
💭 Thinking
**Searched 2 websites**
💭 Thinking
**Created certificate-carrying CAM compiler textbook with verified PDF figures**
=
Cmd;
type Cut =
Cmd;
```
The source API can make impossible sequences difficult to construct.
## 10.5 Limits of type-level safety
TypeScript types are erased. A forged value, unchecked deserialization, stale controller state, or physical mismatch can violate the index. Type-level typestate proves a property of the host program under its model; it does not prove the machine is physically in that state.
Runtime preflight must re-establish assumptions at the execution boundary.
## 10.6 Algebraic effects versus monolithic state
One large `MachineState` can become difficult to reason about. An alternative is to describe effects separately:
```ts
type Effect =
| ReadPose
| RequireHomed
| SelectTool
| SetSpindle
| Move
| RemoveStock
| Probe
| EmitDiagnostic;
```
Handlers interpret these effects for simulation, validation, preview, or controller execution. This can improve modularity, but it still requires a coherent ordering and state model. The key is not the syntax of monads versus effect handlers; it is the explicit representation of effects and their laws.
## 10.7 Worked example: probe then offset
A probe returns a measured coordinate:
```ts
type Probe = Cmd;
type SetWorkOrigin =
(m: Measurement) => Cmd;
```
Kleisli composition connects the returned value to the next operation:
```ts
const establishWcs = probeSurface(direction, maxTravel)
.flatMap(measurement => setWorkOrigin(measurement));
```
The data dependency is explicit. A command list that merely places `probe` before `set offset` without binding the result is semantically incomplete.
## 10.8 Exercises
1. Implement `pure` and `bind` for a result-and-state command type.
2. State the three monad laws and explain their practical value for command sequencing.
3. Design indexed states for unhomed, homed, tool-selected, and spindle-running modes.
4. Explain one invariant that TypeScript typestate cannot establish about a physical machine.
5. Model a probe command that can return contact, no contact, or alarm.
6. Compare a state monad with an explicit effect algebra for CAM.
# State Tokens, SSA, and Ordering
> **Learning objectives.** The reader should be able to use an SSA-style state token to make effects explicit, construct def-use dependencies, and identify which transformations are legal around stateful commands.
## 11.1 The machine state as a linear resource
A practical IR need not encode every typestate distinction in TypeScript generics. It can make ordering explicit with a state token. Each effectful operation consumes one token and produces the next.
{width=98%}
```text
%s0 = machine.initial
%s1 = machine.require_homed %s0
%s2 = tool.select %s1 @T1
%s3 = spindle.start %s2 12000rpm
%s4 = motion.cut %s3 path=@p feed=400
%s5 = spindle.stop %s4
```
The token is not the full runtime state. It is an ordering and dependency witness.
## 11.2 Relation to SSA
Static single assignment form gives each value one definition and makes data dependencies explicit [R15]. A machine-state token applies the same discipline to side effects. Operations cannot be silently reordered across token dependencies.
Pure geometry computations need no token:
```text
%p1 = path.offset %feature by=1.2mm
%p2 = path.reverse %p1
```
Effectful program construction does:
```text
%s1 = motion.traverse %s0 to=%p1.start
%s2 = motion.cut %s1 path=%p1
```
## 11.3 Multiple resources
One global token is simple but can over-serialize independent work. A richer IR can use separate tokens for:
- controller state;
- stock state;
- tool library state;
- measurement environment;
- diagnostic/provenance stream.
However, splitting resources requires precise alias and commutativity rules. Two cuts that affect disjoint stock regions might commute geometrically but not mechanically if they change support or linking clearance.
For an initial implementation, a single machine/process token is usually safer.
## 11.4 Probe values and control flow
SSA makes measurements explicit values:
```text
%m, %s1 = probe.toward %s0 direction=-Z max=10mm
%t = frame.from_probe %m datum=@top_surface
%s2 = frame.install %s1 %t as=G54
```
A failed probe can branch:
```text
switch %m.status:
contact -> continue
no_contact -> abort
alarm -> quarantine_session
```
The IR can represent merge points with block arguments or phi-like values. A validator must ensure that state invariants hold along every incoming path.
## 11.5 Effect summaries
Optimization and scheduling require summaries:
```ts
interface EffectSummary {
reads: readonly ResourceRegion[];
writes: readonly ResourceRegion[];
requires: readonly Predicate[];
ensures: readonly Predicate[];
mayFail: readonly FailureClass[];
}
```
A pass may commute two operations only if their effects are independent and the reordered preconditions remain valid.
## 11.6 Linear and affine use
A state token should usually be consumed exactly once. Duplicating it would fork the machine into two contradictory futures. Dropping it can omit required shutdown or recovery behavior.
A linear type system enforces exactly-once use; an affine system permits dropping but not duplication. Most mainstream TypeScript code cannot enforce this statically, but the IR verifier can check def-use counts.
## 11.7 Worked example: preventing an unsafe reorder
Suppose an optimizer sees:
```text
%s1 = spindle.start %s0 12000rpm
%s2 = motion.cut %s1 @p
%s3 = spindle.stop %s2
```
Moving `spindle.stop` before the cut would require consuming `%s1` and producing a new state passed to the cut. The cut's `SpindleRunning` requirement fails. The token graph exposes the invalid transformation.
## 11.8 Exercises
1. Convert a small imperative command list into state-token SSA.
2. Explain why duplicating a machine state token is unsound.
3. Design a verifier for single-definition and single-consumption token use.
4. Show a legal reordering of two pure geometry operations.
5. Give a case where two cuts in disjoint regions still should not commute.
6. Model a branch after probing and the merge of its safe paths.
# Provenance, Identity, and Reproducibility
> **Learning objectives.** The reader should be able to design total provenance, content-address artifacts, distinguish identity from display names, and bind diagnostics and certificates to exact inputs.
## 12.1 Provenance is semantic data
When a final move fails a check, the system should explain which source operation, feature, strategy, and compiler pass produced it. Provenance is therefore not an optional debug string. It supports:
- diagnostics;
- certificate dependency graphs;
- incremental recompilation;
- audit and review;
- visual selection in the UI;
- comparison between compiler versions;
- fault localization.
## 12.2 A provenance chain
```ts
interface Provenance {
sourceSpan?: SourceSpan;
authoringNode?: NodeId;
operation?: OperationId;
feature?: FeatureId;
strategy?: { id: string; version: string };
passHistory: readonly PassRecord[];
parentArtifacts: readonly Hash[];
}
```
Every transformation either preserves provenance, refines it, or introduces a synthetic operation with an explicit reason such as `safety-retract` or `postprocessor-spindle-stop`.
## 12.3 Content addressing
An artifact hash should cover canonical serialization of:
- semantic content;
- schema version;
- relevant configuration;
- referenced artifact hashes.
A display filename is not identity. Two jobs named `part.nc` may differ; the same job may have several names.
Canonical serialization must define:
- map key order;
- number format;
- treatment of negative zero;
- Unicode normalization;
- omitted versus null fields;
- endianness for binary data;
- schema versioning.
## 12.4 Reproducible passes
A pass result should be a function of explicit inputs:
$$
O=F(I,C,V,S),
$$
where $C$ is configuration, $V$ identifies the pass implementation, and $S$ is any declared random seed. Hidden time, locale, thread interleaving, or unordered iteration can break reproducibility.
Reproducibility does not guarantee correctness, but it makes evidence, debugging, and regression analysis tractable.
## 12.5 Machine and firmware identity
A machine profile named `z1` is not sufficient if firmware revisions change protocol or motion semantics. The executable bundle should identify:
- machine model and configured limits;
- controller dialect and firmware compatibility range;
- relevant capability flags;
- postprocessor version;
- calibration profile version;
- known semantic deviations.
Runtime preflight compares live identity with the bundle assumptions.
## 12.6 Provenance through optimization
An optimizer may merge, split, or reorder paths. It should retain a many-to-many mapping:
```ts
interface OriginMap {
outputRange: CommandRange;
inputs: readonly {
artifact: Hash;
operation?: OperationId;
pathRange?: ParameterInterval;
}[];
transformation: string;
}
```
This allows a gouge counterexample at final block 813 to highlight the source finishing operation and the arc-fitting pass that changed it.
## 12.7 Worked example: cache key
A toolpath-planning cache key should include more than the feature geometry:
```text
hash(
intentIR,
targetMeshHash,
stockHash,
toolAssemblyHash,
strategyIdAndVersion,
planningTolerance,
machine-relevant constraints,
deterministicSeed
)
```
Omitting the tool hash can reuse a path computed for a different cutter. Omitting the tolerance can attach an outdated witness to a stricter request.
## 12.8 Exercises
1. Design a canonical serialization rule for floating-point numbers.
2. Explain why a filename is not an artifact identity.
3. List the inputs to a deterministic contour-planning cache key.
4. Define provenance for an automatically inserted retract.
5. Describe how a certificate becomes stale after a machine-profile change.
6. Give one source of nondeterminism in JavaScript object iteration or parallel planning and show how to control it.
# Designing an Extensible CAM API
> **Learning objectives.** The reader should be able to design an API that is composable, explicit about context, extensible through strategies and kernels, and resistant to invalid states.
## 13.1 Separate stable concepts from plugins
The stable API should expose semantic concepts:
- frames and units;
- stock, target, fixtures, and tools;
- manufacturing features and operations;
- paths and motion classes;
- tolerances, assumptions, and diagnostics;
- compilation and certification stages.
Strategies should be plugins:
```ts
interface Strategy {
id: string;
version: string;
supports(intent: I, context: PlanningContext): SupportResult;
plan(intent: I, context: PlanningContext): Result<{
paths: readonly PlannedPath[];
witness: W;
}, Diagnostic[]>;
}
```
A strategy may propose output; it should not mint final safety claims.
## 13.2 Kernel independence
Geometry algorithms should depend on interfaces rather than one mesh library:
```ts
interface SurfaceOracle {
bounds(): Box3;
heightAtXY(x: Mm, y: Mm): Interval | "outside";
closestPoint(p: Point3): ClosestPointBound;
raycast(ray: Ray3): readonly HitBound[];
}
```
Different kernels can implement exact B-rep queries, mesh acceleration structures, interval fields, or remote computation. The semantic contract says what bounds the result provides.
## 13.3 Explicit contexts
Avoid ambient mutable settings such as “current feed,” “current tool,” or “current frame” inside planners. Pass immutable contexts:
```ts
interface PlanningContext {
machine: MachineProfileRef;
setup: SetupRef;
activeTool: ToolRef;
frame: FrameId;
toleranceBudget: ErrorBudget;
stockState: StockStateRef;
seed: bigint;
}
```
The authoring API may offer convenient scopes, but elaboration should convert them into explicit fields.
## 13.4 Result types and diagnostics
Exceptions are appropriate for programmer errors and violated internal invariants. User-level compilation failures should be values:
```ts
type CompileResult =
| { ok: true; value: T; diagnostics: readonly Diagnostic[] }
| { ok: false; diagnostics: readonly Diagnostic[] };
```
A diagnostic should include severity, stable code, source provenance, artifact context, quantitative details, and suggested remediation.
## 13.5 Escape hatches
Advanced users may need raw controller operations. An escape hatch should be isolated:
```ts
interface RawControllerBlock {
text: string;
declaredDialect: DialectId;
declaredEffects?: EffectSummary;
provenance: Provenance;
}
```
Self-declared effects are assumptions, not proof. An independent parser may establish actual effects for a supported grammar. Otherwise, affected analyses become unknown and production certification should fail closed.
## 13.6 API layers
A pleasant system can offer three layers:
**Feature API** for most jobs:
```ts
roughPocket(feature, { tool: "T1", strategy: "adaptive" });
finishPocket(feature, { tool: "T2" });
```
**Path API** for custom machining geometry:
```ts
cut(path, { tool: "T1", feed: mmPerMin(350), intent: "finish" });
```
**Machine API** for exact canonical actions:
```ts
program.append(traverse(path, clearance));
program.append(dwell(seconds(1)));
```
Lower layers carry more responsibility and require stronger evidence.
## 13.7 Law-driven API testing
Algebraic laws become property tests:
- path identity and associativity under exact endpoints;
- frame-transform identity and inverse;
- serialization round trip;
- deterministic planning under fixed inputs;
- pass idempotence for canonicalization;
- effect-summary conservativeness;
- certificate invalidation under changed dependencies.
The API design should make laws visible enough to test.
## 13.8 Worked example: compiling explicitly
```ts
const authored = evaluateScript(source, scriptEnvironment);
const plan = elaborate(authored.ast, projectContext);
const intent = normalizeIntent(plan.value);
const proposed = strategyRegistry.plan(intent, planningContext);
const checkedPaths = checkPlanningWitness(intent, proposed);
const scheduled = schedule(checkedPaths, schedulingPolicy);
const machine = lowerToMachine(scheduled, z1Profile);
const controller = lowerToMakera(machine, makeraDialect);
const bytes = serialize(controller);
const final = validateFinalArtifact({
intent,
machine,
controller,
bytes,
setup,
});
```
Each call has an explicit input and output. There is no hidden global “current job” whose meaning changes between preview and export.
## 13.9 Exercises
1. Design a strategy interface for constant-Z waterline finishing.
2. Define a geometry-kernel query with a sound outer bound.
3. Explain when to use an exception versus a diagnostic result.
4. Design three API layers for drilling.
5. Specify how a raw controller block affects certification.
6. Write five algebraic or metamorphic properties for the API.
7. Explain why plugin version identity belongs in provenance.
EOF
wc -l -w -c /mnt/data/z1_textbook_work/book/Certificate_Carrying_CAM_Compilers.md
```
The first ten chapters are drafted, including bounded refinement, stock semantics, path/effect modeling, modal lowering, and JavaScript staging. Numerical guarantees now explicitly distinguish inner from outer approximations.
💭 Thinking
**Appended language design chapters and wrote compiler passes**
(
state: S,
motion: CuttingMotion,
): Result {
requireFinitePath(motion.path);
requirePositiveFeed(motion.feed);
requireToolMatch(state.tool, motion.tool);
// geometric and runtime obligations remain explicit claims
}
```
Do not pretend that a runtime assertion about metadata proves physical collision freedom. Contracts should state the boundary of what they establish.
## 22.9 Exercises
1. Write a Hoare triple for spindle start.
2. Derive $wp$ for `select tool; start spindle; cut` with final condition `stock conforms to roughing intent`.
3. State and prove a stock-monotonicity invariant for a simplified semantics.
4. Distinguish an assumption from a precondition in a live tool check.
5. Give an example of a local resource footprint for two independent operations.
6. Explain partial versus total correctness for an abort command.
# Abstract Interpretation for Machine Programs
> **Learning objectives.** The reader should be able to define concrete and abstract domains, implement sound transfer functions, compute invariants over control flow, and use unknown states conservatively.
## 23.1 Simulating one trace is not analyzing all traces
A simulator executes one concrete state through one control path. A validator often needs to cover many possible states: unknown initial modal settings, uncertain positions, branches after probing, controller faults, or values from macros. Abstract interpretation computes over-approximations of these possibilities [R7].
Let $C$ be a concrete domain and $A$ an abstract domain. A concretization function:
$$
\gamma:A\to\mathcal{P}(C)
$$
maps an abstract value to the concrete states it represents.
A sound abstract transfer function $\widehat{F}$ satisfies:
$$
F(\gamma(a))\subseteq\gamma(\widehat{F}(a)).
$$
## 23.2 Abstract machine state
```ts
interface AbstractMachineState {
position: Box3 | "unknown";
homing: "homed" | "unhomed" | "maybe";
tool: ToolRef | Set | "unknown";
spindle: "off" | RpmInterval | "unknown";
wcs: TransformInterval | "unknown";
motionMode: Set;
feed: Interval | "unknown";
playing: "yes" | "no" | "maybe";
alarm: "yes" | "no" | "maybe";
}
```
The domain should be just expressive enough for the claims it checks.
## 23.3 Interval transfer
For a linear absolute move to $X=x$, the abstract X interval becomes $[x,x]$ after accounting for rounding and transform uncertainty. In incremental mode, it becomes:
$$
X' = X + [x-\rho,x+\rho].
$$
If distance mode is `{absolute, incremental}`, the successor joins both possibilities. Precision drops, but soundness remains.
## 23.4 Modal-state analysis
An abstract G-code interpreter can prove:
- units definitely metric;
- distance mode definitely absolute;
- spindle definitely on before each cut;
- position remains inside travel bounds;
- no motion occurs with unknown WCS;
- raw commands do not leave required modal components unknown;
- final spindle state is definitely off.
Each block records an invariant before and after:
```ts
interface BlockInvariant {
blockIndex: number;
before: AbstractMachineState;
after: AbstractMachineState;
}
```
A small proof checker replays abstract transfers and verifies safety predicates.
## 23.5 Joins and loss of precision
If one branch selects tool T1 and another selects T2, the merge state contains `{T1,T2}`. A later operation requiring exactly T1 cannot be proved safe without a guard.
Widening may be necessary for loops. For example, repeated incremental motion can make position unbounded unless the loop count is bounded. A production-certifiable dialect may reject unbounded macros rather than analyze them imprecisely.
## 23.6 Reduced products
Different abstract domains can cooperate. A position box and a linear relation domain may jointly prove tighter bounds. A modal-state domain and typestate domain can reduce each other: if an alarm is definite, playing is false; if spindle is off, RPM interval is zero.
Such combinations increase checker complexity. Begin with simple domains tied to explicit claims.
## 23.7 Unknown raw effects
A raw block that is not parsed should conservatively set affected state to unknown. Self-declared effects can be recorded as assumptions, but they do not justify a proved claim.
```ts
function transferRaw(state: AbstractState, raw: RawBlock): AbstractState {
return {
...state,
position: "unknown",
motionMode: allMotionModes,
feed: "unknown",
spindle: "unknown",
wcs: "unknown",
};
}
```
A later explicit preamble can re-establish some components.
## 23.8 Worked example: final spindle state
A program branches around an optional finishing pass. Both branches eventually execute `M5`. At the merge, spindle is definitely off. If one branch omits `M5`, the merge state is `{off,on}` and the final safety epilogue claim fails.
## 23.9 Exercises
1. Define a concretization function for an interval.
2. Write abstract transfer rules for G90, G91, G20, and G21.
3. Explain why joining branches loses precision.
4. Design a sound state update for an unknown raw command.
5. Show how a loop of incremental X moves can require widening.
6. Propose a reduced product relevant to probing and frames.
# Robust Numerics and Computational Geometry
> **Learning objectives.** The reader should be able to distinguish topological predicates from metric constructions, use exact or adaptive predicates, apply interval enclosures, and identify failure modes of floating-point geometry.
## 24.1 Why geometric bugs are discontinuous
A small floating-point error in a distance often causes a small distance error. A small error in a sign predicate can change topology completely: two contours connect instead of remaining separate, a polygon changes orientation, or an intersection is missed.
Computational geometry therefore distinguishes:
- **predicates**, which decide discrete facts such as orientation or intersection;
- **constructions**, which compute coordinates.
Predicates deserve stronger numerical methods.
## 24.2 Orientation predicates
For points $a,b,c$ in 2D, orientation is the sign of:
$$
\operatorname{orient2d}(a,b,c)=
(b_x-a_x)(c_y-a_y)-(b_y-a_y)(c_x-a_x).
$$
Near collinearity, floating-point cancellation can return the wrong sign. Adaptive exact predicates evaluate cheaply in ordinary cases and increase precision only near degeneracy [R22].
Use robust predicates for:
- polygon orientation;
- segment intersection;
- point-in-polygon decisions;
- Delaunay or Voronoi topology;
- contour stitching;
- mesh adjacency and ray intersections.
## 24.3 Exact topology, approximate geometry
A practical architecture can keep topology exact while allowing bounded approximate coordinates. For grid-generated contours, use grid-edge identifiers rather than re-quantized endpoint coordinates. For polygon kernels, use integer-scaled coordinates within a proven range or exact rational predicates.
The endpoint-key failure discussed later is a violation of this principle: a lossy packed coordinate is used as topological identity.
## 24.4 Interval arithmetic
An interval $[a,b]$ represents every real number between its endpoints. Arithmetic operations use outward rounding so the exact result is enclosed. IEEE 1788.1 specifies interval arithmetic over binary floating-point endpoints [R23]; Moore, Kearfott, and Cloud provide a broad treatment of interval analysis [R24].
If:
$$
x\in[a,b],\quad y\in[c,d],
$$
then:
$$
x+y\in[a+c,b+d]
$$
with outward-rounded endpoints. Multiplication takes the min and max of all endpoint products.
Intervals can bound:
- curve coordinates over a parameter range;
- transform uncertainty;
- distance to a surface;
- polynomial extrema;
- swept-volume occupancy;
- numerical residuals.
## 24.5 The dependency problem
Interval arithmetic can overestimate when the same variable appears repeatedly. For $x\in[0,1]$:
$$
x-x=[-1,1]
$$
under naive interval evaluation, although the true result is zero. Subdivision, affine arithmetic, Taylor models, or symbolic simplification can improve tightness.
An inconclusive wide interval is not a false result. The checker can subdivide or reject.
## 24.6 Conservative meshing
A triangle mesh is often treated as exact geometry, but it approximates a design surface. A certificate should record:
- source artifact hash;
- tessellation tolerance;
- orientation and watertightness status;
- whether the mesh encloses or is enclosed by the intended solid;
- repairs performed;
- unresolved non-manifold or self-intersection issues.
Without an enclosure relation, mesh-based collision checks prove facts about the mesh, not necessarily the intended CAD solid.
## 24.7 Tolerance and topology
Using one epsilon everywhere is dangerous. Distinct tolerances are needed for:
- numeric comparison;
- geometric construction;
- topological snapping;
- machining allowance;
- certification bound.
A topological snap modifies geometry. Its displacement must be recorded and charged to an error budget.
## 24.8 Worked example: collision of two nearly touching paths
Suppose a line passes $2\,\mu$m from a fixture in nominal double precision, while tool-radius uncertainty is $5\,\mu$m and frame uncertainty is $10\,\mu$m. An exact floating-point distance does not make the move safe. The relevant outer enclosure intersects the obstacle. Numerical exactness and physical robustness are different dimensions.
## 24.9 Exercises
1. Compute `orient2d` for three nearly collinear points and explain cancellation risk.
2. Distinguish a predicate from a construction.
3. Give a use of interval subdivision in curve bounding.
4. Explain the interval dependency problem.
5. Design metadata for a mesh enclosure claim.
6. List four different tolerances in a CAM compiler and their roles.
7. Explain why exact arithmetic does not eliminate model uncertainty.
# Swept Volumes, Stock Models, and Collision Proofs
> **Learning objectives.** The reader should be able to define swept volume, choose conservative stock representations, distinguish cutting from holder collision, and formulate no-gouge and guaranteed-removal claims.
## 25.1 Swept volume
For a tool solid $T$ and pose trajectory $x(t)$, the swept volume is:
$$
\operatorname{Sweep}(T,x)=\bigcup_{t\in[0,T]}x(t)T.
$$
Swept-volume computation is central to collision detection, stock simulation, and manufacturing verification [R26]. Exact computation is difficult for general geometry and trajectories, so practical systems use conservative enclosures or discrete representations.
## 25.2 Stock evolution
For cutting command $i$ with removed volume $R_i$:
$$
S_{i+1}=S_i\setminus R_i.
$$
A simulator may approximate $R_i$ using the swept cutting geometry. The semantic distinction among commands remains important:
- cut updates stock;
- traverse must not update stock;
- probe ideally stops at first contact and may touch without intended removal;
- tool change and dwell preserve stock.
If a missing traverse is silently converted to a cut, the stock semantics change, not merely the visualization.
## 25.3 Tool versus holder
Let $T_c$ be cutting geometry and $T_a$ the full assembly. Then:
**No target gouge:**
$$
\operatorname{Sweep}(T_c,x)^+\cap P_{protected}=\varnothing.
$$
**No fixture collision:**
$$
\operatorname{Sweep}(T_a,x)^+\cap O^+=\varnothing.
$$
**Guaranteed removal:**
$$
R_{required}\subseteq \operatorname{Sweep}(T_c,x)^-.
$$
The superscripts indicate outer and inner enclosures.
## 25.4 Dexel and voxel models
A dexel model stores material intervals along parallel rays. A height field stores one surface value per XY cell and cannot represent undercuts or multiple layers. Triple-dexel models use three orthogonal directions and improve surface representation [R27, R28]. Voxels represent occupancy in three dimensions.
Tradeoffs include:
- memory;
- update speed;
- ability to represent overhangs and cavities;
- surface error;
- ease of conservative enclosure;
- suitability for cutter contact.
For a three-axis no-overhang part, a height field can be efficient, but its resolution must be connected to a continuous-domain bound.
## 25.5 A grid size is not a guarantee
Sampling motion at spacing $h$ and stock on a grid of cell size $g$ does not by itself prove “verified to $\max(h,g)$.” A narrow fixture or brief penetration can occur between samples.
A sound cell method needs one of:
- conservative occupancy of every cell touched by the continuous sweep;
- interval bounds over each cell and motion interval;
- a Lipschitz bound plus adaptive subdivision;
- exact primitive sweep tests;
- a certified distance-field enclosure.
Otherwise, label the result simulation-only.
## 25.6 Configuration-space collision
For fixed orientation, configuration-space obstacles reduce moving-solid collision to point-path collision [R25]:
$$
O_C=O\oplus(-T_a).
$$
A clearance checker can build an outer enclosure $O_C^+$ and prove that the tool-reference path is separated by a positive bound.
For rotating tools or multi-axis orientation, configuration space has more dimensions and the expansion varies with orientation.
## 25.7 Continuous path checking
Lines and arcs often admit analytic bounds. Splines and sampled paths can be recursively subdivided. A generic branch-and-bound checker operates on parameter intervals:
1. Bound path positions over interval $I$.
2. Expand by tool assembly and uncertainty.
3. If disjoint from obstacle enclosure, accept $I$.
4. If definitely intersecting, return a counterexample interval.
5. Otherwise subdivide until a limit.
6. If the limit is reached unresolved, return inconclusive.
This produces honest coverage of the continuous parameter domain.
## 25.8 Worked example: rapid through stock
A rapid from A to B at low Z is safe only if the entire outer swept assembly is disjoint from current stock and fixtures. Checking endpoints misses an obstacle between them. Checking sampled points can miss a thin wall. A segment-versus-expanded-obstacle test or conservative recursive enclosure addresses the whole move.
## 25.9 Exercises
1. Write set formulas for no-gouge, fixture collision, and guaranteed removal.
2. Compare height fields, dexels, triple dexels, and voxels.
3. Explain why one grid resolution cannot be attached blindly to all claims.
4. Design a recursive continuous collision checker.
5. Give a case where cutting geometry is clear but holder geometry collides.
6. Explain how stock state affects link verification.
# Error Budgets and Quantitative Refinement
> **Learning objectives.** The reader should be able to construct typed error budgets, compose bounds through passes, allocate tolerances, and distinguish numerical, model, calibration, and process uncertainty.
## 26.1 A budget is a proof structure
An error budget is not merely a UI sum. It records how a final bound follows from component bounds under explicit propagation rules.
Sources include:
- design-surface tessellation;
- tool geometry approximation;
- tool dimension tolerance and runout;
- path planning discretization;
- curve fitting and linearization;
- coordinate transform uncertainty;
- numeric rounding;
- controller interpolation;
- servo following error;
- probing and calibration;
- thermal and material effects.
Some are compiler-controlled; others are runtime assumptions.
## 26.2 Typed metrics
```ts
type ErrorBound =
| { metric: "hausdorff-position"; frame: FrameId; value: Mm }
| { metric: "normal-surface"; surface: Hash; value: Mm }
| { metric: "max-gouge-depth"; target: Hash; value: Mm }
| { metric: "transform-translation"; transform: Hash; value: Mm }
| { metric: "transform-rotation"; transform: Hash; value: Radians }
| { metric: "axis-following"; axis: AxisId; value: Mm };
```
Only compatible bounds can be combined directly. Rotational error becomes positional error only after multiplying by a radius or applying a more precise transform bound.
## 26.3 Budget allocation
Suppose a feature tolerance is $0.05$ mm. The compiler may allocate:
```text
CAD tessellation 0.010 mm
planning and refinement 0.012 mm
postprocessor rounding 0.003 mm
frame and probing 0.010 mm
machine following 0.010 mm
reserve 0.005 mm
```
This allocation is meaningful only if each number is a valid bound in a compatible metric and the composition theorem supports addition. A planner that consumes more than its allocation must refine or fail.
## 26.4 Correlation and worst-case composition
Worst-case scalar addition is conservative when errors can align. Root-sum-square composition assumes statistical independence and a probabilistic interpretation; it is not a deterministic maximum bound. Certificates must identify whether a claim is worst-case, probabilistic, empirical, or nominal.
## 26.5 Pass amplification
A small angular error $\delta\theta$ at radius $r$ creates positional error approximately $r\delta\theta$. An offset operation can amplify boundary error near sharp corners or topology changes. A coordinate transform with scale should not exist in rigid machining frames, but a calibration map may have local condition numbers.
Each pass needs a sensitivity or Lipschitz bound when it propagates prior error.
## 26.6 Residual-driven refinement
An adaptive algorithm should report a residual related to the claimed metric. For a height field, comparing neighboring samples is not automatically a surface-error residual. A useful refinement loop is:
```text
propose approximation
compute certified local bound
if bound <= allocated budget: accept cell
else if subdivision limit not reached: subdivide
else: inconclusive
```
The residual, subdivision depth, and unresolved regions become evidence.
## 26.7 Runtime budgets
Some budget components are checked at runtime. A tool measurement may tighten diameter uncertainty; a probe sequence may establish a frame bound; a machine calibration record may establish following-error limits. If live bounds exceed the bundle allocation, execution is refused or the job is recompiled.
## 26.8 Worked example: final surface error
Suppose:
- target mesh outer deviation: $0.008$ mm;
- drop-cutter field bound: $0.012$ mm;
- arc fitting: $0.004$ mm;
- output rounding: $0.001$ mm;
- frame translation: $0.010$ mm;
- angular frame uncertainty: $0.0002$ rad at 50 mm radius, contributing $0.010$ mm.
A conservative additive position bound is $0.045$ mm if the metrics and directions align. If the requested bound is $0.04$ mm, the program is not certified merely because each individual pass met its local default.
## 26.9 Exercises
1. Classify six error sources as numerical, model, calibration, or process uncertainty.
2. Convert an angular bound to a positional bound at a given radius.
3. Explain when root-sum-square composition is inappropriate.
4. Design a typed budget for a planar pocket floor.
5. State a residual-driven refinement algorithm.
6. Explain how a runtime measurement can discharge a compile-time assumption.
# Certificate Schemas and Proof Graphs
> **Learning objectives.** The reader should be able to write precise claims, bind them to artifacts and assumptions, organize dependencies as a DAG, and avoid ambiguous status labels.
## 27.1 A certificate is a graph of propositions
A certificate should not be one boolean or one table of reassuring labels. It is a graph connecting artifacts, assumptions, claims, evidence, and checkers.
{width=86%}
A change to any dependency invalidates downstream claims.
## 27.2 Structured claims
```ts
interface Claim {
id: ClaimId;
subject: ArtifactRef;
proposition: StructuredPredicate;
result:
| "proved-exact"
| "proved-bounded"
| "translation-validated"
| "exhaustive-finite-check"
| "simulation-only"
| "assumed"
| "unknown"
| "refuted";
method: MethodRef;
assumptions: readonly AssumptionRef[];
evidence: readonly EvidenceRef[];
dependencies: readonly ClaimId[];
bound?: ErrorBound;
checker: CheckerIdentity;
}
```
The proposition is not a string such as `"gouge"`. It is structured:
```ts
{
kind: "max-penetration",
sweptArtifact: "sha256:...",
protectedTarget: "sha256:...",
maximum: mm(0.02),
metric: "signed-normal-depth",
}
```
## 27.3 Results and methods are orthogonal
“Checked to resolution” combines method and conclusion. Separate:
- proposition;
- method;
- result;
- quantitative bound;
- coverage;
- assumptions.
A sampled simulation method may produce a counterexample and thus refute a claim. Failure to find a counterexample does not upgrade it to proof.
## 27.4 Assumption records
```ts
interface Assumption {
id: AssumptionId;
proposition: StructuredPredicate;
source: "operator" | "calibration" | "machine-attestation" | "library";
evidence?: ArtifactRef;
validFrom?: Timestamp;
validUntil?: Timestamp;
runtimeCheck?: RuntimeCheckSpec;
}
```
Examples:
- tool T1 diameter lies in $[3.170,3.180]$ mm;
- fixture model hash matches setup QR code;
- machine firmware belongs to a compatible semantic profile;
- G54 transform lies inside an interval;
- stock dimensions meet a measured bound.
## 27.5 Evidence types
```ts
type Evidence =
| AbstractInterpretationTrace
| IntervalSubdivisionTree
| CollisionSeparationWitness
| CoverageWitness
| ParseBackTraceComparison
| SolverCertificate
| ModelCheckingTrace
| Counterexample
| CalibrationRecord
| SignatureAttestation;
```
Evidence schemas should be stable, versioned, and independently checkable.
## 27.6 Claim granularity
Separate claims by meaning:
- target no-gouge;
- fixture collision;
- holder collision;
- rapid-through-stock;
- required removal;
- machine travel;
- feed and dynamics;
- modal equivalence;
- final spindle stop;
- exact upload hash;
- controller start acknowledgement.
One generic evidence object should not be able to mint unrelated rows. Strong typing can enforce this:
```ts
function certifyGouge(
claim: GougeClaim,
evidence: GougeEvidence,
): CertifiedClaim;
```
## 27.7 Completeness policy
A bundle policy states which claims are required for a use class:
```text
Preview-only:
schema, finite values, parse success
Attended air cut:
travel, controller parse-back, exact bytes, runtime identity
Attended material cut:
+ target, fixture, holder, stock, tool and WCS assumptions
Unattended production:
+ protocol liveness, runtime monitor, calibrated dynamic bounds,
recovery and interlock claims
```
A function such as `isFullyVerified` must derive from explicit policy, not from absence of severe diagnostics.
## 27.8 Worked example: false evidence reuse
Suppose a dexel simulation checks low rapids and spoilboard penetration but receives no target surface. It can support:
```text
rapid-through-current-stock sampled simulation
spoilboard penetration sampled simulation
```
It cannot support:
```text
maximum gouge into protected target <= 0.02 mm
```
because the proposition's target artifact is absent. A schema that requires `protectedTargetHash` and target-specific evidence prevents the incorrect promotion.
## 27.9 Exercises
1. Write a structured claim for machine travel.
2. Design separate evidence types for rapid collision and target gouge.
3. Explain why a digital signature is not a semantic proof.
4. Define a completeness policy for an attended air cut.
5. Draw a dependency graph for an arc-linearized final job.
6. Describe certificate invalidation after a tool change.
# Trusted Checkers and Proof-Carrying CAM
> **Learning objectives.** The reader should be able to minimize a trusted computing base, explain proof-carrying code, design producer-consumer separation, and evaluate checker independence.
## 28.1 The producer is complicated
CAM planners use spatial indices, heuristics, solvers, floating-point kernels, caches, parallelism, and UI state. Treating this entire implementation as trusted makes assurance fragile.
Proof-carrying code separates an untrusted producer from a consumer-side checker: code arrives with evidence that it satisfies a policy, and the consumer validates the evidence before execution [R20]. Foundational proof-carrying code reduces reliance on specialized verification-condition generators by grounding evidence in a smaller logic [R21].
The analogous CAM architecture is:
```text
complex planner / optimizer / postprocessor
|
v
artifact + evidence
|
v
small independent checker
|
accept or reject
```
## 28.2 Trusted computing base
A realistic trusted base includes:
- definitions of claim predicates;
- canonical artifact hashing and serialization;
- independent parsers and semantic interpreters;
- robust numeric primitives used by checkers;
- certificate dependency validation;
- runtime identity and upload-hash handshake;
- a small execution monitor;
- explicitly accepted physical assumptions.
The UI, heuristic planners, optimizers, and preview renderer should not need to be trusted.
## 28.3 Independence
A checker that calls the same buggy helper as the producer is not strongly independent. Independence can be improved by:
- separate implementations;
- different algorithms or representations;
- reduced feature set;
- smaller codebase;
- strict schemas;
- deterministic behavior;
- extensive property and differential testing;
- optional mechanized proofs for critical kernels.
Independence is a spectrum, not a binary property.
## 28.4 Proof objects versus recomputation
A checker can:
1. recompute the property independently;
2. verify a compact witness;
3. check a formal proof term;
4. combine these methods.
For contour coverage, a cell decomposition witness may be cheaper than re-running planning. For modal equivalence, replaying both programs is simple. For a linear or mixed-integer optimizer, a solver certificate or dual bound may support optimality.
## 28.5 Checker resource bounds
Evidence can be adversarial or malformed. Checkers need:
- schema validation;
- size and recursion limits;
- deterministic resource bounds;
- integer overflow protection;
- denial-of-service resistance;
- explicit version compatibility;
- no execution of producer-supplied code.
## 28.6 Compositional certificates
If pass $P_1$ establishes $R_1(A,B)$ and $P_2$ establishes $R_2(B,C)$, a composition theorem establishes $R(A,C)$:
$$
R_1(A,B)\land R_2(B,C)\Longrightarrow R(A,C).
$$
The theorem may accumulate quantitative bounds. Certificate composition should be implemented by a checker, not inferred from matching stage names.
## 28.7 Mechanization strategy
Formalize the small semantic core first:
- canonical command semantics;
- controller modal semantics;
- pass-relation composition;
- certificate validity;
- state-machine authorization;
- numeric lemmas for common primitives.
Leave complex search algorithms unverified but validated. This yields more assurance per unit effort than attempting to prove an entire CAM application at once.
## 28.8 Worked example: validating a solver schedule
An untrusted optimizer returns operation order $\pi$, path orientations, total cost $J$, and a lower bound $L$. The checker verifies:
1. $\pi$ is a permutation of required operations;
2. all precedence edges are respected;
3. every selected orientation is legal;
4. each transition cost is recomputed;
5. total cost equals the sum;
6. the lower-bound certificate is valid;
7. the reported gap $(J-L)/L$ is correct.
The optimizer's internal search does not enter the trusted base.
## 28.9 Exercises
1. List the trusted components in a minimal CAM checker.
2. Give an example where a checker is insufficiently independent.
3. Compare recomputation with witness checking.
4. Design resource limits for a certificate checker.
5. State a composition theorem for two bounded geometric passes.
6. Choose three components suitable for formal mechanization and justify them.
# Temporal Semantics and Controller Protocols
> **Learning objectives.** The reader should be able to model the host-controller interaction as a state machine, state safety and liveness properties, and reason about ambiguous failures and authorization races.
## 29.1 The protocol is part of the compiler target
A final G-code file is useless unless the correct bytes are transferred, stored, selected, and executed. The controller interface is therefore part of the compilation and deployment semantics.
{width=96%}
## 29.2 States and transitions
A controller model should include states such as:
- disconnected;
- connected but unidentified;
- idle;
- uploading;
- ready with a specific stored hash;
- running a specific execution instance;
- held;
- stopped;
- alarmed;
- ambiguous or quarantined after timeout.
Transitions have guards and effects. `Resume` is not a read-only command; it enables motion. `FeedHold` is a stop-class action and should remain available even when ordinary command admission is blocked.
## 29.3 Safety properties
Examples:
$$
\Box(\operatorname{Running}(h)\Rightarrow
\operatorname{Authorized}(h)).
$$
$$
\Box(\operatorname{Start}(h)\Rightarrow
\operatorname{StoredHash}=h).
$$
$$
\Box(\operatorname{Motion}\Rightarrow
\neg\operatorname{Alarm}).
$$
$$
\Box(\operatorname{GenericReadPath}\Rightarrow
\neg\operatorname{MotionEffect}).
$$
The last property requires complete parsing, not prefix classification.
## 29.4 Liveness properties
$$
\Box(\operatorname{UploadStarted}\Rightarrow
\Diamond(\operatorname{Ready}\lor\operatorname{Failed}\lor\operatorname{Quarantined})).
$$
$$
\Box(\operatorname{AbortRequested}\Rightarrow
\Diamond(\operatorname{Stopped}\lor\operatorname{Alarm})).
$$
Liveness depends on assumptions about network delivery, controller scheduling, and machine responsiveness. Those assumptions must be stated.
## 29.5 Atomic admission and execution
A preflight that checks state, releases a lock, and later sends motion has a time-of-check/time-of-use gap. Another command can change the state between admission and execution.
A safer design serializes:
```text
acquire session authority
refresh live state
check preconditions
bind authorization to command/job hash and state epoch
send command
observe acknowledgement or quarantine
release authority
```
The state epoch invalidates admission if intervening events occur.
## 29.6 Ambiguous timeout
After sending a command, a timeout does not imply that the machine did nothing. The command may have executed while the reply was lost. The correct successor state is a set of possibilities. The session should enter an ambiguous/quarantined state until re-synchronized through a trusted status query and protocol boundary.
Blind retry is especially dangerous for motion or state-changing commands.
## 29.7 Message streams and loss
Safety-relevant events should not share a lossy queue designed for UI telemetry. A dropped alarm, completion marker, or protocol sentinel can make the host state inconsistent. Separate durable control events from best-effort display updates.
Partial writes must also be handled. A transport `Write` may write fewer bytes than requested without a fatal error; command framing must loop until complete or fail before execution can be assumed.
## 29.8 Model checking
A finite abstraction of the protocol can be exhaustively checked for invariants and deadlocks. TLA-style specifications are well suited to concurrency and temporal properties [R8, R34]. Hybrid automata extend state machines with continuous dynamics when stop distance and watchdog timing matter [R35].
## 29.9 Worked example: compound command classification
A classifier that examines only the first whitespace token may label:
```text
status\nG0 X100
```
as read-only because `status` is first. The semantic policy concerns every parsed command in the payload. A fail-closed grammar rejects embedded newlines or parses all blocks and proves that every effect belongs to the allowed class.
## 29.10 Exercises
1. Define states and transitions for upload, start, hold, resume, and abort.
2. State three safety and two liveness properties.
3. Explain the time-of-check/time-of-use race in preflight.
4. Model an ambiguous timeout as a set of successor states.
5. Explain why stop commands should bypass ordinary motion admission.
6. Design a fail-closed read-only command grammar.
7. Identify which messages require durable delivery.
# Runtime Assurance and Physical Assumptions
> **Learning objectives.** The reader should be able to bind compile-time evidence to live machine state, design a runtime assurance monitor, and distinguish logical proof from physical validation.
## 30.1 Conditional assurance
A compile-time certificate proves a conditional theorem:
```text
if assumptions A hold, artifact B satisfies claims C
```
Runtime preflight must establish as much of $A$ as possible. The remaining assumptions require operator acceptance, calibration records, or physical interlocks.
## 30.2 Hash-bound execution
{width=88%}
A robust protocol is:
1. Host proposes certified bundle hash $H$ and assumptions $A$.
2. Controller stores exact bytes and reports stored hash $H'$.
3. Controller reports identity, firmware, homing, WCS, tool state, alarm state, and job state $M$.
4. Host verifies $H'=H$ and $M\models A$.
5. Host authorizes one execution instance of $H$.
6. Controller acknowledges start of that exact instance.
7. Host monitors state until terminal completion, abort, or fault.
## 30.3 Runtime checks
Possible checks include:
- machine identity and firmware semantics profile;
- homed axes;
- active work coordinate system and measured transform;
- tool ID, length, and optional diameter measurement;
- fixture/setup identifier;
- stock presence and dimensions;
- door, probe, and accessory interlocks;
- no active alarm;
- exact stored job hash;
- controller idle or permitted paused state;
- calibration validity period.
## 30.4 Runtime assurance monitor
A runtime assurance architecture places a small trusted monitor around a more capable controller or host planner. Simplex-style systems switch to a trusted safety action when an advanced component approaches an unsafe region; modern runtime-assurance frameworks apply this to cyber-physical systems [R36].
For a Z1-class machine, a realistic monitor can enforce:
- authorized state transitions;
- command classes;
- job-hash binding;
- axis and feed envelopes;
- spindle/tool consistency;
- watchdog policy;
- communication-loss behavior;
- explicit confirmation of stop.
## 30.5 Stopping distance and latency
A stop request is not an instantaneous stop. If velocity is $v$ and guaranteed deceleration is $a$, a simple lower bound on stopping distance is:
$$
d_{stop}\ge\frac{v^2}{2a},
$$
plus command, communication, and controller latency. A safety envelope must reserve this distance. Feed hold may preserve the job and decelerate differently from emergency stop or reset.
## 30.6 Physical model validation
Even perfect software cannot prove that the CAD fixture model matches reality. Useful physical validation practices include:
- setup identifiers and photographs;
- measured stock and tool records;
- probing routines with uncertainty;
- air cuts and reduced-feed first runs;
- witness marks or sacrificial stock;
- calibration artifacts;
- independent inspection of critical dimensions;
- bounded validity periods for calibration.
These produce assumptions and attestations, not mathematical facts from the compiler.
## 30.7 Degradation policies
A runtime system should define what happens when an assumption cannot be established:
- refuse execution;
- downgrade to preview or air-cut mode;
- require explicit operator override with recorded rationale;
- reduce feed and restrict motion envelope;
- re-probe or re-measure;
- recompile with wider uncertainty;
- quarantine the session after ambiguity.
Silent continuation is not a policy.
## 30.8 Worked example: changed G54
A job was certified under work transform $T_0$ with uncertainty set $\Xi$. Before execution, the live controller reports $T_1$. The runtime checker computes whether $T_1$ lies inside the certified set. If not, the travel and collision claims are stale. The correct response is to revalidate or recompile, not to rely on the same file hash.
## 30.9 Design rules
```latex
\begin{warningbox}
A certificate is valid only for the exact artifact and assumption set named by its claims. Live machine identity, tools, frames, setup, and controller state are inputs to execution, not incidental operator details.
\end{warningbox}
```
## 30.10 Exercises
1. Design a runtime assumption manifest for a pocket job.
2. Explain why upload success is weaker than exact-byte execution.
3. Derive stopping distance for a given velocity and deceleration, then add latency distance.
4. List five monitor-enforceable properties and five physical assumptions it cannot prove.
5. Design a degradation policy for an unknown tool measurement.
6. Explain how a changed WCS invalidates geometric certificates.
EOF
wc -l -w -c /mnt/data/z1_textbook_work/book/Certificate_Carrying_CAM_Compilers.md
```
💭 Thinking
**Drafted contract, CAM, architecture, appendix, and implementation chapters**
💭 Thinking
**Appended appendices and selected exercise solutions to textbook**
💭 Thinking
**Building the reference list**
I’m reconciling publication details, correcting uncertain entries, and assembling a reliable bibliography covering semantics, verification, geometry, optimization, runtime assurance, and the project’s implementation context.
**Searched 2 websites**
💭 Thinking
**Inspected textbook files, headings, references, and citation numbers**
💭 Thinking
**Searched 6 websites**
💭 Thinking
**Audited textbook appendix headings and citations for references R42 and R43**
💭 Thinking
**Searched 16 websites**
💭 Thinking
**Appended glossary and reading paths**
💭 Thinking
**Searched 13 websites**
💭 Thinking
**Read PDF skill instructions**
💭 Thinking
**Built and validated textbook PDF with font and figure adjustments**
💭 Thinking
**Rebuilt and validated the textbook PDF with corrected headings and references**
💭 Thinking
**Packaged final textbook deliverables and source bundle**
💭 Thinking
**Inspected PDF guidelines and existing deliverables**
**Reconstructing textbook materials**
I’m inferring that the earlier deliverables aren’t available in the current workspace. I’ll inspect the available archive and use the conversation’s existing outline and content to rebuild the four-chapter textbook.
**Reconstructed textbook materials**
**Designing the textbook**
I’m consolidating the material into four substantial chapters with learning goals, definitions, examples, counterexamples, implementation guidance, exercises, diagrams, and a capstone project, while avoiding unnecessary fragmentation.
**Designed the textbook**
💭 Thinking
**Inspected Dropcut/Z1 sources, documentation headings, and TypeScript files**
**Planning the textbook**
I’m building a substantial four-chapter textbook around semantics, compiler architecture, certification, controller modeling, validation, and implementation. I’ll use a running machining example, diagrams, exercises, solutions, and a capstone.
**Planned the textbook**
**Structuring verification topics**
I’m organizing the second half around witness translation, provenance, IR lowering, testing, geometry, uncertainty, planning, Hoare logic, abstract interpretation, certificates, controller invariants, and runtime assurance.
**Structured verification topics**
💭 Thinking
**Inspected Dropcut Studio source architecture**
💭 Thinking
**Created pedagogical figures and drafted CAM compiler textbook front matter**
💭 Thinking
**Updated and audited verified motion planning textbook content and glossary definitions**
💭 Thinking
**Patched chapter definitions and normalized Markdown formatting anomalies**
💭 Thinking
**Compiled and refined Markdown textbook PDF with Pandoc**
💭 Thinking
**Rendered, inspected, rebuilt, and validated the textbook PDF and manuscript bundle**
💭 Thinking
**Packaged revised pedagogical textbook deliverables**