pub struct IrRuleMetadata {Show 25 fields
pub fact_reads: Vec<String>,
pub projection_reads: Vec<IrProjectionRead>,
pub fact_writes: Vec<String>,
pub record_sources: Vec<IrRecordSource>,
pub fact_consumes: Vec<String>,
pub effects: Vec<IrEffectNode>,
pub dependencies: Vec<IrEffectDependency>,
pub region: Option<IrRegion>,
pub case_branches: Vec<IrRuleCaseBranch>,
pub terminal_outputs: Vec<IrTerminalOutput>,
pub terminal_branches: Vec<IrTerminalCaseBranch>,
pub terminal_completes: Vec<String>,
pub redactions: Vec<IrRedaction>,
pub egress_payload_reads: BTreeMap<String, BTreeSet<String>>,
pub declassified_roots: BTreeSet<String>,
pub endorsed_roots: BTreeSet<String>,
pub endorsed_claim_items: BTreeSet<String>,
pub record_field_reads: BTreeMap<String, BTreeMap<String, BTreeSet<String>>>,
pub coerce_input_roots: BTreeMap<String, BTreeSet<String>>,
pub after_aliases: BTreeMap<String, String>,
pub egress_case_influence: BTreeMap<String, BTreeSet<String>>,
pub complete_field_reads: BTreeMap<String, BTreeMap<String, BTreeSet<String>>>,
pub milestone_field_reads: BTreeMap<String, BTreeMap<String, BTreeSet<String>>>,
pub bounded_egresses: Vec<IrBoundedEgress>,
pub max_after_depth: usize,
}Fields§
§fact_reads: Vec<String>§projection_reads: Vec<IrProjectionRead>§fact_writes: Vec<String>§record_sources: Vec<IrRecordSource>§fact_consumes: Vec<String>§effects: Vec<IrEffectNode>§dependencies: Vec<IrEffectDependency>§region: Option<IrRegion>DR-0043: the rule’s during/until region (at most one in v1).
case_branches: Vec<IrRuleCaseBranch>§terminal_outputs: Vec<IrTerminalOutput>§terminal_branches: Vec<IrTerminalCaseBranch>§terminal_completes: Vec<String>The output bindings this rule completes (the name of each complete <binding> {…} in the body, recursing into after/case/branch/handler blocks).
Surfaced for the information-flow checker: a complete result returns a value
to the workflow’s invoker, an egress sink at the invoker boundary (DR-0030 X2).
IFC-only — deliberately NOT rendered in the .ir snapshot, so it adds no
golden/hash churn.
redactions: Vec<IrRedaction>The redact <source> keep [..] as <out> projections in this rule body
(recursing into after/case/branch/handler blocks). Surfaced for the
information-flow value-flow engine: a redaction is the explicit crossing at
which the rule-level opaque join box is refined — the projected binding
carries only the kept fields’ labels (DR-0027, proven in
models/lean/Whipple/Redaction.lean). IFC-only — NOT rendered in the .ir
snapshot, so it adds no golden/hash churn.
egress_payload_reads: BTreeMap<String, BTreeSet<String>>Per egress sink, the set of binding roots its payload references (union
across branches), keyed by the sink string the IFC engine uses: a complete <binding> by its binding, a record <Schema> by fact:<Schema>, a send via <channel> by the channel. IFC-only (NOT in the .ir snapshot). The engine
uses this to recognize a FULLY-REDACTED egress — one whose payload references
only redaction outputs — and govern its leak check by the projection’s
per-field label rather than the rule’s whole read set (DR-0027 redact, the
static refinement).
declassified_roots: BTreeSet<String>The output roots of coerce … declassified crossings in this rule: the
coerce’s binding plus its after <binding> succeeds|completes as <alias>
aliases (the names an egress payload actually references). The IFC engine
waives the read×sink leak check for an egress carried ENTIRELY by these
roots when a matching grant declassify covers the sink (DR-0027
I-IFC3 — grants authorize marked crossings only). IFC-only (NOT in the
.ir snapshot).
endorsed_roots: BTreeSet<String>The endorsed dual of declassified_roots: output roots of coerce … endorsed crossings, and (DR-0051 §2) the claimed item of claim … endorsed crossings. Consulted by the inject check. IFC-only (NOT in the
.ir snapshot).
endorsed_claim_items: BTreeSet<String>DR-0051 §3: the item bindings of claim … endorsed effects — the
names a when <tracker> has ready issue as <binding> trigger bound, not
the claim’s own as binding.
Carried separately from endorsed_roots because the two answer different
questions. endorsed_roots says which values crossed; this says which
queue the crossing drew its authority from, so the checker can refuse a
marker whose tracker nobody vouched. IFC-only (NOT in the .ir
snapshot).
record_field_reads: BTreeMap<String, BTreeMap<String, BTreeSet<String>>>DR-0051 §4: per-field binding roots for each record <Schema> { … }
egress — the same shape as complete_field_reads, keyed by
fact:<Schema> and then by field name.
egress_payload_reads collapses a record’s roots to one set, which is
enough to decide whether a sink is carried by a marked crossing but not
which field it shaped. §4 needs the finer grain: a verdict field shaped
by an endorsement must be schema-closed, while a sibling field holding a
constant is nobody’s business. IFC-only (NOT in the .ir snapshot).
coerce_input_roots: BTreeMap<String, BTreeSet<String>>Per-coerce argument roots: for EVERY coerce f(args…) as <binding> in
the rule (marked or not), the binding roots its argument expressions
reference. The IFC engine resolves these to governed sources for
input-side provenance narrowing at marked crossings — including chaining
through unmarked coerces (a model call is a total mixing point: its
output carries the join of all its inputs). IFC-only (NOT in the .ir
snapshot).
after_aliases: BTreeMap<String, String>after <effect-binding> succeeds|completes as <alias> → the effect
binding, so the IFC engine can resolve payload and argument roots
through the aliases bodies actually reference. IFC-only (NOT in the
.ir snapshot).
egress_case_influence: BTreeMap<String, BTreeSet<String>>Per egress sink, the binding roots of every enclosing case scrutinee
(DR-0046): a sink inside a case arm is INFLUENCED by the scrutinee —
branching on model output and recording per-arm constants is the
classic implicit channel. Covers record/complete/milestone/send/write
uniformly. IFC-only (NOT in the .ir snapshot).
complete_field_reads: BTreeMap<String, BTreeMap<String, BTreeSet<String>>>Per complete <binding> egress, the binding roots each RESULT FIELD
references — a two-level map binding -> field -> {roots}. Where
egress_payload_reads joins all of a sink’s fields into one set (enough for the
fully-redacted recognizer), this keeps them SEPARATE so the IFC engine can
compute a PER-FIELD flow signature (DR-0030 X2 v2): the reads reaching each
result field, refined at fact granularity. IFC-only (NOT in the .ir
snapshot). Union across branches; a Shorthand field resolves to the
terminal’s from binding.
milestone_field_reads: BTreeMap<String, BTreeMap<String, BTreeSet<String>>>Per emit milestone "<name>" egress, the binding roots each MILESTONE FIELD
references — same shape and purpose as complete_field_reads, but keyed by
milestone name. Milestone payloads are child-to-parent egresses, so IFC needs
their per-field flow signature too (D3′). IFC-only (NOT in the .ir
snapshot). Union across branches.
bounded_egresses: Vec<IrBoundedEgress>Bounded-type projection egresses (record <T> from <src>): each is governed
by the kept fields’ per-field label join, like an explicit redact. IFC-only
(NOT in the .ir snapshot). DR-0027 auto-redaction, the bounded-type reading.
max_after_depth: usizeMaximum nesting depth of after blocks in the rule body (0 = no after,
1 = a top-level after, 2 = an after inside an after, …). Surfaced for the
lint.deep_after_nesting maintainability check.
Trait Implementations§
Source§impl Clone for IrRuleMetadata
impl Clone for IrRuleMetadata
Source§fn clone(&self) -> IrRuleMetadata
fn clone(&self) -> IrRuleMetadata
1.0.0 (const: unstable) · Source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
source. Read more