AD-31 Coverage Predicates

AD-31 coverage predicates

Generated by npm run generate:ad31-table. Do not edit: npm run check:ad31-table compares this file byte for byte against the builder and fails on any difference.

AD-20’s seven discipline rules, each with a relevance predicate and a satisfaction predicate, run over the hand-authored contract corpus AD-31 names as their publication target. The historical worked example is not a publication target and appears nowhere below.

The fourteen predicates

Rule	Relevance predicate	Satisfaction predicate
success-indicator-separation	success-indicator-separation-relevance	success-indicator-separation-satisfaction
whole-body	whole-body-relevance	whole-body-satisfaction
malformed-input	malformed-input-relevance	malformed-input-satisfaction
per-record	per-record-relevance	per-record-satisfaction
sibling-cross-check	sibling-cross-check-relevance	sibling-cross-check-satisfaction
omission-and-completeness	omission-and-completeness-relevance	omission-and-completeness-satisfaction
state-change-read-back	state-change-read-back-relevance	state-change-read-back-satisfaction

Declaration-state coverage

Rule	Absent	Explicitly empty	Witnessed	Unwitnessed
success-indicator-separation	absent-success-indicator	empty-channel-roles	satisfied-declarations	split-indicator-oracle
whole-body	no-operation-inventory	single-required-response-key	satisfied-declarations	per-key-split-oracles
malformed-input	no-operation-inventory	empty-request-shapes	satisfied-declarations	no-type-violating-step
per-record	absent-collection-locations	empty-collection-locations	satisfied-declarations	no-collection-quantifier
sibling-cross-check	absent-sibling-groups	empty-sibling-groups	satisfied-declarations	unaddressed-parameter-sibling
omission-and-completeness	absent-collection-locations	unnamed-reference-set	satisfied-declarations	wrong-cardinality-form
state-change-read-back	no-operation-inventory	no-state-change-marker	satisfied-declarations	no-read-back-relation

Each cell names the corpus contract that occupies it. Relevance false with satisfaction false occupies no cell and cannot: a rule that is relevant for no site is satisfied vacuously, so a relevance predicate answering false forces its satisfaction twin to answer true.

Coverage gaps

One CoverageGap record per corpus contract per rule where relevance fired and satisfaction failed.

