Thoughts on invariant reasoning

[jadephilipoom]

Just a few quick notes about how the Invariant.v infrastructure is set up and the way I think it can scale.

An important principle: if circuit X changes its implementation but not its behavior, then that shouldn't break proofs for circuits that use circuit X.

That's accomplished by a separation of the "invariant" and the "specification". The invariant relates the circuit's actual state to some higher-level Gallina representation, and circuits should be able to reason about their subcircuits using the higher-level representation alone.

With this setup, a change to the implementation of a circuit might require changes to the circuit's invariant, but should never require changes to its specification unless the actual behavior has changed. Higher-level circuits should never unfold its subcircuits' invariants; that would expose the real state of the subcircuits and mean that changes to the subcircuit invariant will break the higher-level proofs.