Questions about Key State and Consistency

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.

2 Likes

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:

Poking this question. I just read the definition of key consistency, and I also tried to figure out Q2 without luck. Any progress on that?

1 Like