Soundness of lightweight coverage-summary audits

def Erdos97Octagon.RawIncidence.PatternSummary.Valid (summary : PatternSummary) : Prop

A pattern summary denotes a checked obstruction with the advertised fields.

Equations

• summary.Valid = ∃ (entry : Erdos97Octagon.RawIncidence.PatternEntry), entry.origin = summary.origin ∧ entry.mask = summary.mask ∧ entry.validB = true

def Erdos97Octagon.RawIncidence.HardSummary.Valid (summary : HardSummary) : Prop

An exact-table summary denotes a checked obstruction with the advertised fields.

Equations

• summary.Valid = ∃ (entry : Erdos97Octagon.RawIncidence.HardEntry), entry.origin = summary.origin ∧ entry.code = summary.code ∧ entry.validB = true

theorem Erdos97Octagon.RawIncidence.PatternSummary.valid_of_validAgainstB {buckets : Array (List PatternEntry)} {summary : PatternSummary} (hvalid : validAgainstB buckets summary = true) : summary.Valid

A successful Boolean lookup gives the obstruction denoted by a pattern summary.

theorem Erdos97Octagon.RawIncidence.HardSummary.valid_of_validAgainstB {buckets : Array (List HardEntry)} {summary : HardSummary} (hvalid : validAgainstB buckets summary = true) : summary.Valid

A successful Boolean lookup gives the obstruction denoted by an exact summary.

theorem Erdos97Octagon.RawIncidence.PatternSummary.valid_of_data {summary : PatternSummary} (hmember : ∃ shard ∈ patternSummaryBucketGroups.toList, ∃ bucket ∈ shard.toList, summary ∈ bucket) : summary.Valid

Every generated pattern summary has the obstruction certified by its source shard.

theorem Erdos97Octagon.RawIncidence.HardSummary.valid_of_data {summary : HardSummary} (hmember : ∃ shard ∈ hardSummaryBucketGroups.toList, ∃ bucket ∈ shard.toList, summary ∈ bucket) : summary.Valid

Every generated hard summary has the obstruction certified by its source shard.

theorem Erdos97Octagon.RawIncidence.PatternSummary.valid_of_memberB {summary : PatternSummary} (hmember : summary.memberB = true) : summary.Valid

Membership in the generated pattern-summary table supplies its audited entry.

theorem Erdos97Octagon.RawIncidence.HardSummary.valid_of_memberB {summary : HardSummary} (hmember : summary.memberB = true) : summary.Valid

Membership in the generated exact-summary table supplies its audited entry.