Midgard Unordered List Properties.

In this module, we list properties related to Midgard Lists. Properties here are mostly instrumental to prove other Midgard Modules.

Step - Actions Properties

Prepend

theorem MUList.Properties.EnabledPrepend {α : Type} {s : State.ListST α} {root_id : Tokens.Elem.TId} (HRoot : State.ListST.is_root_node root_id s = true) {key : State.Key} {data : α} : ∃ (s' : State.ListST α), Computation.next (State.Actions.UnsafePrepend key data root_id) s = ComputationResult.Success s'

Prepending elements to lists is always enabled if we give the root node.

theorem MUList.Properties.Prepend_Props {α : Type} {s : State.ListST α} {root_id : Tokens.Elem.TId} (HRoot : State.ListST.is_root_node root_id s = true) {key : State.Key} {data : α} : ∃ (s' : State.ListST α), Computation.next (State.Actions.UnsafePrepend key data root_id) s = ComputationResult.Success s' ∧ State.ListST.get_link root_id s' = some key ∧ ∃ (a : Tokens.Elem.TokenD (State.Elemt State.Key α)), Tokens.State.Tokens.get (Tokens.State.Tokens.last_id s') s' = some a ∧ a.data.key = some key ∧ a.data.data = data ∧ a.data.link = State.ListST.get_link root_id s

Properties after prepending a node to the list.

theorem MUList.Properties.Prepend_prepends' {α : Type} {s s' : State.ListST α} {root_id : Tokens.Elem.TId} {key : State.Key} {data : α} (step : Computation.next (State.Actions.UnsafePrepend key data root_id) s = ComputationResult.Success s') : State.ListST.is_member key (Tokens.State.Tokens.last_id s') s' = true ∧ State.ListST.is_anchor key root_id s' = true ∧ State.ListST.is_root_node root_id s = true ∧ State.ListST.is_root_node root_id s' = true