Contract	Rule	Relevance predicate	Satisfaction predicate	Severity	Why relevance fired	Why satisfaction failed
absent-success-indicator	success-indicator-separation	success-indicator-separation-relevance	success-indicator-separation-satisfaction	critical	operation create-thing nominates no success indicator	operation create-thing nominates no success indicator, so no oracle can separate one from the body
split-indicator-oracle	success-indicator-separation	success-indicator-separation-relevance	success-indicator-separation-satisfaction	critical	operation create-thing gives pointer /id a channel role beside its success indicator	no oracle addresses operation create-thing’s success indicator beside another roled pointer at one step, in both channels
split-indicator-oracle	whole-body	whole-body-relevance	whole-body-satisfaction	critical	operation create-thing declares 2 distinct required response keys	no oracle covers every required response key of operation create-thing at one addressed step, in both channels
no-operation-inventory	success-indicator-separation	success-indicator-separation-relevance	success-indicator-separation-satisfaction	critical	the contract declares no operation, so the declaration this rule reads is absent	the contract declares no operation, so the site this rule fires on has no declaration to witness
no-operation-inventory	whole-body	whole-body-relevance	whole-body-satisfaction	critical	the contract declares no operation, so the declaration this rule reads is absent	the contract declares no operation, so the site this rule fires on has no declaration to witness
no-operation-inventory	malformed-input	malformed-input-relevance	malformed-input-satisfaction	critical	the contract declares no operation, so the declaration this rule reads is absent	the contract declares no operation, so the site this rule fires on has no declaration to witness
no-operation-inventory	per-record	per-record-relevance	per-record-satisfaction	critical	the contract declares no operation, so the declaration this rule reads is absent	the contract declares no operation, so the site this rule fires on has no declaration to witness
no-operation-inventory	omission-and-completeness	omission-and-completeness-relevance	omission-and-completeness-satisfaction	critical	the contract declares no operation, so the declaration this rule reads is absent	the contract declares no operation, so the site this rule fires on has no declaration to witness
no-operation-inventory	state-change-read-back	state-change-read-back-relevance	state-change-read-back-satisfaction	critical	the contract declares no operation, so the declaration this rule reads is absent	the contract declares no operation, so the site this rule fires on has no declaration to witness
per-key-split-oracles	whole-body	whole-body-relevance	whole-body-satisfaction	critical	operation create-thing declares 2 distinct required response keys	no oracle covers every required response key of operation create-thing at one addressed step, in both channels
no-type-violating-step	malformed-input	malformed-input-relevance	malformed-input-satisfaction	critical	operation create-thing declares body key name	no step invoking operation create-thing binds a type-violating matcher under a check that addresses it
absent-collection-locations	per-record	per-record-relevance	per-record-satisfaction	critical	operation create-thing declares no collection-location list, so no collection is declared to range over	operation create-thing declares no collection-location list, so no quantifier can range over a declared collection
absent-collection-locations	omission-and-completeness	omission-and-completeness-relevance	omission-and-completeness-satisfaction	critical	operation create-thing declares no collection-location list, so no location can name a reference set	operation create-thing declares no collection-location list, so no location can be reconciled against a reference set
no-collection-quantifier	per-record	per-record-relevance	per-record-satisfaction	critical	operation list-things declares 1 collection location	no check quantifies over collection /items of operation list-things
absent-sibling-groups	sibling-cross-check	sibling-cross-check-relevance	sibling-cross-check-satisfaction	critical	the contract declares no sibling groups	the contract declares no sibling groups, so no group is declared to cross-check
unaddressed-parameter-sibling	sibling-cross-check	sibling-cross-check-relevance	sibling-cross-check-satisfaction	critical	the contract declares 1 operation sibling group	no oracle addresses two members of the parameter sibling group limit and offset in both channels
wrong-cardinality-form	omission-and-completeness	omission-and-completeness-relevance	omission-and-completeness-satisfaction	critical	operation list-things names reference set expected-things for collection /items	no check reconciles collection /items of operation list-things against reference set expected-things in the form its page-bounded cardinality requires
no-read-back-relation	state-change-read-back	state-change-read-back-relevance	state-change-read-back-satisfaction	critical	operation create-thing declares stateChangeMarker: true	no check relates operation create-thing’s call inputs to the response body of a later step that changes no state

The full matrix

Every corpus contract against every rule.

