Skip to content

Commit 6d2430e

Browse files
committed
engine: delete verdict.conf, not wire it to the floor
A verdict carried a confidence that nothing read. Five sites wrote it and none consumed it: the only readers of a stored verdict are same_verdict(), comparing target, kind and origin, and evidence_resolve(), reading kind and target. It looked like the floor gate for curation, and a rule author would reasonably have believed it was one. No such gate belongs there, for the reason that already makes constraint rules sound. resolve_evidence() gates observations and coverings before curate_to_fixpoint() runs and again after every round; a verdict_fn is handed the evidence set and nothing else; and all seven curation rules skip invalid observations. In a floored run there is no sub-floor evidence for a curation rule to see, so every verdict it emits is derived purely from at-or-above-floor inputs by construction. The two windows do not share rulings either, the caller clearing n_verdicts between them. Gating coverings closed the last hole in that chain. The field was also incoherent. Most writers set it to the confidence of the observation being invalidated, firmware_memmap_holes to that of the evidence justifying the retraction, and only the second reading would make a floor test mean anything -- so wiring it up as written would have produced arbitrary results. A future curation kind wanting a strength value would have had to redefine it across every writer regardless, which is no cheaper than adding a defined field then. derived_from and lineage_count stay, but not because they work: three of the four rules set derived_from[0] to the target's own id, duplicating observation_id, and only x86_64_vmalloc_vmemmap_invariant records the other side of the comparison that justified the drop. Nothing consumes them, so the gap is inert. They are kept as a data field with an obvious meaning rather than a mechanism something could mistake for enforcing soundness, and the comment now states what a future consumer has to fix first. origin stays because dedup compares it.
1 parent 2a71c06 commit 6d2430e

6 files changed

Lines changed: 26 additions & 24 deletions

File tree

