Skip to content

Trust Propagation

Trust is propagated across functions through the use of the trust keyword. So for example, if a function is marked with trust at the definition/top-level, like so:

spectre
pub fn danger_func() void = trust {
    // ...
}

Then this function must be explicitly trusted at each of its callsites, or be called from a trusted context. This is somewhat akin to the "unsafe" concept from other languages, however it adopts the inverse semantics and revolves around the DbC verification guarantees rather than generally-dangerous functions.

Trust Blocks

Trust can be applied in blocks, for example:

spectre
trust {
    statement_one()
    statement_two()
    if whatever {
        statement_three()
    }
}

Inline Trust

Trust can be applied inline, too. For example:

spectre
trust some_function()
trust some_other_function()