pub enum BodyStmt {
Record(RecordStmt),
Done {
binding: String,
replacement: Option<RecordStmt>,
span: SourceSpan,
},
Effect(EffectStmt),
After(AfterBlock),
Region(RegionBlock),
Case(CaseBlock),
Terminal(TerminalStmt),
Cancel {
binding: String,
span: SourceSpan,
},
Milestone {
name: String,
payload_class: Option<String>,
fields: Vec<FieldAssign>,
span: SourceSpan,
},
Redact {
source: String,
keep: Vec<String>,
binding: String,
span: SourceSpan,
},
}Variants§
Record(RecordStmt)
Done
done x / done x -> record ... — marks a fact terminal, optionally
replacing it with a record.
Effect(EffectStmt)
After(AfterBlock)
Region(RegionBlock)
Case(CaseBlock)
Terminal(TerminalStmt)
Cancel
Milestone
emit milestone "<name>" of <PayloadClass> { fields } (Family C,
child-milestone lifecycle): a synchronous durable fact the child workflow
projects mid-flight for an observing parent. It is NOT an async effect —
it derives a workflow.milestone:<name> fact in the child’s own base at
rule-commit time, mirroring record. payload_class types the parent’s
after p reaches "<name>" as m binding. See
spec/decision-records/discriminated-families-design.md section 7.3.
Redact
redact <source> keep [<field>, …] as <out> (DR-0027 redact): an explicit,
audited PROJECTION of the record bound to source onto the kept field set,
producing a new binding out. It is the information-flow crossing the
rule-level opaque join box is refined at — the projection carries only the
labels of the KEPT fields (the dropped fields are non-interfering, proven in
models/lean/Whipple/Redaction.lean: canRead_redact). It is NOT an async
effect: it is a synchronous, pure restructure (like a record projection), so
it never becomes an IrEffectKind — it is rule metadata the IFC checker and
the runtime projection both read. out’s type is the source schema projected
to the kept fields (redact.<rule>.<out>); accessing a dropped field on out
is a type error.