Lean spec of ccfraft and trace validation

[cjen1-msft]

This is a port of ccfraft.tla over to lean.
I've tried to keep the structure similar to the DR work, and am very willing to align this further, and also change up the model substantially if required. (proof work will need to be repaired unfortunately)

This has

• Protocol/Model.lean
• Protocol/Safety.lean - the safety properties on the model
• Proof/Invaraint.lean - the inductive invariant

Reduction

There is some additional work here that was unnecessary on the other purpose-built protocols.
I tried to align this model with ccfraft.tla (possibly unnecessarily), which means that we have have to deal with non-determinism in the mapping between the model and the code.

For this I'm proposing that we extend the python side to have what I'm calling a reduction step.
As we control both the code and the model, we can use this to deterministically align the 'grains of atomicity' between the two.

This is what that looks like, we have rules in python which reduce a matching set of instructions to a set of actions.

[recv_append_entries, become_follower, send_append_entries_response]
  => [updateTerm, receive]

e.g. reduction.py sees node 1 (stale candidate, term 2) get an AppendEntries at term 4. Because the paired become_follower shows a strictly higher term, it splits the one C++ callback chain into two deterministic canonical actions plus observations:

[
	{"observation": "state", "node": "1",
	 "fields": {"role": "candidate", "currentTerm": 1}},

	{"observation": "message", "source": "0", "destination": "1",
	 "packet": {"msg": "raft_append_entries", "term": 3}},

	{"action": "updateTerm", "source": "0", "destination": "1"},

	{"observation": "state", "node": "1",
	 "fields": {"role": "follower", "currentTerm": 3}},

	{"action": "receive", "source": "0", "destination": "1"},

	{"observation": "state", "node": "1",
	 "fields": {"role": "follower", "currentTerm": 3}},

	{"observation": "message", "source": "1", "destination": "0",
	 "selection": "last",
	 "packet": {"msg": "raft_append_entries_response", "term": 3}}
]

The pipeline I'm proposing for this is:

raft trace -(reduction)-> actions and observations list -(trace validator)-> valid or the failing trace step

The property we get out of trace validation is the alignment between the code and the model.
This alignment is dependent on how well we constrain the model to match the code.
This approach I think should allow us to maximise that alignment and make each step separately auditable.

Comments

SMT trace validation

This trace validation relies on a concrete initial state that we then trace from.
This is not an option for production, as we need to be able to create an initial state from the remote.

We can hack around this by trying to infer what that initial state should be, or producing something 'good-enough', but we will be stuck with a violation trying to work out whether the initial inference was broken or the actual implementation.

Fundamentally what we get from a trace is a set of constraints in the form of observations about each state, and the actions that each node should have taken.
This constitutes a formula that we can then 'just check', and for small traces this works.

The problem is the representation of the trace.
For example supposing that your ledger representation became: fn candidate : predicate(c)
Then to simply evaluate the final state of the trace you have to go via 50-500 of those lambdas.
And tbh SMT trace validation seems to be a mine-field of exactly these kind of issues.

So for example:

• You observe quadratic scaling in your trace length to checking time.
• You microbenchmark the current ledger representation, and conclude that it has quadratic scaling.
• You microbenchmark alternative representations and find one which has linear scaling
• You update the trace validator
• You still have quadratic scaling from another component.

Additionally as soon as you do this, your trace validator has drifted from your original model.
In theory, and in practise, you can then prove that the trace validator representation preserves the original properties, and largely this is a mechanical proof, but data-dependent paths in the model make this proof very expensive/difficult.

All of this is to say that this approach works, and can be made to work, but the cost is very high, and this might be a punt for the next generation of models, or improvements in the integration with SMT solvers.
Additionally small prototypes can scale absolutely fine, and then the full thing breaks horribly.

tl;dr

SMT solvers are likely the right approach for this, and the UX works for it. But getting it to scale as it should be possible (this is deterministic, and just filling in details) there are too many hard edges to go down this route yet.

Merging this PR

I'll also split this up further in the future to get it merged. This draft PR is mainly for discussion.

[Heidi Howard (heidihoward)]

A few initial thoughts:

• Is this reduction step needed? Can't we just change the model to align with the implementation. For instance, I see that the updateTerm action still exists. I claim we don't need a separate updateTerm action now that we have the flexibility of Lean over TLA+.
• Can we migrate DR to ExecutableTransitionSystem and make this shared code? anything else we can make shared? some of the trace validation code?
• Whilst I'm very keen on production tracing, that's out of scope for this PR. We are only aiming to trace validate the same traces as the TLA+
• Rename spec to consensus, don't call it raft as the protocol long since drifted from raft
• Move protocol/safety.lean into properties. The properties.lean file should include enough detail on the properties proven that the reader can get a high level understanding of what's been proven
• I think we should minimize the trace manipulation in python, traces should go (as directly as possible) into Lean. This was needed with TLA+ but should be easier in Lean

[cjen1-msft]

Heidi Howard (@heidihoward) sorry for the essay...

Can we migrate DR to ExecutableTransitionSystem

Definitely, lots can be shared.

production tracing, that's out of scope for this PR.

Yep thats agreed. I was looking into it as I expect we will not want to drastically change the model after we hit merge. And ensuring we are not wholly locked out of production tracing was important to work out.

minimize the trace manipulation in python

Is this reduction step needed? Can't we just change the model to align with the implementation.

You are correct, we can just align the model with the implementation, I was aiming for something comparable with ccfraft.tla for this model but a more aligned one is also possible.

I'm not sure this is exactly what we want to do as proof repair becomes an expensive concern, say if we add another trace event to raft.h or reorder when things get sent.
Most of the time that should be trivial to repair the proof, but its not going to be a human doing that repair.
But anytime an agent needs to read the entirety of a 50k line proof that is going to cost a reasonable amount.
(Currently its about 5 USD every time Astra reads the proof, with Sol at around 2 USD)

We have two somewhat orthogonal aims here

• Extracting model constraints from the trace which needs to be audited no matter what
• Discovering an example of model steps which matches the constraints, or proving that none could.

The discovery requires that we either use some search function to discover this, which becomes intractable quickly (infinite models etc), or SMT scaling problems.
Or we have a mapping from trace actions to model steps, with full alignment being a limiting case of this, and we audit this / AI repair this.

The reduction approach is just a way to represent that mapping.

I don't fully see the tradeoff between python and lean as the host for the mapping.
One possible benefit would be if we could have a meta-properties over the mapping like 'The committed ledger prefixes map in this way and this is ensured over all mappings' which could allow you to better align the safety properties with the implementation.

[cjen1-msft]

Also to capture a thought.
We currently have multiple trace events which map to one big atomic event.

This can be modelled either as N -> 1 reduction.
Or it can be modelled as 1->1.

The issue is that the 1->1 model must reconstruct the serial execution of the raft.h, via sequencing or phases.