schema: 1
drafts:
DLV-0017:
revision: c0923db07e0d33f1a67c9644489c004a68fe242a08e3769bfd8af1c99ea6961b
candidate: |-
requirement retry_dlq_lifecycle {
category: 2a
vocabulary {
state retries_bounded()
}
assume { }
require {
always retries_bounded()
}
}
gate:
status: passed
warnings: []
admission:
state: admitted
review: optional
by: Gordon Greene
at_unix: 1792095672
bindings:
- symbol: retries_bounded
category: model
observable: RetriesBounded
fidelity: definitional
DLV-0018:
revision: 569c6ae841dad1a243e13315836487973521d69ecf0f9472c8b967074eb925c5
candidate: |-
requirement pop_atomicity {
category: 2a
vocabulary {
state at_most_one_holder()
state lock_matches_holder()
}
assume { }
require {
always at_most_one_holder()
always lock_matches_holder()
}
}
gate:
status: passed
warnings: []
admission:
state: admitted
review: optional
by: Gordon Greene
at_unix: 1790734086
bindings:
- symbol: at_most_one_holder
category: model
observable: AtMostOneHolder
fidelity: definitional
- symbol: lock_matches_holder
category: model
observable: LockMatchesHolder
fidelity: definitional
DLV-0019:
revision: 76d1d0b4edc6998b752551637e5d78c2f786d126f39797fcd0615913270a49ca
candidate: |-
requirement ack_nack_ownership {
category: 2a
vocabulary {
state finalized_only_by_owner()
state owner_matches_lock()
}
assume { }
require {
always finalized_only_by_owner()
always owner_matches_lock()
}
}
gate:
status: passed
warnings: []
admission:
state: admitted
review: optional
by: Gordon Greene
at_unix: 1790737259
bindings:
- symbol: finalized_only_by_owner
category: model
observable: FinalizedOnlyByOwner
fidelity: definitional
- symbol: owner_matches_lock
category: model
observable: OwnerMatchesLock
fidelity: definitional
DLV-0020:
revision: b0126728f49a3cb1133408bdb0243a25de7dd19014bad248c435069a6ade83c4
candidate: |-
requirement lock_expiry_recovery {
category: 2a
vocabulary {
state sweep_always_enabled_for_expired()
}
assume { }
require {
always sweep_always_enabled_for_expired()
}
}
gate:
status: passed
warnings: []
admission:
state: admitted
review: optional
by: Gordon Greene
at_unix: 1790798071
bindings:
- symbol: sweep_always_enabled_for_expired
category: model
observable: SweepAlwaysEnabledForExpired
fidelity: definitional
DLV-0021:
revision: b1f8eda1607be42b16d435b9942a69e7fd3952a9a0fb2a26ec6185b9167ed8fa
candidate: |-
requirement expired_lock_recheck {
category: 2a
vocabulary {
state sweep_acts_only_on_expired()
}
assume { }
require {
always sweep_acts_only_on_expired()
}
}
gate:
status: passed
warnings: []
admission:
state: admitted
review: optional
by: Gordon Greene
at_unix: 1790802006
bindings:
- symbol: sweep_acts_only_on_expired
category: model
observable: SweepActsOnlyOnExpired
fidelity: definitional
DLV-0022:
revision: 6769a2b94120f5120c09ece21b63612acab6f718dd91eb9a04cdbdfd16b50416
candidate: |-
requirement no_duplicate_payload {
category: 2a
vocabulary {
state at_most_one_per_payload()
}
assume { }
require {
always at_most_one_per_payload()
}
}
gate:
status: passed
warnings: []
admission:
state: admitted
review: optional
by: Gordon Greene
at_unix: 1790804323
bindings:
- symbol: at_most_one_per_payload
category: model
observable: AtMostOnePerPayload
fidelity: definitional
DLV-0023:
revision: c534ed9d43cd492be06f5945076e1599014da80ce3b5c186a67d419edbcf573c
candidate: |-
requirement lock_ordering_deadlock_free {
category: 2a
vocabulary {
state deadlock_free()
}
assume { }
require {
always deadlock_free()
}
}
gate:
status: passed
warnings: []
admission:
state: admitted
review: optional
by: Gordon Greene
at_unix: 1790805695
bindings:
- symbol: deadlock_free
category: model
observable: DeadlockFree
fidelity: definitional
PER-0002:
revision: 256d8c1ff0920a8b08d2f9c64dfdf1552d2340b031d228b223f59960032bc707
candidate: |-
requirement queue_isolation {
category: 1
vocabulary {
state storage_key_is_queue_prefixed(k: StorageKey)
state storage_key_in_queue_scan_range(k: StorageKey)
}
assume { }
require {
each k: StorageKey . always storage_key_is_queue_prefixed(k)
each k: StorageKey . always storage_key_in_queue_scan_range(k)
}
}
gate:
status: passed
warnings: []
admission:
state: admitted
review: optional
by: Gordon Greene
at_unix: 1790564683
bindings:
- symbol: StorageKey
category: code
observable: StorageKey
fidelity: definitional
- symbol: storage_key_is_queue_prefixed
category: code
observable: storage_key_is_queue_prefixed
fidelity: definitional
- symbol: storage_key_in_queue_scan_range
category: code
observable: storage_key_in_queue_scan_range
fidelity: definitional
PER-0022:
revision: b511f240946732aaee149dbc82979e82f1da45d839e144389bca165b358c4716
candidate: |-
requirement queue_scan_isolation {
category: 2a
vocabulary {
state scan_yields_only_in_range()
}
assume { }
require {
always scan_yields_only_in_range()
}
}
gate:
status: passed
warnings: []
admission:
state: admitted
review: optional
by: Gordon Greene
at_unix: 1792095636
bindings:
- symbol: scan_yields_only_in_range
category: model
observable: ScanYieldsOnlyInRange
fidelity: definitional
PER-0023:
revision: d8784ffe5df0c377e5cc232b5353ff3019458e17dec6f1deac0cad96d2f864e1
candidate: |-
requirement compaction_never_serves_stale {
category: 2a
vocabulary {
state never_serves_stale()
}
assume { }
require {
always never_serves_stale()
}
}
gate:
status: passed
warnings: []
admission:
state: admitted
review: optional
by: Gordon Greene
at_unix: 1790814986
bindings:
- symbol: never_serves_stale
category: model
observable: NeverServesStale
fidelity: definitional
SYS-0028:
revision: 2277cb2e6c99b15342bab933c2979e7db88a81d80420a52c48a928edabb5781c
candidate: |-
requirement counter_cache_consistency {
category: 2a
vocabulary {
state counters_match_population()
state counters_non_negative()
}
assume { }
require {
always counters_match_population()
always counters_non_negative()
}
}
gate:
status: passed
warnings: []
admission:
state: admitted
review: optional
by: Gordon Greene
at_unix: 1790704895
bindings:
- symbol: counters_match_population
category: model
observable: CountersMatchPopulation
fidelity: definitional
- symbol: counters_non_negative
category: model
observable: CountersNonNegative
fidelity: definitional
SYS-0029:
revision: 0d5bdca10bd90f7fd25c94ae1daa30bcef37e9900e8447074a9d4318dc71909d
candidate: |-
requirement hot_tier_coherent {
category: 2a
vocabulary {
state hot_tier_coherent()
}
assume { }
require {
always hot_tier_coherent()
}
}
gate:
status: passed
warnings: []
admission:
state: admitted
review: optional
by: Gordon Greene
at_unix: 1790809217
bindings:
- symbol: hot_tier_coherent
category: model
observable: HotTierCoherent
fidelity: definitional
SYS-0030:
revision: c12b68a2fc91d367049426ebab1f85c6e6ef1dd8a6c87f1d81872b7f72d5e142
candidate: |-
requirement startup_init_gating {
category: 2a
vocabulary {
state mutations_gated_by_init()
}
assume { }
require {
always mutations_gated_by_init()
}
}
gate:
status: passed
warnings: []
admission:
state: admitted
review: optional
by: Gordon Greene
at_unix: 1790813573
bindings:
- symbol: mutations_gated_by_init
category: model
observable: MutationsGatedByInit
fidelity: definitional
SYS-0031:
revision: f31dc4418c780c1b396962b7e83ebca17200ad62fa279a0a6bb17be76ee1f2a0
candidate: |-
requirement counter_reconcile_convergence {
category: 2a
vocabulary {
state drifted()
state consistent()
}
assume { }
require {
drifted() leads_to consistent()
}
}
gate:
status: passed
warnings: []
admission:
state: admitted
review: optional
by: Gordon Greene
at_unix: 1792000726
bindings:
- symbol: drifted
category: model
observable: Drifted
fidelity: definitional
- symbol: consistent
category: model
observable: Consistent
fidelity: definitional