Project a revocation mirror
As a mirror contributor, I want to open a registry or record a published revocation from its supplied issuer seal.
These executable statement-model calls preserve the source boundary. Lifecycle synchronization actions do not bypass Checkpoint funding or evidence guards. The theorem statements remain unproved.
Examples below are model fixtures. Their oracle fields describe synthetic verification outcomes; they are not evidence accepted from production callers. The input shown includes common fixture context as well as the call.
flowchart LR
Caller[Caller] -->|Supplied published evidence| Assessment[Evidence assessment]
Assessment -->|Missing required evidence| Unknown[unknown]
Assessment -->|Complete model inputs| Model[Model operation]
Model -->|Predicate fails| Refused[Named refusal]
Model -->|Predicate holds| Result[State, flow or verdict]History
As a caller, I want to update an issuer history in the mirror model.
Operation: mirror.history. The corpus contains 2 observations.
Named refusals:
mirror.history-refused: The named executable source operation returns none.
Accepted example
Caller supplies this model fixture:
{
"params": {
"toadFloor": 2
},
"action": {
"action": "mirror.history",
"aid": 1,
"historyAction": {
"action": "history.advance",
"sn": 30,
"toad": 2
}
},
"state": {
"ckpt": [
{
"aid": 1,
"checkpoint": {
"aid": 1,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
},
{
"aid": 2,
"checkpoint": {
"aid": 2,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
}
],
"reg": [
{
"registry": {
"issuer": 1,
"revoked": [],
"rid": 10
},
"rid": 10
},
{
"registry": {
"issuer": 2,
"revoked": [],
"rid": 20
},
"rid": 20
}
]
},
"oracle": {
"receipted": true,
"signatureEpoch": null,
"signed": true
}
}
Caller obtains:
{
"status": "accepted",
"value": {
"ckpt": [
{
"aid": 1,
"checkpoint": {
"aid": 1,
"cur": 3,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
},
{
"leaf": {
"epoch": 3,
"prev": 20,
"toad": 2
},
"sn": 30
}
],
"latest": 30,
"parent": null
}
},
{
"aid": 2,
"checkpoint": {
"aid": 2,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
}
],
"reg": [
{
"registry": {
"issuer": 1,
"revoked": [],
"rid": 10
},
"rid": 10
},
{
"registry": {
"issuer": 2,
"revoked": [],
"rid": 20
},
"rid": 20
}
]
}
}
Refused example
Caller supplies this model fixture:
{
"params": {
"toadFloor": 2
},
"action": {
"action": "mirror.history",
"aid": 9,
"historyAction": {
"action": "history.advance",
"sn": 30,
"toad": 2
}
},
"state": {
"ckpt": [
{
"aid": 1,
"checkpoint": {
"aid": 1,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
},
{
"aid": 2,
"checkpoint": {
"aid": 2,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
}
],
"reg": [
{
"registry": {
"issuer": 1,
"revoked": [],
"rid": 10
},
"rid": 10
},
{
"registry": {
"issuer": 2,
"revoked": [],
"rid": 20
},
"rid": 20
}
]
},
"oracle": {
"receipted": true,
"signatureEpoch": null,
"signed": true
}
}
Caller obtains:
{
"status": "refused",
"refusal": "mirror.history-refused"
}
Miss
As a caller, I want to check absence from a supplied revocation mirror.
Operation: mirror.miss. The corpus contains 2 observations.
This query returns a Boolean. False is an evaluated result, not a refusal.
Evaluated true example
Caller supplies this model fixture:
{
"params": {
"toadFloor": 2
},
"action": {
"action": "mirror.miss",
"rid": 10,
"said": 1010
},
"state": {
"ckpt": [
{
"aid": 1,
"checkpoint": {
"aid": 1,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
},
{
"aid": 2,
"checkpoint": {
"aid": 2,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
}
],
"reg": [
{
"registry": {
"issuer": 1,
"revoked": [],
"rid": 10
},
"rid": 10
},
{
"registry": {
"issuer": 2,
"revoked": [],
"rid": 20
},
"rid": 20
}
]
},
"oracle": {
"receipted": true,
"signatureEpoch": null,
"signed": true
}
}
Caller obtains:
{
"status": "accepted",
"value": true
}
Evaluated false example
Caller supplies this model fixture:
{
"params": {
"toadFloor": 2
},
"action": {
"action": "mirror.miss",
"rid": 10,
"said": 1010
},
"state": {
"ckpt": [
{
"aid": 1,
"checkpoint": {
"aid": 1,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
},
{
"aid": 2,
"checkpoint": {
"aid": 2,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
}
],
"reg": []
},
"oracle": {
"receipted": true,
"signatureEpoch": null,
"signed": true
}
}
Caller obtains:
{
"status": "accepted",
"value": false
}
Open
As a caller, I want to open an issuer-bound mirror from a sealed registry inception.
Operation: mirror.open. The corpus contains 3 observations.
Named refusals:
mirror.open-refused: The named executable source operation returns none.
Accepted example
Caller supplies this model fixture:
{
"params": {
"toadFloor": 2
},
"action": {
"action": "mirror.open",
"issuer": 1,
"w": {
"core": {
"e": 10,
"idx": 1,
"kel": {
"establishment": false,
"seals": [
{
"d": 0,
"i": 99,
"s": 0
},
{
"d": 10010,
"i": 10,
"s": 0
}
],
"sn": 15
},
"succ": 20
},
"tel": {
"i": 10,
"kind": "vcp",
"ri": 10,
"s": 0
}
}
},
"state": {
"ckpt": [
{
"aid": 1,
"checkpoint": {
"aid": 1,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
},
{
"aid": 2,
"checkpoint": {
"aid": 2,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
}
],
"reg": []
},
"oracle": {
"receipted": true,
"signatureEpoch": null,
"signed": true
}
}
Caller obtains:
{
"status": "accepted",
"value": {
"ckpt": [
{
"aid": 1,
"checkpoint": {
"aid": 1,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
},
{
"aid": 2,
"checkpoint": {
"aid": 2,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
}
],
"reg": [
{
"registry": {
"issuer": 1,
"revoked": [],
"rid": 10
},
"rid": 10
}
]
}
}
Refused example
Caller supplies this model fixture:
{
"params": {
"toadFloor": 2
},
"action": {
"action": "mirror.open",
"issuer": 1,
"w": {
"core": {
"e": 10,
"idx": 1,
"kel": {
"establishment": false,
"seals": [
{
"d": 0,
"i": 99,
"s": 0
},
{
"d": 10010,
"i": 10,
"s": 0
}
],
"sn": 15
},
"succ": 20
},
"tel": {
"i": 10,
"kind": "vcp",
"ri": 10,
"s": 0
}
}
},
"state": {
"ckpt": [
{
"aid": 1,
"checkpoint": {
"aid": 1,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
},
{
"aid": 2,
"checkpoint": {
"aid": 2,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
}
],
"reg": [
{
"registry": {
"issuer": 1,
"revoked": [],
"rid": 10
},
"rid": 10
},
{
"registry": {
"issuer": 2,
"revoked": [],
"rid": 20
},
"rid": 20
}
]
},
"oracle": {
"receipted": true,
"signatureEpoch": null,
"signed": true
}
}
Caller obtains:
{
"status": "refused",
"refusal": "mirror.open-refused"
}
Push
As a caller, I want to record a published revocation in its mirror.
Operation: mirror.push. The corpus contains 3 observations.
Named refusals:
mirror.push-refused: The named executable source operation returns none.
Accepted example
Caller supplies this model fixture:
{
"params": {
"toadFloor": 2
},
"action": {
"action": "mirror.push",
"w": {
"core": {
"e": 10,
"idx": 1,
"kel": {
"establishment": false,
"seals": [
{
"d": 0,
"i": 99,
"s": 0
},
{
"d": 11020,
"i": 1020,
"s": 1
}
],
"sn": 15
},
"succ": 20
},
"tel": {
"i": 1020,
"kind": "rev",
"ri": 20,
"s": 1
}
}
},
"state": {
"ckpt": [
{
"aid": 1,
"checkpoint": {
"aid": 1,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
},
{
"aid": 2,
"checkpoint": {
"aid": 2,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
}
],
"reg": [
{
"registry": {
"issuer": 1,
"revoked": [],
"rid": 10
},
"rid": 10
},
{
"registry": {
"issuer": 2,
"revoked": [],
"rid": 20
},
"rid": 20
}
]
},
"oracle": {
"receipted": true,
"signatureEpoch": null,
"signed": true
}
}
Caller obtains:
{
"status": "accepted",
"value": {
"ckpt": [
{
"aid": 1,
"checkpoint": {
"aid": 1,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
},
{
"aid": 2,
"checkpoint": {
"aid": 2,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
}
],
"reg": [
{
"registry": {
"issuer": 1,
"revoked": [],
"rid": 10
},
"rid": 10
},
{
"registry": {
"issuer": 2,
"revoked": [
1020
],
"rid": 20
},
"rid": 20
}
]
}
}
Refused example
Caller supplies this model fixture:
{
"params": {
"toadFloor": 2
},
"action": {
"action": "mirror.push",
"w": {
"core": {
"e": 10,
"idx": 1,
"kel": {
"establishment": false,
"seals": [
{
"d": 0,
"i": 99,
"s": 0
},
{
"d": 11020,
"i": 1020,
"s": 1
}
],
"sn": 15
},
"succ": 20
},
"tel": {
"i": 1020,
"kind": "rev",
"ri": 20,
"s": 1
}
}
},
"state": {
"ckpt": [
{
"aid": 1,
"checkpoint": {
"aid": 1,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
},
{
"aid": 2,
"checkpoint": {
"aid": 2,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
}
],
"reg": [
{
"registry": {
"issuer": 1,
"revoked": [],
"rid": 10
},
"rid": 10
},
{
"registry": {
"issuer": 2,
"revoked": [
1020
],
"rid": 20
},
"rid": 20
}
]
},
"oracle": {
"receipted": true,
"signatureEpoch": null,
"signed": true
}
}
Caller obtains:
{
"status": "refused",
"refusal": "mirror.push-refused"
}
Register
As a caller, I want to introduce an issuer checkpoint into the mirror model.
Operation: mirror.register. The corpus contains 2 observations.
Named refusals:
mirror.register-refused: The named executable source operation returns none.
Accepted example
Caller supplies this model fixture:
{
"params": {
"toadFloor": 2
},
"action": {
"action": "mirror.register",
"aid": 3,
"epoch": 0,
"parent": null,
"toad": 2
},
"state": {
"ckpt": [
{
"aid": 1,
"checkpoint": {
"aid": 1,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
},
{
"aid": 2,
"checkpoint": {
"aid": 2,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
}
],
"reg": []
},
"oracle": {
"receipted": true,
"signatureEpoch": null,
"signed": true
}
}
Caller obtains:
{
"status": "accepted",
"value": {
"ckpt": [
{
"aid": 1,
"checkpoint": {
"aid": 1,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
},
{
"aid": 2,
"checkpoint": {
"aid": 2,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
},
{
"aid": 3,
"checkpoint": {
"aid": 3,
"cur": 0,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
}
],
"latest": 0,
"parent": null
}
}
],
"reg": []
}
}
Refused example
Caller supplies this model fixture:
{
"params": {
"toadFloor": 2
},
"action": {
"action": "mirror.register",
"aid": 1,
"epoch": 0,
"parent": null,
"toad": 2
},
"state": {
"ckpt": [
{
"aid": 1,
"checkpoint": {
"aid": 1,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
},
{
"aid": 2,
"checkpoint": {
"aid": 2,
"cur": 2,
"hist": [
{
"leaf": {
"epoch": 0,
"prev": null,
"toad": 2
},
"sn": 0
},
{
"leaf": {
"epoch": 1,
"prev": 0,
"toad": 2
},
"sn": 10
},
{
"leaf": {
"epoch": 2,
"prev": 10,
"toad": 2
},
"sn": 20
}
],
"latest": 20,
"parent": null
}
}
],
"reg": []
},
"oracle": {
"receipted": true,
"signatureEpoch": null,
"signed": true
}
}
Caller obtains:
{
"status": "refused",
"refusal": "mirror.register-refused"
}
Download every example · Read the complete shape · Read semantics and limits