I find portions of he Key Consistency docs a little bit confusing.
Why do we need an unknown key state?
"key state"s are defined to be one of three:
assigned to the latest Create | non-consuming Exercise | Fetch action of a contract on said key.
free if the latest action is consuming Exercise | NoSuchKey assertion
unknown.
If there is not last action, why not consider the state as free ?
Consistency Q1
“If act is a Create action or NoSuchKey assertion, then s is free or unknown .”
… again why not just be free? We’re going to great lengths to be precise about things here and that “or” seems odd.
Consistency Q2
" If act is an Exercise or Fetch action on some contract c, then s is assigned to c or unknown ."
This time why would it be unknown? If we’ve just performed either of those two transactions, shouldn’t the state be assigned ?
When reading this portion of the documentation, I feel like I’m lacking some assumed piece of background knowledge that I should have already understood. Please let me know if there’s something that would be helpful.
The current formulation serves to then be able to define internal consistency as follows:
A transaction is internally consistent if it is internally consistent for all contracts and consistent for all keys.
But your point is valid. Consistency is defined before internal consistency, so I see how it reads like an unnecessary complication at the point of definition. I’ve added this as a todo item in an upcoming change to the keys part of the ledger model write-up: