Type invariants

[tjhance]

Background

It's very common to have types to have "well-formedness" predicates that need to be carried around everywhere, usually called wf(&self) or well_formed(&self) or similar.

It would be ideal to make these automatic so that we don't have to manually cart around the predicates everywhere, especially when 'wf' is 'closed'. Having these be automatic also makes it easier to use generic code (so the generic code doesn't have to reason about the well-formedness of its types) and makes it possible to specify "safe APIs" that rely on internal type invariants.

Broken invariants

One of the challenges with the feature is how to handle temporarily-broken invariants.

Suppose we wanted to do:

struct X { a: u64, b: u64 };
  with invariant (a == b)

We might want to write a function where the invariant is temporarily broken and restored at the end:

fn stuff(x: &mut X) {
  assert(x.a == x.b);

  x.a = 5;
  // Invariant is broken at this point
  x.b = 5;

  // Invariant is restored
  assert(x.a == x.b);
}

Ordinarily, this wouldn't be an issue using the existing idiom of just putting x.wf() in the precondition and postcondition.

Doing this soundly is somewhat difficult; as I understand it, it's especially nontrivial in the presence of &mut and prophecies.

However, I observe that we already have a sound way to handle temporarily broken invariants, which is the mask system we use for AtomicInvariant & LocalInvariant. Using this, it's possible to "encode" temporarily broken invariants if you already have always-on invariants.

The idea is to have an "invariant switch" that can enable or disable the invariant:

struct X {
  a: u64,
  b: u64,
  ghost invariant_is_enabled: bool,
};
with invariant (invariant_is_enabled ==> a == b)

// Now we never need to break the invariant.

fn stuff(x: &mut X) {
  proof { x.invariant_is_enabled = false; }
  x.a = 5;
  x.b = 5;
  proof { x.invariant_is_enabled = true; }
}

There's a problem here, which is that now we need to cart around the predicate x.invariant_is_enabled == true, which defeats the whole point. However, if were to treat the 'invariant_is_enabled' flag as a special Verus built-in thing, then Verus's mask system could serve as a lightweight way to disable the invariants.

fn stuff(x: &mut X)
  opens_invariants [ type_invariant_for_X ],
{
  disable_invariants!{
    assert(x.a == x.b);

    x.a = 5;

    stuff(&mut *x); // Not allowed

    x.b = 5;
  }
}

In fact, it's already possible to encode something like this using ghost objects:

struct X {
  a: u64,
  b: u64,
  tracked invariant_is_enabled: StructXInvariantEnablerToken,
};
with invariant (invariant_is_enabled.value ==> a == b)

fn stuff(x: &mut X, tracked controller_inv: &LocalInvariant<StructXGlobalInvariantController>)
    opens_invariants [ controller_inv.namespace() ],
{
    open_local_invariant!(controller_inv, controller_token => {
        // The 'controller_inv' local invariant ensures controller_token has everything enabled
        assert(controller_token.everything_is_enabled());
        // So we can learn that 'x' is enabled:
        proof {
            learn_is_enabled(&controller_token, &x.invariant_is_enabled);
            assert(x.invariant_is_enabled.value);
        }

        assert(x.a == x.b); // This is true because we just learned the invariant holds.

        // We can 'disable' x:
        proof {
            disable(&mut controller_token, &mut x.invariant_is_enabled);

            // This is recorded in the controller
            assert(controller_token.one_object_is_disabled());
            assert(x.invariant_is_enabled.value == false);
        }

        x.a = 5;

        // Technically, the invariant for 'x' still holds, because x.invariant_is_enabled.value == false

        x.b = 5;

        // Re-enable invariant:
        proof {
            enable(&mut controller_token, &mut x.invariant_is_enabled);

            assert(controller_token.everything_is_enabled());
            assert(x.invariant_is_enabled.value == true);
        }

        // Can close out the open_local_invariant block out here
        // because the controller_token says everything is enabled
   });
}

I'm not saying we should actually do it like this, this is really cumbersome and involves lugging around a lot of ghost state. But I think we could use this as a sort of template for designing a more lightweight system.

Conclusion

I haven't made a concrete design for anything, but I propose that the design problem can be divided into roughly orthogonal components:

• Design a type-invariant system for invariants that must be enabled always, at every program point.
  • How does the user specify their invariant? Should we have a fixed function name, or an attribute that can be applied to any boolean function?
  • How does it work with &mut references? (this is still nontrivial, I think)
  • Where do we insert asserts and assumes in AIR?
• Design a system for temporarily breaking invariants, based on the mask system, which is analogous to the encoding above, but more convenient.
  • Does disabling work on a per-type basis or a per-object basis?
  • How do we name the invariants?
  • Determine priority for this feature - what are the use-cases?

[parno]

FWIW, VCC allows you to associate a type invariant with a type definition, and it can be a one- or two-state predicate. I think you can rely on the invariant if you know the object is closed, but you can also choose to open it to temporarily violate the invariant. That of course adds a fair bit of boilerplate for the common case where you don't want to open the invariant.

Chalice has a Java-like notion of certain classes being designated as "monitors" which have a monitor invariant that can hold onto implicit-dynamic-frame permissions. Hence this behaves like a lock invariant in Verus.

[tjhance]

The open/closed sounds a lot like the invariant_is_enabled switch in my example above.

How does VCC track the open/closedness of an object's invariant?

[parno]

It's been a while since I looked, but I think you might have to explicitly say requires closed(obj)

[parno]

FWIW, it looks like Dominik Stolz wrote an MS thesis about type invariants in Creusot, which might be relevant.