src/include/kasld/engine_rules.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,6 @@ static inline int kasld_emit_va_band_verdicts(const struct evidence_set *ev,
6868
memset(v, 0, sizeof(*v));
6969
v->observation_id = o->id;
7070
v->kind = V_INVALID;
71-
v->conf = o->conf;
7271
v->derived_from[0] = o->id;
7372
v->lineage_count = 1;
7473
snprintf(v->origin, ORIGIN_LEN, "%s", origin);

src/include/kasld/evidence.h

Lines changed: 26 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -72,26 +72,34 @@ enum verdict_kind {
7272
V_INVALID = 0, /* drop the observation from the effective set */
7373
};
7474

75+
/* A verdict carries no confidence, deliberately. A retraction needs no floor
76+
* of its own because the floor is already applied to everything a curation rule
77+
* can read: resolve_evidence() gates observations and coverings before
78+
* curate_to_fixpoint() runs and again after every round, and a verdict_fn is
79+
* handed the evidence set and nothing else. So in a floored run every verdict
80+
* is derived purely from at-or-above-floor evidence by construction -- the same
81+
* argument that makes constraint rules sound, and the reason a rule cannot
82+
* label its way around either.
83+
*
84+
* The two windows do not share rulings: the caller clears n_verdicts between
85+
* them, so a verdict formed under the all-signals run never applies to the
86+
* guaranteed one. */
7587
struct verdict {
7688
uint32_t observation_id; /* target observation */
7789
enum verdict_kind kind;
78-
/* Lineage and reporting only. evidence_resolve() applies every verdict
79-
* regardless of this value, so unlike an observation's or a covering's conf
80-
* it is NOT a floor gate -- a curation rule cannot make a retraction
81-
* conditional on the run's floor by setting it, and nothing else reads it.
82-
*
83-
* Wiring it to the floor is not a small change, because the writers do not
84-
* currently agree on what it means: most set it to the confidence of the
85-
* observation being invalidated, while firmware_memmap_holes sets it to the
86-
* confidence of the evidence justifying the retraction. Only the second
87-
* reading makes a floor test meaningful, so gating on the field as written
88-
* would produce arbitrary results. Settle the semantics across every writer
89-
* first.
90+
/* Intended as the observations the ruling was drawn from, and not yet that.
91+
* Three of the four curation rules set derived_from[0] to the target's own
92+
* id, duplicating observation_id above; only
93+
* x86_64_vmalloc_vmemmap_invariant records the other side of the comparison
94+
* that justified the drop. Nothing consumes it, so the gap is inert -- dedup
95+
* compares target, kind and origin and ignores lineage on purpose, so two
96+
* rules reaching one ruling by different routes collapse to a single entry.
9097
*
91-
* Coverings are gated at the input instead (see covering_active), which is
92-
* what keeps a below-floor map out of the guaranteed window on the verdict
93-
* path without depending on this. */
94-
enum kasld_confidence conf;
98+
* Kept rather than dropped because it is a data field with an obvious
99+
* meaning, not a mechanism something could mistake for enforcing soundness.
100+
* Anything that starts consuming it has to fix the writers first: a cluster
101+
* filter's justification is the cluster, and a map rule's is the covering,
102+
* neither of which is the observation being dropped. */
95103
uint32_t derived_from[MAX_LINEAGE];
96104
uint8_t lineage_count;
97105
char origin[ORIGIN_LEN]; /* emitting curation rule */
@@ -116,8 +124,8 @@ uint32_t evidence_add(struct evidence_set *ev, const struct observation *src);
116124

117125
/* Append a covering extent (copied). Assigns and returns a fresh id from the
118126
* same id space as observations, and sets valid=1. Coverings carry no
119-
* effective view — they are not curated, only grouped by origin and read by
120-
* map rules — but they do carry the floor gate's verdict on their confidence.
127+
* effective view — they are not curated, and no verdict targets them, only
128+
* grouped by origin and read by map rules — but they do take the floor gate.
121129
* Returns 0 if full. */
122130
uint32_t evidence_add_covering(struct evidence_set *ev,
123131
const struct covering *src);

src/rules/firmware_memmap_holes.c

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,6 @@ int rule_firmware_memmap_holes(const struct evidence_set *ev,
7575
memset(v, 0, sizeof(*v));
7676
v->observation_id = c->id;
7777
v->kind = V_INVALID;
78-
v->conf = c->conf;
7978
v->derived_from[0] = c->id;
8079
v->lineage_count = 1;
8180
snprintf(v->origin, ORIGIN_LEN, "firmware_memmap_holes");

src/rules/text_cluster_filter.c

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,6 @@ int rule_text_cluster_filter(const struct evidence_set *ev, struct verdict *out,
8787
memset(v, 0, sizeof(*v));
8888
v->observation_id = o->id;
8989
v->kind = V_INVALID;
90-
v->conf = o->conf;
9190
v->derived_from[0] = o->id;
9291
v->lineage_count = 1;
9392
snprintf(v->origin, ORIGIN_LEN, "text_cluster_filter");

src/rules/x86_64_vmalloc_vmemmap_invariant.c

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -83,7 +83,6 @@ int rule_x86_64_vmalloc_vmemmap_invariant(const struct evidence_set *ev,
8383
memset(v, 0, sizeof(*v));
8484
v->observation_id = vi->id;
8585
v->kind = V_INVALID;
86-
v->conf = vi->conf;
8786
v->derived_from[0] = vi->id;
8887
v->derived_from[1] = vj->id;
8988
v->lineage_count = 2;
@@ -94,7 +93,6 @@ int rule_x86_64_vmalloc_vmemmap_invariant(const struct evidence_set *ev,
9493
memset(v, 0, sizeof(*v));
9594
v->observation_id = vj->id;
9695
v->kind = V_INVALID;
97-
v->conf = vj->conf;
9896
v->derived_from[0] = vi->id;
9997
v->derived_from[1] = vj->id;
10098
v->lineage_count = 2;

tests/test_evidence.c

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,6 @@ static struct verdict mk_invalidate(uint32_t id, const char *origin) {
3434
memset(&v, 0, sizeof(v));
3535
v.observation_id = id;
3636
v.kind = V_INVALID;
37-
v.conf = CONF_DERIVED;
3837
snprintf(v.origin, ORIGIN_LEN, "%s", origin);
3938
return v;
4039
}

0 commit comments

Comments
 (0)