Contract	Rule	Relevant	Satisfied	Gap	Relevance reason	Satisfaction reason
absent-success-indicator	success-indicator-separation	yes	no	yes	operation create-thing nominates no success indicator	operation create-thing nominates no success indicator, so no oracle can separate one from the body
absent-success-indicator	whole-body	yes	yes	no	operation create-thing declares 2 distinct required response keys	every operation declaring more than one required response key has an oracle covering all of them at one step
absent-success-indicator	malformed-input	yes	yes	no	operation create-thing declares body key name	every operation declaring a request key has a type-violating step some check addresses
absent-success-indicator	per-record	yes	yes	no	operation list-things declares 1 collection location	every declared collection location is the collection of some quantifier
absent-success-indicator	sibling-cross-check	yes	yes	no	the contract declares 1 operation sibling group	every declared sibling group has an oracle reading two of its members
absent-success-indicator	omission-and-completeness	yes	yes	no	operation list-things names reference set expected-things for collection /items	every collection location naming a reference set is reconciled against it in the declared form
absent-success-indicator	state-change-read-back	yes	yes	no	operation create-thing declares stateChangeMarker: true	every state-changing operation is read back through a later non-state-changing step
empty-channel-roles	success-indicator-separation	no	yes	no	every operation nominates a success indicator and gives no other pointer a channel role	the rule is relevant for no site, so satisfaction holds vacuously
empty-channel-roles	whole-body	yes	yes	no	operation create-thing declares 2 distinct required response keys	every operation declaring more than one required response key has an oracle covering all of them at one step
empty-channel-roles	malformed-input	yes	yes	no	operation create-thing declares body key name	every operation declaring a request key has a type-violating step some check addresses
empty-channel-roles	per-record	yes	yes	no	operation list-things declares 1 collection location	every declared collection location is the collection of some quantifier
empty-channel-roles	sibling-cross-check	yes	yes	no	the contract declares 1 operation sibling group	every declared sibling group has an oracle reading two of its members
empty-channel-roles	omission-and-completeness	yes	yes	no	operation list-things names reference set expected-things for collection /items	every collection location naming a reference set is reconciled against it in the declared form
empty-channel-roles	state-change-read-back	yes	yes	no	operation create-thing declares stateChangeMarker: true	every state-changing operation is read back through a later non-state-changing step
satisfied-declarations	success-indicator-separation	yes	yes	no	operation create-thing gives pointer /id a channel role beside its success indicator	every operation the rule fires on has an oracle reading its success indicator beside another roled pointer
satisfied-declarations	whole-body	yes	yes	no	operation create-thing declares 2 distinct required response keys	every operation declaring more than one required response key has an oracle covering all of them at one step
satisfied-declarations	malformed-input	yes	yes	no	operation create-thing declares body key name	every operation declaring a request key has a type-violating step some check addresses
satisfied-declarations	per-record	yes	yes	no	operation list-things declares 1 collection location	every declared collection location is the collection of some quantifier
satisfied-declarations	sibling-cross-check	yes	yes	no	the contract declares 1 operation sibling group	every declared sibling group has an oracle reading two of its members
satisfied-declarations	omission-and-completeness	yes	yes	no	operation list-things names reference set expected-things for collection /items	every collection location naming a reference set is reconciled against it in the declared form
satisfied-declarations	state-change-read-back	yes	yes	no	operation create-thing declares stateChangeMarker: true	every state-changing operation is read back through a later non-state-changing step
split-indicator-oracle	success-indicator-separation	yes	no	yes	operation create-thing gives pointer /id a channel role beside its success indicator	no oracle addresses operation create-thing’s success indicator beside another roled pointer at one step, in both channels
split-indicator-oracle	whole-body	yes	no	yes	operation create-thing declares 2 distinct required response keys	no oracle covers every required response key of operation create-thing at one addressed step, in both channels
split-indicator-oracle	malformed-input	yes	yes	no	operation create-thing declares body key name	every operation declaring a request key has a type-violating step some check addresses
split-indicator-oracle	per-record	yes	yes	no	operation list-things declares 1 collection location	every declared collection location is the collection of some quantifier
split-indicator-oracle	sibling-cross-check	yes	yes	no	the contract declares 1 operation sibling group	every declared sibling group has an oracle reading two of its members
split-indicator-oracle	omission-and-completeness	yes	yes	no	operation list-things names reference set expected-things for collection /items	every collection location naming a reference set is reconciled against it in the declared form
split-indicator-oracle	state-change-read-back	yes	yes	no	operation create-thing declares stateChangeMarker: true	every state-changing operation is read back through a later non-state-changing step
no-operation-inventory	success-indicator-separation	yes	no	yes	the contract declares no operation, so the declaration this rule reads is absent	the contract declares no operation, so the site this rule fires on has no declaration to witness
no-operation-inventory	whole-body	yes	no	yes	the contract declares no operation, so the declaration this rule reads is absent	the contract declares no operation, so the site this rule fires on has no declaration to witness
no-operation-inventory	malformed-input	yes	no	yes	the contract declares no operation, so the declaration this rule reads is absent	the contract declares no operation, so the site this rule fires on has no declaration to witness
no-operation-inventory	per-record	yes	no	yes	the contract declares no operation, so the declaration this rule reads is absent	the contract declares no operation, so the site this rule fires on has no declaration to witness
no-operation-inventory	sibling-cross-check	yes	yes	no	the contract declares 1 operation sibling group	every declared sibling group has an oracle reading two of its members
no-operation-inventory	omission-and-completeness	yes	no	yes	the contract declares no operation, so the declaration this rule reads is absent	the contract declares no operation, so the site this rule fires on has no declaration to witness
no-operation-inventory	state-change-read-back	yes	no	yes	the contract declares no operation, so the declaration this rule reads is absent	the contract declares no operation, so the site this rule fires on has no declaration to witness
single-required-response-key	success-indicator-separation	yes	yes	no	operation create-thing gives pointer /id a channel role beside its success indicator	every operation the rule fires on has an oracle reading its success indicator beside another roled pointer
single-required-response-key	whole-body	no	yes	no	no operation declares more than one distinct required response key	the rule is relevant for no site, so satisfaction holds vacuously
single-required-response-key	malformed-input	yes	yes	no	operation create-thing declares body key name	every operation declaring a request key has a type-violating step some check addresses
single-required-response-key	per-record	yes	yes	no	operation list-things declares 1 collection location	every declared collection location is the collection of some quantifier
single-required-response-key	sibling-cross-check	yes	yes	no	the contract declares 1 operation sibling group	every declared sibling group has an oracle reading two of its members
single-required-response-key	omission-and-completeness	yes	yes	no	operation list-things names reference set expected-things for collection /items	every collection location naming a reference set is reconciled against it in the declared form
single-required-response-key	state-change-read-back	yes	yes	no	operation create-thing declares stateChangeMarker: true	every state-changing operation is read back through a later non-state-changing step
per-key-split-oracles	success-indicator-separation	yes	yes	no	operation create-thing gives pointer /id a channel role beside its success indicator	every operation the rule fires on has an oracle reading its success indicator beside another roled pointer
per-key-split-oracles	whole-body	yes	no	yes	operation create-thing declares 2 distinct required response keys	no oracle covers every required response key of operation create-thing at one addressed step, in both channels
per-key-split-oracles	malformed-input	yes	yes	no	operation create-thing declares body key name	every operation declaring a request key has a type-violating step some check addresses
per-key-split-oracles	per-record	yes	yes	no	operation list-things declares 1 collection location	every declared collection location is the collection of some quantifier
per-key-split-oracles	sibling-cross-check	yes	yes	no	the contract declares 1 operation sibling group	every declared sibling group has an oracle reading two of its members
per-key-split-oracles	omission-and-completeness	yes	yes	no	operation list-things names reference set expected-things for collection /items	every collection location naming a reference set is reconciled against it in the declared form
per-key-split-oracles	state-change-read-back	yes	yes	no	operation create-thing declares stateChangeMarker: true	every state-changing operation is read back through a later non-state-changing step
empty-request-shapes	success-indicator-separation	yes	yes	no	operation create-thing gives pointer /id a channel role beside its success indicator	every operation the rule fires on has an oracle reading its success indicator beside another roled pointer
empty-request-shapes	whole-body	yes	yes	no	operation create-thing declares 2 distinct required response keys	every operation declaring more than one required response key has an oracle covering all of them at one step
empty-request-shapes	malformed-input	no	yes	no	no operation declares a request key on any transport channel	the rule is relevant for no site, so satisfaction holds vacuously
empty-request-shapes	per-record	yes	yes	no	operation list-things declares 1 collection location	every declared collection location is the collection of some quantifier
empty-request-shapes	sibling-cross-check	yes	yes	no	the contract declares 1 operation sibling group	every declared sibling group has an oracle reading two of its members
empty-request-shapes	omission-and-completeness	yes	yes	no	operation list-things names reference set expected-things for collection /items	every collection location naming a reference set is reconciled against it in the declared form
empty-request-shapes	state-change-read-back	yes	yes	no	operation create-thing declares stateChangeMarker: true	every state-changing operation is read back through a later non-state-changing step
no-type-violating-step	success-indicator-separation	yes	yes	no	operation create-thing gives pointer /id a channel role beside its success indicator	every operation the rule fires on has an oracle reading its success indicator beside another roled pointer
no-type-violating-step	whole-body	yes	yes	no	operation create-thing declares 2 distinct required response keys	every operation declaring more than one required response key has an oracle covering all of them at one step
no-type-violating-step	malformed-input	yes	no	yes	operation create-thing declares body key name	no step invoking operation create-thing binds a type-violating matcher under a check that addresses it
no-type-violating-step	per-record	yes	yes	no	operation list-things declares 1 collection location	every declared collection location is the collection of some quantifier
no-type-violating-step	sibling-cross-check	yes	yes	no	the contract declares 1 operation sibling group	every declared sibling group has an oracle reading two of its members
no-type-violating-step	omission-and-completeness	yes	yes	no	operation list-things names reference set expected-things for collection /items	every collection location naming a reference set is reconciled against it in the declared form
no-type-violating-step	state-change-read-back	yes	yes	no	operation create-thing declares stateChangeMarker: true	every state-changing operation is read back through a later non-state-changing step
absent-collection-locations	success-indicator-separation	yes	yes	no	operation create-thing gives pointer /id a channel role beside its success indicator	every operation the rule fires on has an oracle reading its success indicator beside another roled pointer
absent-collection-locations	whole-body	yes	yes	no	operation create-thing declares 2 distinct required response keys	every operation declaring more than one required response key has an oracle covering all of them at one step
absent-collection-locations	malformed-input	yes	yes	no	operation create-thing declares body key name	every operation declaring a request key has a type-violating step some check addresses
absent-collection-locations	per-record	yes	no	yes	operation create-thing declares no collection-location list, so no collection is declared to range over	operation create-thing declares no collection-location list, so no quantifier can range over a declared collection
absent-collection-locations	sibling-cross-check	yes	yes	no	the contract declares 1 operation sibling group	every declared sibling group has an oracle reading two of its members
absent-collection-locations	omission-and-completeness	yes	no	yes	operation create-thing declares no collection-location list, so no location can name a reference set	operation create-thing declares no collection-location list, so no location can be reconciled against a reference set
absent-collection-locations	state-change-read-back	yes	yes	no	operation create-thing declares stateChangeMarker: true	every state-changing operation is read back through a later non-state-changing step
empty-collection-locations	success-indicator-separation	yes	yes	no	operation create-thing gives pointer /id a channel role beside its success indicator	every operation the rule fires on has an oracle reading its success indicator beside another roled pointer
empty-collection-locations	whole-body	yes	yes	no	operation create-thing declares 2 distinct required response keys	every operation declaring more than one required response key has an oracle covering all of them at one step
empty-collection-locations	malformed-input	yes	yes	no	operation create-thing declares body key name	every operation declaring a request key has a type-violating step some check addresses
empty-collection-locations	per-record	no	yes	no	every operation declares an explicitly empty collection-location list	the rule is relevant for no site, so satisfaction holds vacuously
empty-collection-locations	sibling-cross-check	yes	yes	no	the contract declares 1 operation sibling group	every declared sibling group has an oracle reading two of its members
empty-collection-locations	omission-and-completeness	no	yes	no	no declared collection location names a reference set	the rule is relevant for no site, so satisfaction holds vacuously
empty-collection-locations	state-change-read-back	yes	yes	no	operation create-thing declares stateChangeMarker: true	every state-changing operation is read back through a later non-state-changing step
no-collection-quantifier	success-indicator-separation	yes	yes	no	operation create-thing gives pointer /id a channel role beside its success indicator	every operation the rule fires on has an oracle reading its success indicator beside another roled pointer
no-collection-quantifier	whole-body	yes	yes	no	operation create-thing declares 2 distinct required response keys	every operation declaring more than one required response key has an oracle covering all of them at one step
no-collection-quantifier	malformed-input	yes	yes	no	operation create-thing declares body key name	every operation declaring a request key has a type-violating step some check addresses
no-collection-quantifier	per-record	yes	no	yes	operation list-things declares 1 collection location	no check quantifies over collection /items of operation list-things
no-collection-quantifier	sibling-cross-check	yes	yes	no	the contract declares 1 operation sibling group	every declared sibling group has an oracle reading two of its members
no-collection-quantifier	omission-and-completeness	yes	yes	no	operation list-things names reference set expected-things for collection /items	every collection location naming a reference set is reconciled against it in the declared form
no-collection-quantifier	state-change-read-back	yes	yes	no	operation create-thing declares stateChangeMarker: true	every state-changing operation is read back through a later non-state-changing step
absent-sibling-groups	success-indicator-separation	yes	yes	no	operation create-thing gives pointer /id a channel role beside its success indicator	every operation the rule fires on has an oracle reading its success indicator beside another roled pointer
absent-sibling-groups	whole-body	yes	yes	no	operation create-thing declares 2 distinct required response keys	every operation declaring more than one required response key has an oracle covering all of them at one step
absent-sibling-groups	malformed-input	yes	yes	no	operation create-thing declares body key name	every operation declaring a request key has a type-violating step some check addresses
absent-sibling-groups	per-record	yes	yes	no	operation list-things declares 1 collection location	every declared collection location is the collection of some quantifier
absent-sibling-groups	sibling-cross-check	yes	no	yes	the contract declares no sibling groups	the contract declares no sibling groups, so no group is declared to cross-check
absent-sibling-groups	omission-and-completeness	yes	yes	no	operation list-things names reference set expected-things for collection /items	every collection location naming a reference set is reconciled against it in the declared form
absent-sibling-groups	state-change-read-back	yes	yes	no	operation create-thing declares stateChangeMarker: true	every state-changing operation is read back through a later non-state-changing step
empty-sibling-groups	success-indicator-separation	yes	yes	no	operation create-thing gives pointer /id a channel role beside its success indicator	every operation the rule fires on has an oracle reading its success indicator beside another roled pointer
empty-sibling-groups	whole-body	yes	yes	no	operation create-thing declares 2 distinct required response keys	every operation declaring more than one required response key has an oracle covering all of them at one step
empty-sibling-groups	malformed-input	yes	yes	no	operation create-thing declares body key name	every operation declaring a request key has a type-violating step some check addresses
empty-sibling-groups	per-record	yes	yes	no	operation list-things declares 1 collection location	every declared collection location is the collection of some quantifier
empty-sibling-groups	sibling-cross-check	no	yes	no	the contract declares explicitly empty operation and parameter sibling groups	the rule is relevant for no site, so satisfaction holds vacuously
empty-sibling-groups	omission-and-completeness	yes	yes	no	operation list-things names reference set expected-things for collection /items	every collection location naming a reference set is reconciled against it in the declared form
empty-sibling-groups	state-change-read-back	yes	yes	no	operation create-thing declares stateChangeMarker: true	every state-changing operation is read back through a later non-state-changing step
unaddressed-parameter-sibling	success-indicator-separation	yes	yes	no	operation create-thing gives pointer /id a channel role beside its success indicator	every operation the rule fires on has an oracle reading its success indicator beside another roled pointer
unaddressed-parameter-sibling	whole-body	yes	yes	no	operation create-thing declares 2 distinct required response keys	every operation declaring more than one required response key has an oracle covering all of them at one step
unaddressed-parameter-sibling	malformed-input	yes	yes	no	operation create-thing declares body key name	every operation declaring a request key has a type-violating step some check addresses
unaddressed-parameter-sibling	per-record	yes	yes	no	operation list-things declares 1 collection location	every declared collection location is the collection of some quantifier
unaddressed-parameter-sibling	sibling-cross-check	yes	no	yes	the contract declares 1 operation sibling group	no oracle addresses two members of the parameter sibling group limit and offset in both channels
unaddressed-parameter-sibling	omission-and-completeness	yes	yes	no	operation list-things names reference set expected-things for collection /items	every collection location naming a reference set is reconciled against it in the declared form
unaddressed-parameter-sibling	state-change-read-back	yes	yes	no	operation create-thing declares stateChangeMarker: true	every state-changing operation is read back through a later non-state-changing step
unnamed-reference-set	success-indicator-separation	yes	yes	no	operation create-thing gives pointer /id a channel role beside its success indicator	every operation the rule fires on has an oracle reading its success indicator beside another roled pointer
unnamed-reference-set	whole-body	yes	yes	no	operation create-thing declares 2 distinct required response keys	every operation declaring more than one required response key has an oracle covering all of them at one step
unnamed-reference-set	malformed-input	yes	yes	no	operation create-thing declares body key name	every operation declaring a request key has a type-violating step some check addresses
unnamed-reference-set	per-record	yes	yes	no	operation list-things declares 1 collection location	every declared collection location is the collection of some quantifier
unnamed-reference-set	sibling-cross-check	yes	yes	no	the contract declares 1 operation sibling group	every declared sibling group has an oracle reading two of its members
unnamed-reference-set	omission-and-completeness	no	yes	no	no declared collection location names a reference set	the rule is relevant for no site, so satisfaction holds vacuously
unnamed-reference-set	state-change-read-back	yes	yes	no	operation create-thing declares stateChangeMarker: true	every state-changing operation is read back through a later non-state-changing step
wrong-cardinality-form	success-indicator-separation	yes	yes	no	operation create-thing gives pointer /id a channel role beside its success indicator	every operation the rule fires on has an oracle reading its success indicator beside another roled pointer
wrong-cardinality-form	whole-body	yes	yes	no	operation create-thing declares 2 distinct required response keys	every operation declaring more than one required response key has an oracle covering all of them at one step
wrong-cardinality-form	malformed-input	yes	yes	no	operation create-thing declares body key name	every operation declaring a request key has a type-violating step some check addresses
wrong-cardinality-form	per-record	yes	yes	no	operation list-things declares 1 collection location	every declared collection location is the collection of some quantifier
wrong-cardinality-form	sibling-cross-check	yes	yes	no	the contract declares 1 operation sibling group	every declared sibling group has an oracle reading two of its members
wrong-cardinality-form	omission-and-completeness	yes	no	yes	operation list-things names reference set expected-things for collection /items	no check reconciles collection /items of operation list-things against reference set expected-things in the form its page-bounded cardinality requires
wrong-cardinality-form	state-change-read-back	yes	yes	no	operation create-thing declares stateChangeMarker: true	every state-changing operation is read back through a later non-state-changing step
no-state-change-marker	success-indicator-separation	yes	yes	no	operation create-thing gives pointer /id a channel role beside its success indicator	every operation the rule fires on has an oracle reading its success indicator beside another roled pointer
no-state-change-marker	whole-body	yes	yes	no	operation create-thing declares 2 distinct required response keys	every operation declaring more than one required response key has an oracle covering all of them at one step
no-state-change-marker	malformed-input	yes	yes	no	operation create-thing declares body key name	every operation declaring a request key has a type-violating step some check addresses
no-state-change-marker	per-record	yes	yes	no	operation list-things declares 1 collection location	every declared collection location is the collection of some quantifier
no-state-change-marker	sibling-cross-check	yes	yes	no	the contract declares 1 operation sibling group	every declared sibling group has an oracle reading two of its members
no-state-change-marker	omission-and-completeness	yes	yes	no	operation list-things names reference set expected-things for collection /items	every collection location naming a reference set is reconciled against it in the declared form
no-state-change-marker	state-change-read-back	no	yes	no	no operation declares stateChangeMarker: true	the rule is relevant for no site, so satisfaction holds vacuously
no-read-back-relation	success-indicator-separation	yes	yes	no	operation create-thing gives pointer /id a channel role beside its success indicator	every operation the rule fires on has an oracle reading its success indicator beside another roled pointer
no-read-back-relation	whole-body	yes	yes	no	operation create-thing declares 2 distinct required response keys	every operation declaring more than one required response key has an oracle covering all of them at one step
no-read-back-relation	malformed-input	yes	yes	no	operation create-thing declares body key name	every operation declaring a request key has a type-violating step some check addresses
no-read-back-relation	per-record	yes	yes	no	operation list-things declares 1 collection location	every declared collection location is the collection of some quantifier
no-read-back-relation	sibling-cross-check	yes	yes	no	the contract declares 1 operation sibling group	every declared sibling group has an oracle reading two of its members
no-read-back-relation	omission-and-completeness	yes	yes	no	operation list-things names reference set expected-things for collection /items	every collection location naming a reference set is reconciled against it in the declared form
no-read-back-relation	state-change-read-back	yes	no	yes	operation create-thing declares stateChangeMarker: true	no check relates operation create-thing’s call inputs to the response body of a later step that changes no state