theorem MUList.Properties.Prepend_prepends {α : Type} {s s' : State.ListST α} {root_id : Tokens.Elem.TId} {key : State.Key} {data : α} (step : Relation.Rel s (State.Actions.UnsafePrepend key data root_id) s') : State.ListST.is_member key (Tokens.State.Tokens.last_id s') s' = true ∧ State.ListST.is_anchor key root_id s' = true ∧ State.ListST.is_root_node root_id s = true ∧ State.ListST.is_root_node root_id s' = true

theorem MUList.Properties.Prepend_prepends_new {α : Type} {s s' : State.ListST α} {root_id : Tokens.Elem.TId} {key : State.Key} {data : α} (step : Relation.Rel s (State.Actions.UnsafePrepend key data root_id) s') : ¬Tokens.State.Tokens.last_id s' ∈ s

Prepending adds a new element to the list, generates an element that was not in the list before.

theorem MUList.Properties.Prepend_others_same {α : Type} {s s' : State.ListST α} {root_id : Tokens.Elem.TId} {key : State.Key} {data : α} (step : Relation.Rel s (State.Actions.UnsafePrepend key data root_id) s') (t : Tokens.Elem.TId) (Hr : ¬t = root_id) (Hl : ¬t = Tokens.State.Tokens.last_id s') : Tokens.State.Tokens.get t s = Tokens.State.Tokens.get t s'

After prepends all other elements, neither the root nor the just added, remain the same.

Append Properties

theorem MUList.Properties.Append_Props {α : Type} (s : State.ListST α) (last : Tokens.Elem.TId) (HLast : State.ListST.is_last_node last s = true) (key : State.Key) (data : α) : ∃ (s' : State.ListST α), Computation.next (State.Actions.UnsafeAppend key data last) s = ComputationResult.Success s' ∧ State.ListST.get_link last s' = some key ∧ ∃ (tkn : Tokens.Elem.TokenD (State.Elemt State.Key α)), Tokens.State.Tokens.get (Tokens.State.Tokens.last_id s') s' = some tkn ∧ tkn.data.key = some key ∧ tkn.data.data = data ∧ tkn.data.link = none

Properties after applying append.

theorem MUList.Properties.EnabledAppend {α : Type} (s : State.ListST α) (last : Tokens.Elem.TId) (HLast : State.ListST.is_last_node last s = true) (key : State.Key) (data : α) : ∃ (s' : State.ListST α), Computation.next (State.Actions.UnsafeAppend key data last) s = ComputationResult.Success s'

theorem MUList.Properties.Append_appends {α : Type} {s s' : State.ListST α} {last : Tokens.Elem.TId} {key : State.Key} {data : α} (HStep : Relation.Rel s (State.Actions.UnsafeAppend key data last) s') : State.ListST.is_member key (Tokens.State.Tokens.last_id s') s' = true ∧ State.ListST.is_anchor key last s' = true ∧ State.ListST.is_last_node (Tokens.State.Tokens.last_id s') s' = true ∧ State.ListST.get_data (Tokens.State.Tokens.last_id s') id s' = some data ∧ (∀ (tid : Tokens.Elem.TId), ¬tid = Tokens.State.Tokens.last_id s' ∧ ¬tid = last → Tokens.State.Tokens.get tid s' = Tokens.State.Tokens.get tid s) ∧ ∃ (tkn : Tokens.Elem.TokenD (State.Elemt State.Key α)), Tokens.State.Tokens.get last s = some tkn ∧ Tokens.State.Tokens.get last s' = some { name := tkn.name, data := have __src := tkn.data; { key := __src.key, link := some key, data := __src.data }, id := tkn.id }

Removes Props

theorem MUList.Properties.EnabledRemove {α : Type} {s : State.ListST α} {k : State.Key} {rem anch : Tokens.Elem.TId} (neq : ¬rem = anch) (RemK : State.ListST.is_member k rem s = true) (Anch : State.ListST.is_anchor k anch s = true) : ∃ (s' : State.ListST α), Computation.next (State.Actions.Remove rem anch) s = ComputationResult.Success s'

theorem MUList.Properties.EnabledRemove' {α : Type} {s : State.ListST α} {k : State.Key} {rem anch : Tokens.Elem.TId} (neq : ¬rem = anch) (RemK : State.ListST.is_member k rem s = true) (Anch : State.ListST.is_anchor k anch s = true) : ∃ (s' : State.ListST α), Relation.Rel s (State.Actions.Remove rem anch) s'

theorem MUList.Properties.Removes_members {α : Type} {s s' : State.ListST α} {rem anch : Tokens.Elem.TId} (HStep : Relation.Rel s (State.Actions.Remove rem anch) s') : rem ∈ s

theorem MUList.Properties.Removes_anch {α : Type} {s s' : State.ListST α} {rem anch : Tokens.Elem.TId} (HStep : Relation.Rel s (State.Actions.Remove rem anch) s') : State.ListST.is_anchor_tokens rem anch s = true

theorem MUList.Properties.NotRemoveself' {α : Type} {s : State.ListST α} {rem : Tokens.Elem.TId} {node : Tokens.Elem.TokenD (State.Elemt State.Key α)} (Hmem : Tokens.State.Tokens.get rem s = some node) : ∃ (err : Computation.Err), Computation.next (State.Actions.Remove rem rem) s = ComputationResult.Failure err

theorem MUList.Properties.NotRemoveSelf {α : Type} {s s' : State.ListST α} {rem anch : Tokens.Elem.TId} (HStep : Relation.Rel s (State.Actions.Remove rem anch) s') : ¬rem = anch

theorem MUList.Properties.Removes_finds_none {α : Type} {s s' : State.ListST α} {rem anch : Tokens.Elem.TId} (HStep : Relation.Rel s (State.Actions.Remove rem anch) s') : Tokens.State.Tokens.get rem s' = none

theorem MUList.Properties.Removes_others {α : Type} {s s' : State.ListST α} {rem anch : Tokens.Elem.TId} (HStep : Relation.Rel s (State.Actions.Remove rem anch) s') (t : Tokens.Elem.TId) : ¬t = rem ∧ ¬t = anch → Tokens.State.Tokens.get t s' = Tokens.State.Tokens.get t s

theorem MUList.Properties.Removes_update_anch_mem_and_key {α : Type} {s s' : State.ListST α} {rem anch : Tokens.Elem.TId} (HStep : Relation.Rel s (State.Actions.Remove rem anch) s') : (∀ (t : State.Key), State.ListST.is_member t anch s' = State.ListST.is_member t anch s) ∧ State.ListST.get_key anch s' = State.ListST.get_key anch s ∧ State.ListST.get_link anch s' = State.ListST.get_link rem s ∧ State.ListST.get_data anch id s' = State.ListST.get_data anch id s ∧ Tokens.State.Tokens.get_name anch s' = Tokens.State.Tokens.get_name anch s ∧ (fun (x : Tokens.Elem.TokenD (State.Elemt State.Key α)) => x.id) <$> Tokens.State.Tokens.get anch s' = (fun (x : Tokens.Elem.TokenD (State.Elemt State.Key α)) => x.id) <$> Tokens.State.Tokens.get anch s

theorem MUList.Properties.Removes_update_anch_mem_and_key' {α : Type} {s s' : State.ListST α} {rem anch : Tokens.Elem.TId} (HStep : Relation.Rel s (State.Actions.Remove rem anch) s') : Tokens.State.Tokens.get anch s' = (fun (x : Tokens.Elem.TokenD (State.Elemt State.Key α)) => { name := x.name, data := have __src := x.data; { key := __src.key, link := State.ListST.get_link rem s, data := __src.data }, id := x.id }) <$> Tokens.State.Tokens.get anch s

theorem MUList.Properties.Removes_update_anch_mem {α : Type} {s s' : State.ListST α} {rem anch : Tokens.Elem.TId} (HStep : Relation.Rel s (State.Actions.Remove rem anch) s') (t : Tokens.Elem.TId) : State.ListST.is_member t anch s' = State.ListST.is_member t anch s

theorem MUList.Properties.Removes_same_anch_key {α : Type} {s s' : State.ListST α} {rem anch : Tokens.Elem.TId} (HStep : Relation.Rel s (State.Actions.Remove rem anch) s') : State.ListST.get_key anch s' = State.ListST.get_key anch s

theorem MUList.Properties.Removes_others_keys {α : Type} {s s' : State.ListST α} {rem anch : Tokens.Elem.TId} (step : Relation.Rel s (State.Actions.Remove rem anch) s') (t : Tokens.Elem.TId) : ¬t = rem → State.ListST.get_key t s' = State.ListST.get_key t s

theorem MUList.Properties.Removes_others_mem {α : Type} {s s' : State.ListST α} {rem anch : Tokens.Elem.TId} (HStep : Relation.Rel s (State.Actions.Remove rem anch) s') (t : Tokens.Elem.TId) : ¬t = rem → ∀ (k : State.Key), State.ListST.is_member k t s' = State.ListST.is_member k t s

theorem MUList.Properties.Removes_members_is_mem {α : Type} {s s' : State.ListST α} {rem anch : Tokens.Elem.TId} (HStep : Relation.Rel s (State.Actions.Remove rem anch) s') {key : State.Key} {t : Tokens.Elem.TId} (is_m : State.ListST.is_member key t s' = true) : State.ListST.is_member key t s = true

theorem MUList.Properties.Removes_members_anch {α : Type} {s s' : State.ListST α} {rem anch : Tokens.Elem.TId} (Step : Relation.Rel s (State.Actions.Remove rem anch) s') : ∃ (a : Tokens.Elem.TokenD (State.Elemt State.Key α)), Tokens.State.Tokens.get anch s' = some a ∧ ∀ (rem_nd : Tokens.Elem.TokenD (State.Elemt State.Key α)), Tokens.State.Tokens.get rem s = some rem_nd → a.data.link = rem_nd.data.link

theorem MUList.Properties.Remove_removes {α : Type} {s s' : State.ListST α} {rem anch : Tokens.Elem.TId} (step : Relation.Rel s (State.Actions.Remove rem anch) s') : ¬rem ∈ s' ∧ State.ListST.get_link anch s' = State.ListST.get_link rem s ∧ State.ListST.get_data anch id s' = State.ListST.get_data anch id s ∧ State.ListST.get_key anch s' = State.ListST.get_key anch s ∧ Tokens.State.Tokens.get_name anch s' = Tokens.State.Tokens.get_name anch s

theorem MUList.Properties.Removes_get_not_removed {α : Type} {s s' : State.ListST α} {rem anch oth : Tokens.Elem.TId} (step : Relation.Rel s (State.Actions.Remove rem anch) s') (H : (Tokens.State.Tokens.get oth s').isSome = true) : ¬oth = rem

ModifyData

theorem MUList.Properties.ModifyData_same_others {α : Type} {s s' : State.ListST α} {tid : Tokens.Elem.TId} {data : α} (step : Relation.Rel s (State.Actions.ModifyData tid data) s') (t : Tokens.Elem.TId) : ¬t = tid → Tokens.State.Tokens.get t s = Tokens.State.Tokens.get t s'

theorem MUList.Properties.ModifyData_find_token {α : Type} {s s' : State.ListST α} {tid : Tokens.Elem.TId} {data : α} (step : Relation.Rel s (State.Actions.ModifyData tid data) s') : (Tokens.State.Tokens.get tid s).isSome = true ∧ (Tokens.State.Tokens.get tid s').isSome = true

theorem MUList.Properties.ModifyData_modified {α : Type} {s s' : State.ListST α} {tid : Tokens.Elem.TId} {data : α} (step : Relation.Rel s (State.Actions.ModifyData tid data) s') : (fun (x : Tokens.Elem.TokenD (State.Elemt State.Key α)) => x.data.data) <$> Tokens.State.Tokens.get tid s' = some data

def MUList.Properties.same_but_data_this {α : Type} (tl tr : State.ListToken α) (data : α) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem MUList.Properties.ModifyData_modified_stronger {α : Type} {s s' : State.ListST α} {tid : Tokens.Elem.TId} {data : α} {tkns tkns' : Tokens.Elem.TokenD (State.Elemt State.Key α)} (step : Relation.Rel s (State.Actions.ModifyData tid data) s') (HS : Tokens.State.Tokens.get tid s = some tkns) (HS' : Tokens.State.Tokens.get tid s' = some tkns') : same_but_data_this tkns tkns' data

theorem MUList.Properties.ModifyData_modified_stronger' {α : Type} {s s' : State.ListST α} {tid : Tokens.Elem.TId} {data : α} {tkns : Tokens.Elem.TokenD (State.Elemt State.Key α)} (step : Relation.Rel s (State.Actions.ModifyData tid data) s') (HS : Tokens.State.Tokens.get tid s = some tkns) : Tokens.State.Tokens.get tid s' = some { name := tkns.name, data := have __src := tkns.data; { key := __src.key, link := __src.link, data := data }, id := tkns.id }

theorem MUList.Properties.ModifyData_same_members {α : Type} {s s' : State.ListST α} {tid : Tokens.Elem.TId} {data : α} (step : Relation.Rel s (State.Actions.ModifyData tid data) s') (k : State.Key) (t : Tokens.Elem.TId) : State.ListST.is_member k t s = State.ListST.is_member k t s'

Well Formed Linked List Properties

def MUList.Properties.NeverEmptyP {α : Type} (s : State.ListST α) : Prop

Correct lists are never empty, root is always alive

Equations

• MUList.Properties.NeverEmptyP s = ((List.any s fun (x : Option (Tokens.Elem.TokenD (MUList.State.Elemt MUList.State.Key α))) => x.isSome) = true)

def MUList.Properties.NeverEmptyB {α : Type} (s : State.ListST α) : Bool

Equations

• MUList.Properties.NeverEmptyB s = List.any s fun (x : Option (Tokens.Elem.TokenD (MUList.State.Elemt MUList.State.Key α))) => x.isSome

theorem MUList.Properties.InitNotEmpty {α : Type} {rinit : α} : NeverEmptyB (State.ListST.init rinit).fst = true

theorem MUList.Properties.InvNotEmpty {α : Type} {s s' : State.ListST α} {a : State.Actions α} (Step : Relation.Rel s a s') : NeverEmptyB s' = true

Not empty invariant.

def MUList.Properties.not_empty_induction {α : Type} {iv : α} : StepMachines.InductionStepMachine () (Computational.StepList iv) fun (x : State.ListST α) => NeverEmptyB x = true

Equations

• ⋯ = ⋯

theorem MUList.Properties.NotEmpty {α : Type} {s : State.ListST α} (reachable : Computational.ReachableUList s) : NeverEmptyB s = true

theorem MUList.Properties.not_remove_root {α : Type} (s s' : State.ListST α) (rem anch : Tokens.Elem.TId) (rem_root : State.ListST.is_root_node rem s = true) : ¬Relation.Rel s (State.Actions.Remove rem anch) s'

We cannot remove root nodes

theorem MUList.Properties.same_root {α : Type} {s s' : State.ListST α} {i : State.Actions α} {root_id : Tokens.Elem.TId} (pre : State.ListST.is_root_node root_id s = true) (step : Relation.Rel s i s') : State.ListST.is_root_node root_id s' = true

Midgard Lists do not change of root nodes.

def MUList.Properties.no_new_root_inv {α : Type} {s s' : State.ListST α} {root_id : Tokens.Elem.TId} {i : State.Actions α} (t_pos_root : State.ListST.is_root_node root_id s' = true) (step : Relation.Rel s i s') : State.ListST.is_root_node root_id s = true

Root remains the same invariant backwards

Equations

• ⋯ = ⋯

def MUList.Properties.only_one_root {α : Type} (s : State.ListST α) : Prop

There is only one root node statmement definition.

Equations

• MUList.Properties.only_one_root s = ∀ (t t_p : Tokens.Elem.TId), MUList.State.ListST.is_root_node t s = true → MUList.State.ListST.is_root_node t_p s = true → t = t_p

theorem MUList.Properties.only_one_root_inv {α : Type} {s s' : State.ListST α} {i : State.Actions α} (pre : only_one_root s) (step : Relation.Rel s i s') : only_one_root s'

Only one root node.

def MUList.Properties.one_root_induction {α : Type} {iv : α} : StepMachines.InductionStepMachine () (Computational.StepList iv) only_one_root

Equations

• ⋯ = ⋯

theorem MUList.Properties.one_root {α : Type} {s : State.ListST α} (reachable : Computational.ReachableUList s) : only_one_root s

def MUList.Properties.OneRootB {α : Type} (s : State.ListST α) : Bool

Equations

• One or more equations did not get rendered due to their size.

def MUList.Properties.OneLastB {α : Type} (s : State.ListST α) : Bool

Equations

• One or more equations did not get rendered due to their size.

def MUList.Properties.all_next_keys_have_token {α : Type} (s : State.ListST α) : Bool

Next keys are alive

Equations

• One or more equations did not get rendered due to their size.

def MUList.Properties.next_key_token {α : Type} (s : State.ListST α) : Prop

Equations

• One or more equations did not get rendered due to their size.

axiom MUList.Properties.all_next_keys_are_alive_inv {α : Type} {s s' : State.ListST α} {i : State.Actions α} (HPre : all_next_keys_have_token s = true) (step : Relation.Rel s i s') : all_next_keys_have_token s' = true

All linked keys are in the list. We test this property using Plausible and Blaster.

def MUList.Properties.IdMatchP {α : Type} (s : State.ListST α) : Prop

Equations

• MUList.Properties.IdMatchP s = ∀ (i : Tokens.Elem.TId) (nd : Tokens.Elem.TokenD (MUList.State.Elemt MUList.State.Key α)), Tokens.State.Tokens.get i s = some nd → nd.id = i

def MUList.Properties.IdMatchFind {α : Type} (s : State.ListST α) : Prop

Equations

• MUList.Properties.IdMatchFind s = ∀ {i : Tokens.Elem.TId} {nd : Tokens.Elem.TokenD (MUList.State.Elemt MUList.State.Key α)}, Tokens.State.Tokens.get i s = some nd → nd.id = i

def MUList.Properties.IdMatchB {α : Type} (s : State.ListST α) : Bool

Equations

• One or more equations did not get rendered due to their size.

theorem MUList.Properties.burn_id_match {α : Type} {s burnt : State.ListST α} {rem : Tokens.Elem.TId} (HB : Tokens.State.Tokens.burn rem s = some burnt) (inv : IdMatchP s) : IdMatchP burnt

def MUList.Properties.proof_id_match {α : Type} (rinit : α) : StepMachines.InductionStepMachine () (Computational.StepList rinit) IdMatchP

Equations

• ⋯ = ⋯

theorem MUList.Properties.find_anchor_correct {α : Type} {s : State.ListST α} {k : State.Key} {tkn : Tokens.Elem.TokenD (State.Elemt State.Key α)} (v : IdMatchP s) (hf : InternalUtils.find_anchor s k = some tkn) : State.ListST.is_anchor k tkn.id s = true

theorem MUList.Properties.find_anchors_correct {α : Type} {s : State.ListST α} {k : State.Key} {anchs : List (Tokens.Elem.TokenD (State.Elemt State.Key α))} (v : IdMatchP s) (hf : InternalUtils.find_anchors s k = anchs) (a : Tokens.Elem.TokenD (State.Elemt State.Key α)) : a ∈ anchs → State.ListST.is_anchor k a.id s = true

theorem MUList.Properties.all_alive_apply_member {α : Type} {s : State.ListST α} {k : State.Key} {t : Tokens.Elem.TId} {p : Tokens.Elem.TokenD (State.Elemt State.Key α) × ℕ → Bool} (hm : State.ListST.is_member k t s = true) (hall : InternalUtils.all_alive_tids s p = true) : ∃ (tkn : Tokens.Elem.TokenD (State.Elemt State.Key α)), Tokens.State.Tokens.get t s = some tkn ∧ p (tkn, t) = true

theorem MUList.Properties.is_member_find_key {α : Type} {s : State.ListST α} {k : State.Key} (hnone : (InternalUtils.find_key s k).isNone = true) (tid : Tokens.Elem.TId) : State.ListST.is_member k tid s = false

theorem MUList.Properties.find_key_none_membership {α : Type} {s : State.ListST α} {k : State.Key} (hnone : (InternalUtils.find_key s k).isNone = true) : ¬k ∈ State.all_keys s

theorem MUList.Properties.all_alive_all_tkn {α : Type} {s : State.ListST α} {f : Tokens.Elem.TokenD (State.Elemt State.Key α) × ℕ → Bool} (v : InternalUtils.all_alive_valid s = true) : InternalUtils.all_alive_tids s f = true ↔ ∀ (t : Tokens.Elem.TId), t ∈ s → ∃ (tkn : Tokens.Elem.TokenD (State.Elemt State.Key α)), Tokens.State.Tokens.get t s = some tkn ∧ f (tkn, tkn.id) = true

def MUList.Properties.IdRef {α : Type} (s : State.ListST α) : Prop

Equations

• MUList.Properties.IdRef s = ∀ (i : Tokens.Elem.TId), i ∈ s → i < List.length s

def MUList.Properties.rememberLastId {α : Type} (s : State.ListST α) (a : State.Actions α) (prev_last : Tokens.Elem.TId) : Tokens.Elem.TId

Equations

• One or more equations did not get rendered due to their size.
• MUList.Properties.rememberLastId s (MUList.State.Actions.UnsafeAppend key data last) prev_last = Tokens.State.Tokens.last_id s
• MUList.Properties.rememberLastId s (MUList.State.Actions.Remove rem anch) prev_last = if MUList.State.ListST.is_last_node rem s = true then anch else prev_last
• MUList.Properties.rememberLastId s a prev_last = prev_last

def MUList.Properties.LastUniqueP {α : Type} (s : State.ListST α) : Prop

Equations

• MUList.Properties.LastUniqueP s = ∀ (i j : Tokens.Elem.TId), MUList.State.ListST.is_last_node i s = true → MUList.State.ListST.is_last_node j s = true → i = j

def MUList.Properties.RemovableTokens {α : Type} {s : State.ListST α} {tid : Tokens.Elem.TId} {k : State.Key} (_hkey : State.ListST.get_key tid s = some k) : Prop

Prop stating that all nodes can be removed. They can be removed if they have an anchor that it is not themselves. They can be anchors of themselves, but they must accept another anchor too. The root node cannot be remove, so what we say is that all nodes with key can be removed.

Equations

• MUList.Properties.RemovableTokens _hkey = ∃ (anchor : Tokens.Elem.TId), ¬tid = anchor ∧ MUList.State.ListST.is_anchor k anchor s = true