Engine: introduce an runtime invariant system for phases

[W95Psp]

By type, some phases must be applied before others.

But often, informal invariants are assumed in phases: a phase expects another phase to be already applied.

We could define an ADT that tracks invariants: i.e. NoSideEffectsInFunctionArguments (possibly with validation functions for sanity checks).

Each phase should declare a list of constraints: "I should run after phase X", "I guarantee invariant Y", "I no longer guarantee invariant A", "I run only on ASTs that guarantee invariant Z".

At runtime, composing phases would accumulate constraints, and we will check those constraints progressively at runtime, and run validation functions at each phase for invariants when sanity mode is enabled (e.g. in hax' CI).

[W95Psp]

I'm adding an example of what this system of invariants would look like.

Let's consider the invariant regarding side effects after the SideEffectHoist phase. This phase moves side effects to "shallow" let bindings: side effects may occur only on RHS of let bindings appearing right below a control flow node (function, closure, match, if...). Note that this phase is 500LoC, and is rather complicated while the invariant is small.

Here is how this would look as OCaml code (note: this code probably won't TC):

(** States that side effects (Break, Continue, Assign, Return, `?`) can only occur in two different places:
     - directly on a "control flow node", that is, the body of a function, the body of a loop, the `then` or `else` branch of a `if`, or on a branch of a match;
     - directly on any of the RHS of a sequence of let-bindings on such a "control flow node".
    For example, that means that side effects are forbidden on a function call argument or on the scrutinee of a match.
 *)
module SideEffectOnlyOnCfNode: AST_INVARIANT = struct
  type position =
    [ `CfNode
      (** Body of a loop/closure, or branch of a match/if. Side effects are allowed. *)
    | `ImmediateRhsLetBinding
      (** RHS of a let binding which is directly on a `ControlFlowNode node. Side effects are allowed. *)
    | `DeepNode
      (** Deeply nested node within an expression. Side effects are forbidden. *)
    ]
  (** Tracks nodes in the AST: are we just below a control flow? *)

  let side_effects_only_on_cf_nodes =
    object
      inherit Ast_visitors.iter as super

      method visit_expr position e =
        match e.e with
        | Loop { body; kind; state; _ } ->
            (* The body is a `CfNode node *)
            super#visit_expr `CfNode body;
            (* The loop kind and state are "deep" nodes *)
            super#visit_loop_kind `DeepNode kind;
            Option.iter ~f:(super#visit_loop_state `DeepNode) kind
        | Closure { body; _ } ->
            (* The body of a closure is a `CfNode node *)
            super#visit_expr `CfNode body
        | If { cond; then_; else_ } ->
            self#visit_expr `DeepNode cond;
            self#visit_expr `CfNode then_;
            Option.iter ~f:(self#visit_expr `CfNode) else_
        | (Break _ | Continue _ | Assign _ | Return _ | QuestionMark _)
          when [%matches? `DeepNode] position ->
            (* If an invariant is detected on a deeply nested node, we raise an exception *)
            raise InvariantBroken
        | Let _ when [%matches? `CfNode] position ->
            (* Collect all immediate let bindings *)
            let lbs, ret = collect_let_bindings e in
            (* Visit them as `ImmediateRhsLetBinding nodes *)
            List.iter
              ~f:(fst >> self#visit_expr `ImmediateRhsLetBinding)
              (ret :: lbs)
        | Block -> super#visit_expr position e
        | _ -> super#visit_expr `DeepNode e

      method visit_arm' _position arm' =
        (* Guards cannot have side effects *)
        Option.iter ~f:(self#visit_expr `DeepNode) arm'.guard;
        self#visit_expr `CfNode arm'.body
    end
end

Then, on the side effect hoist phase, we would have:

module SideEffectHoist ... = struct
  ...

  let invariants = {
    requires = [...];
    ensures = [...; (module SideEffectOnlyOnCfNode); ...];
    breaks = [...];
  };
end

Doing this for every informal invariant will allow the engine to test those invariants at runtime between each phase, accumulating invariants.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[karthikbhargavan]

@W95Psp see what is needed here for new engine.

[W95Psp]

This will be very similar for the Rust engine

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.