Struct DeclassifyStep 

pub struct DeclassifyStep {
    pub class: String,
    pub source: String,
    pub output_type: String,
    pub shield: String,
    pub loc: Loc,
}

v4.5.0 — declassify <Class> from <source> -> <Type> via <Shield>.

Retiring a class is an ACT, not an inference. The compiler does not decide that a value stopped being PHI; someone declares it, and the compiler refuses the declaration when it is structurally impossible — when the destination type still carries the class being retired.

The class is NAMED at the site rather than left to the shield, so a reader of the flow sees what was retired without going to look it up.

Fields

class: String

The regulatory class being retired. One per statement: retiring two classes is two acts, and collapsing them would hide which control justified which.

source: String

The value entering the operation.

output_type: String

The DECLARED TYPE the value leaves as. It must be a different type, because the type is the only thing a boundary reads.

shield: String

The shield that authorises this. It must declare the class in its own declassifies: — retiring a class is a capability, not a side effect of scanning.

loc: Loc

Trait Implementations

impl Debug for DeclassifyStep

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl Default for DeclassifyStep

fn default() -> DeclassifyStep

Returns the “default value” for a type.