From 5904a8ae37f4bc1a0a420ca9878adde801ac9ba6 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 2 Nov 2026 00:52:44 +0000 Subject: [PATCH 1/3] Joins: exclusions found through shared keys, not every pair The sola fide joins took the kernel 51 seconds: every one of 6105 pairs of claims was checked for a clash, each check a comparison of whole facts. - Ontology: a meaning's keys are the facts it affirms, denies or holds in a nogood, and the things its relations are about. shares_of_clash: two coherent meanings that clash share a key, since a literal meets its negation in one fact, a rule relates facts about one thing, and a nogood is completed by the other meaning's literal. - Meaning: the definition stays, as exclusionsByPairs. exclusionsUnder now takes the claims from the last to the first, each against an index of the keys of the claims after it, and checks only those it shares a key with. exclusionsUnder_eq: the two are the same list, pair for pair and in order. - Docs: the semantics chapter says how the exclusions are found. - bench: the sola fide exclusions. Pinned: 2318 library definitions for #check_citations. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01BC49XsbtehCbmJMavF1K5Q --- Testimony/Semantics/Meaning.lean | 189 ++++++++++++++++++++++- Testimony/Semantics/Ontology.lean | 100 ++++++++++++ arguments/TestimonyArguments/Checks.lean | 2 +- arguments/bench/Engine.lean | 6 + docs/src/semantics.md | 11 ++ 5 files changed, 304 insertions(+), 4 deletions(-) diff --git a/Testimony/Semantics/Meaning.lean b/Testimony/Semantics/Meaning.lean index 73b51b0..e880548 100644 --- a/Testimony/Semantics/Meaning.lean +++ b/Testimony/Semantics/Meaning.lean @@ -108,13 +108,196 @@ def pairsOf {β : Type} : List β → List (β × β) | x :: xs => xs.map (x, ·) ++ pairsOf xs /-- **Every pair of claims whose meanings exclude each other**, under a given -ontology: `(a, b)`, with `a` listed before `b`, when the two meanings, read for -what their words mean, cannot both be held. -/ -def exclusionsUnder [DecidableEq α] (O : Ontology) : List (α × α) := +ontology, by definition: `(a, b)`, with `a` listed before `b`, when the two +meanings, read for what their words mean, cannot both be held. Every pair is +checked; `exclusionsUnder` computes the same list through shared keys. -/ +def exclusionsByPairs [DecidableEq α] (O : Ontology) : List (α × α) := let shaped := (all : List α).map fun a => (a, Ontology.closed O (means a)) (pairsOf shaped).filterMap fun ((a, s), (b, t)) => if a ≠ b && Ontology.excludes O s t then some (a, b) else none +/-! #### Exclusions through shared keys + +Two coherent meanings clash only where they share a key +(`Testimony.Semantics.Ontology.shares_of_clash`): a fact, or a thing a relation +is about. So the claims are taken from the last to the first, each against an +index from every key to the later claims that hold it, and each claim is +checked only against the claims it shares a key with. A pair sharing nothing is +never compared, which is almost every pair: checking all of them was what made +an argument's joins dear, quadratic in its claims and each check a comparison +of whole facts. The list found is the definition's, pair for pair and in the +same order (`exclusionsUnder_eq`). -/ + +/-- An index from keys to the claims holding them. -/ +abbrev KeyIndex (α : Type) := List (Ontology.Key × List α) + +/-- The claims the index holds under a key. -/ +def KeyIndex.find : KeyIndex α → Ontology.Key → List α + | [], _ => [] + | (k', as) :: rest, k => if k' = k then as else KeyIndex.find rest k + +/-- The index with one more claim under a key. -/ +def KeyIndex.add : KeyIndex α → Ontology.Key → α → KeyIndex α + | [], k, a => [(k, [a])] + | (k', as) :: rest, k, a => + if k' = k then (k', a :: as) :: rest else (k', as) :: KeyIndex.add rest k a + +omit [HasMeanings α] in +theorem KeyIndex.find_add (ix : KeyIndex α) (k k' : Ontology.Key) (a : α) : + KeyIndex.find (KeyIndex.add ix k a) k' = + if k = k' then a :: KeyIndex.find ix k' else KeyIndex.find ix k' := by + induction ix with + | nil => by_cases h : k = k' <;> simp [KeyIndex.add, KeyIndex.find, h] + | cons e rest ih => + obtain ⟨k'', as⟩ := e + by_cases h₁ : k'' = k + · subst h₁ + by_cases h₂ : k'' = k' <;> simp [KeyIndex.add, KeyIndex.find, h₂] + · by_cases h₂ : k'' = k' + · subst h₂ + simp [KeyIndex.add, KeyIndex.find, h₁, Ne.symm h₁] + · simp [KeyIndex.add, KeyIndex.find, h₁, h₂, ih] + +omit [HasMeanings α] in +theorem KeyIndex.mem_find_foldl_add (ks : List Ontology.Key) (a b : α) (k : Ontology.Key) : + ∀ ix : KeyIndex α, b ∈ KeyIndex.find (ks.foldl (fun ix k => KeyIndex.add ix k a) ix) k ↔ + b ∈ KeyIndex.find ix k ∨ (k ∈ ks ∧ b = a) := by + induction ks with + | nil => simp + | cons k₀ ks ih => + intro ix + rw [List.foldl_cons, ih, KeyIndex.find_add] + by_cases h : k₀ = k + · subst h; simp only [if_true, List.mem_cons, true_or, true_and]; tauto + · simp only [h, if_false, List.mem_cons] + constructor + · rintro (h' | ⟨hk, rfl⟩) + · exact .inl h' + · exact .inr ⟨.inr hk, rfl⟩ + · rintro (h' | ⟨hk | hk, rfl⟩) + · exact .inl h' + · exact absurd hk.symm h + · exact .inr ⟨hk, rfl⟩ + +/-- The exclusions among a list of claims, and the index of the coherent ones +by key: the claims from the last to the first, each checked against the later +claims it shares a key with. -/ +def exclusionsGo [DecidableEq α] (O : Ontology) : List α → List (α × α) × KeyIndex α + | [] => ([], []) + | a :: xs => + match exclusionsGo O xs with + | (acc, ix) => + let s := Ontology.closed O (means a) + let c := Ontology.coherent O s + let ks := Ontology.keysOf s + let near := if c then ks.flatMap (KeyIndex.find ix) else [] + let found := xs.filterMap fun b => + let t := Ontology.closed O (means b) + if near.contains b && a ≠ b && Ontology.clash O (s.lits ++ t.lits) (s.nogoods ++ t.nogoods) + then some (a, b) else none + (found ++ acc, if c then ks.foldl (fun ix k => KeyIndex.add ix k a) ix else ix) + +theorem mem_find_exclusionsGo [DecidableEq α] (O : Ontology) (k : Ontology.Key) (b : α) : + ∀ xs : List α, b ∈ KeyIndex.find (exclusionsGo O xs).2 k ↔ + b ∈ xs ∧ Ontology.coherent O (Ontology.closed O (means b)) = true ∧ + k ∈ Ontology.keysOf (Ontology.closed O (means b)) + | [] => by simp [exclusionsGo, KeyIndex.find] + | a :: xs => by + have ih := mem_find_exclusionsGo O k b xs + simp only [exclusionsGo] + split + · rename_i hc + rw [KeyIndex.mem_find_foldl_add, ih] + constructor + · rintro (⟨hb, hcb, hkb⟩ | ⟨hk, rfl⟩) + · exact ⟨List.mem_cons_of_mem _ hb, hcb, hkb⟩ + · exact ⟨List.mem_cons_self, hc, hk⟩ + · rintro ⟨hb, hcb, hkb⟩ + rcases List.mem_cons.mp hb with rfl | hb + · exact .inr ⟨hkb, rfl⟩ + · exact .inl ⟨hb, hcb, hkb⟩ + · rename_i hc + rw [ih] + constructor + · rintro ⟨hb, hcb, hkb⟩ + exact ⟨List.mem_cons_of_mem _ hb, hcb, hkb⟩ + · rintro ⟨hb, hcb, hkb⟩ + rcases List.mem_cons.mp hb with rfl | hb + · exact absurd hcb (by simpa using hc) + · exact ⟨hb, hcb, hkb⟩ + +theorem exclusionsGo_fst [DecidableEq α] (O : Ontology) : ∀ xs : List α, + (exclusionsGo O xs).1 = + (pairsOf (xs.map fun a => (a, Ontology.closed O (means a)))).filterMap + fun ((a, s), (b, t)) => if a ≠ b && Ontology.excludes O s t then some (a, b) else none + | [] => rfl + | a :: xs => by + have ih := exclusionsGo_fst O xs + have hmem := fun k b => mem_find_exclusionsGo O k b xs + rcases h : exclusionsGo O xs with ⟨acc, ix⟩ + rw [h] at ih hmem + simp only at ih hmem + simp only [exclusionsGo, h, List.map_cons, pairsOf, List.filterMap_append, + List.filterMap_map, ← ih] + congr 1 + apply List.filterMap_congr + intro b hb + simp only [Function.comp_apply, Ontology.excludes] + by_cases hca : Ontology.coherent O (Ontology.closed O (means a)) = true + · by_cases hcb : Ontology.coherent O (Ontology.closed O (means b)) = true + · have hnear : ((Ontology.keysOf (Ontology.closed O (means a))).flatMap + (KeyIndex.find ix)).contains b = + (Ontology.keysOf (Ontology.closed O (means a))).any + (· ∈ Ontology.keysOf (Ontology.closed O (means b))) := by + apply Bool.eq_iff_iff.mpr + simp only [List.contains_iff_mem, List.mem_flatMap, List.any_eq_true, decide_eq_true_eq, + hmem] + constructor + · rintro ⟨k, hk, -, -, hkb⟩; exact ⟨k, hk, hkb⟩ + · rintro ⟨k, hk, hkb⟩; exact ⟨k, hk, hb, hcb, hkb⟩ + simp only [hca, hcb, if_true, hnear, Bool.true_and] + by_cases hcl : Ontology.clash O ((Ontology.closed O (means a)).lits ++ + (Ontology.closed O (means b)).lits) ((Ontology.closed O (means a)).nogoods ++ + (Ontology.closed O (means b)).nogoods) = true + · have hsa : Ontology.clash O (Ontology.closed O (means a)).lits + (Ontology.closed O (means a)).nogoods = false := by + simp only [Ontology.coherent, Bool.and_eq_true, Bool.not_eq_true'] at hca; exact hca.2 + have hsb : Ontology.clash O (Ontology.closed O (means b)).lits + (Ontology.closed O (means b)).nogoods = false := by + simp only [Ontology.coherent, Bool.and_eq_true, Bool.not_eq_true'] at hcb; exact hcb.2 + obtain ⟨k, hk, hkb⟩ := Ontology.shares_of_clash hsa hsb hcl + have : (Ontology.keysOf (Ontology.closed O (means a))).any + (· ∈ Ontology.keysOf (Ontology.closed O (means b))) = true := + List.any_eq_true.mpr ⟨k, hk, by simpa using hkb⟩ + simp only [this, hcl, Bool.true_and, Bool.and_true] + · simp only [Bool.not_eq_true] at hcl + simp [hcl] + · simp only [Bool.not_eq_true] at hcb + have hnear : ((Ontology.keysOf (Ontology.closed O (means a))).flatMap + (KeyIndex.find ix)).contains b = false := by + apply Bool.eq_false_iff.mpr + intro hc + obtain ⟨k, -, hk⟩ := List.mem_flatMap.mp (List.contains_iff_mem.mp hc) + obtain ⟨-, hcb', -⟩ := (hmem k b).mp hk + simp [hcb] at hcb' + simp only [hca, if_true, hnear, hcb, Bool.false_and, Bool.and_false, Bool.false_eq_true, + if_false] + · simp only [Bool.not_eq_true] at hca + simp [hca] + +/-- **Every pair of claims whose meanings exclude each other**, under a given +ontology: `(a, b)`, with `a` listed before `b`, when the two meanings, read for +what their words mean, cannot both be held. Computed through shared keys, and +the same list as the definition, `exclusionsByPairs` (`exclusionsUnder_eq`). -/ +def exclusionsUnder [DecidableEq α] (O : Ontology) : List (α × α) := + (exclusionsGo O (all : List α)).1 + +/-- **The exclusions through shared keys are the exclusions**, pair for pair and +in the same order. -/ +theorem exclusionsUnder_eq [DecidableEq α] (O : Ontology) : + exclusionsUnder (α := α) O = exclusionsByPairs O := + exclusionsGo_fst O _ + /-- **Every pair of claims whose meanings entail one another**, under a given ontology: `(a, b)` when the meaning of `a`, read for what its words mean, asserts everything the meaning of `b` does. -/ diff --git a/Testimony/Semantics/Ontology.lean b/Testimony/Semantics/Ontology.lean index 815852e..12a8bf6 100644 --- a/Testimony/Semantics/Ontology.lean +++ b/Testimony/Semantics/Ontology.lean @@ -297,6 +297,106 @@ for what its words mean, every literal of the other and every nogood. -/ def entails (O : Ontology) (s t : Shape) : Bool := coherent O s && t.read && t.lits.all s.lits.contains && t.nogoods.all s.nogoods.contains +/-! ### Where two meanings can meet + +Two meanings can clash only where they touch. A literal meets its negation in +the same fact; a definition's rule (**only**, **functional**) relates two facts +about the same thing; a nogood is completed by the other meaning's literal. +So a meaning's **keys** are the facts of its literals and nogoods, and the +things its relations are about, and two coherent meanings that share no key +cannot clash (`shares_of_clash`). A claim is then checked only against the +claims it shares a key with, found through an index of keys, rather than +against every claim (`Testimony.Semantics.HasMeanings.exclusionsUnder`). -/ + +/-- Where a meaning can meet another: a fact, or a thing a relation is about. -/ +inductive Key + /-- A fact a literal affirms or denies. -/ + | fact (f : Fact) + /-- A thing a relation is about. -/ + | term (t : Term) +deriving DecidableEq + +/-- The keys of one fact: itself, and the things it relates, if a relation. -/ +def factKeys : Fact → List Key + | f@(.rel _ a b) => [.fact f, .term a, .term b] + | f => [.fact f] + +/-- **The keys of a meaning**: those of every fact it affirms or denies, and of +every fact in its nogoods. -/ +def keysOf (s : Shape) : List Key := + s.lits.flatMap (fun l => factKeys l.fact) ++ s.nogoods.flatMap (·.map fun l => Key.fact l.fact) + +theorem fact_mem_factKeys (f : Fact) : Key.fact f ∈ factKeys f := by + cases f <;> simp [factKeys] + +theorem mem_keysOf_of_lit {s : Shape} {l : Lit} {k : Key} (hl : l ∈ s.lits) + (hk : k ∈ factKeys l.fact) : k ∈ keysOf s := by + simp only [keysOf, List.mem_append, List.mem_flatMap] + exact .inl ⟨l, hl, hk⟩ + +theorem mem_keysOf_of_nogood {s : Shape} {n : List Lit} {x : Lit} (hn : n ∈ s.nogoods) + (hx : x ∈ n) : Key.fact x.fact ∈ keysOf s := by + simp only [keysOf, List.mem_append, List.mem_flatMap, List.mem_map] + exact .inr ⟨n, hn, x, hx, rfl⟩ + +/-- A definition's rule makes two literals clash only when their relations are +about one same thing. -/ +theorem shares_of_clashes {a : Axiom} {l m : Lit} (h : a.clashes l m = true) : + ∃ t, Key.term t ∈ factKeys l.fact ∧ Key.term t ∈ factKeys m.fact := by + unfold Axiom.clashes at h + split at h + · rename_i _ _ _ _ b _ _ d + simp only [Bool.and_eq_true, beq_iff_eq, bne_iff_ne, ne_eq] at h + obtain ⟨⟨⟨-, -⟩, hbd⟩, -⟩ := h + exact ⟨b, by simp [factKeys], by simp [factKeys, hbd]⟩ + · rename_i _ _ a _ _ c _ + simp only [Bool.and_eq_true, beq_iff_eq, bne_iff_ne, ne_eq] at h + obtain ⟨⟨⟨-, -⟩, hac⟩, -⟩ := h + exact ⟨a, by simp [factKeys], by simp [factKeys, hac]⟩ + · simp at h + +/-- **Two coherent meanings that clash share a key.** A clash between them is +a literal and its negation, two literals a rule sets against each other, or a +nogood of one completed by the other; none of these is inside one meaning alone, +since each is coherent, so each joins the two, at a fact or at a thing their +relations are about. -/ +theorem shares_of_clash {O : Ontology} {s t : Shape} (hs : clash O s.lits s.nogoods = false) + (ht : clash O t.lits t.nogoods = false) + (h : clash O (s.lits ++ t.lits) (s.nogoods ++ t.nogoods) = true) : + ∃ k ∈ keysOf s, k ∈ keysOf t := by + simp only [clash, Bool.or_eq_false_iff, Bool.or_eq_true, List.any_eq_false, List.any_eq_true, + List.all_eq_true, List.contains_iff_mem, List.mem_append, Bool.not_eq_true] at hs ht h + obtain ⟨⟨hs₁, hs₂⟩, hs₃⟩ := hs + obtain ⟨⟨ht₁, ht₂⟩, ht₃⟩ := ht + rcases h with (⟨l, hl, hn⟩ | ⟨l, hl, m, hm, d, hd, hc⟩) | ⟨n, hn, hall⟩ + · -- a literal and its negation + rcases hl with hl | hl <;> rcases hn with hn | hn + · exact absurd (by simpa using hn) (hs₁ l hl) + · exact ⟨_, mem_keysOf_of_lit hl (fact_mem_factKeys _), + mem_keysOf_of_lit hn (fact_mem_factKeys _)⟩ + · exact ⟨_, mem_keysOf_of_lit hn (fact_mem_factKeys _), + mem_keysOf_of_lit hl (fact_mem_factKeys _)⟩ + · exact absurd (by simpa using hn) (ht₁ l hl) + · -- a rule setting two literals against each other + obtain ⟨u, hu₁, hu₂⟩ := shares_of_clashes hc + rcases hl with hl | hl <;> rcases hm with hm | hm + · exact absurd ⟨m, hm, d, hd, hc⟩ (hs₂ l hl) + · exact ⟨_, mem_keysOf_of_lit hl hu₁, mem_keysOf_of_lit hm hu₂⟩ + · exact ⟨_, mem_keysOf_of_lit hm hu₂, mem_keysOf_of_lit hl hu₁⟩ + · exact absurd ⟨m, hm, d, hd, hc⟩ (ht₂ l hl) + · -- a nogood completed across the two + rcases hn with hn | hn + · obtain ⟨x, hx, hxs⟩ : ∃ x ∈ n, x ∉ s.lits := + Classical.byContradiction fun hno => + hs₃ n hn fun x hx => Classical.byContradiction fun hxs => hno ⟨x, hx, hxs⟩ + have hxt : x ∈ t.lits := (hall x hx).resolve_left hxs + exact ⟨_, mem_keysOf_of_nogood hn hx, mem_keysOf_of_lit hxt (fact_mem_factKeys _)⟩ + · obtain ⟨x, hx, hxt⟩ : ∃ x ∈ n, x ∉ t.lits := + Classical.byContradiction fun hno => + ht₃ n hn fun x hx => Classical.byContradiction fun hxt => hno ⟨x, hx, hxt⟩ + have hxs : x ∈ s.lits := (hall x hx).resolve_right hxt + exact ⟨_, mem_keysOf_of_lit hxs (fact_mem_factKeys _), mem_keysOf_of_nogood hn hx⟩ + end Ontology end Testimony.Semantics diff --git a/arguments/TestimonyArguments/Checks.lean b/arguments/TestimonyArguments/Checks.lean index 3d4c82f..0fc1777 100644 --- a/arguments/TestimonyArguments/Checks.lean +++ b/arguments/TestimonyArguments/Checks.lean @@ -101,7 +101,7 @@ The canonical witness #check_refutations under TestimonyArguments using unfoldSets /-- -info: every entry is a tagged definition, and every key names one: 2298 definitions, 176 entries +info: every entry is a tagged definition, and every key names one: 2318 definitions, 176 entries -/ #guard_msgs in #check_citations under Testimony diff --git a/arguments/bench/Engine.lean b/arguments/bench/Engine.lean index 3fcb072..f530e6b 100644 --- a/arguments/bench/Engine.lean +++ b/arguments/bench/Engine.lean @@ -33,6 +33,8 @@ The benchmarks, from the smallest unit up: arguments' own tables are proved; and a row of a hearing, where every party's inferences are re-rated under a standard, with the parties' re-rated strengths; - **a verdict**: the solver's checked witness for each of the two disputes; +- **the joins**: the exclusions among sola fide's 111 claims, read for what + their words mean; - **an assessment** and **a rating**: Miller's dissent, searched and certified, and the laws' step; - **`establish`** on a package, the tactic every package's soundness uses; @@ -255,6 +257,10 @@ example (j : JamesParty) : (rerated_strength .evidence .trentOnTheWord) (rerated_strength .evidence j) ?_ cases j <;> horn_certify +#bench (runs := 1) "joins: sola fide exclusions, 111 claims" in +example : (Testimony.Semantics.HasMeanings.exclusions (α := Claim)).length = 6 := by + decide +kernel + #bench "verdict: sola fide, only Paul's word unanswered" in example : Verdict solaFideDispute where finite := solaFideFinite diff --git a/docs/src/semantics.md b/docs/src/semantics.md index 34817d8..7a491b9 100644 --- a/docs/src/semantics.md +++ b/docs/src/semantics.md @@ -123,6 +123,17 @@ all, how many claims use each defined word as doctrine or of a text or voice, an each definition contributes: those found with it and not with it taken out. It fails the build if any meaning contradicts itself. +**How the exclusions are found.** Two meanings can clash only where they touch: a literal +meets its negation in one fact, a definition's rule relates two facts about one thing, a +nogood is completed by the other meaning's literal. So each meaning's **keys** are its facts +and the things its relations are about, and two coherent meanings that share no key cannot +exclude each other (`Testimony.Semantics.Ontology.shares_of_clash`). The claims are taken one +by one against an index of the keys of the claims after them, and each is checked only against +those it shares a key with, not against every claim. The list found is the definition's, pair +for pair and in order (`Testimony.Semantics.HasMeanings.exclusionsUnder_eq`), and it is +checked by the kernel in a fraction of the time: every pair compared, the sola fide joins took +the kernel 51 seconds. + The first article, `Testimony.Ontology.Relations`, writes out three definitions the vocabulary already gave in words: "not a ground" is the denial of "a ground"; the only means of a thing is a means of it, and nothing else is; the whole ground of a thing is a ground of it, and nothing From 4d1d75e8f9e585ca4ac6238600c3f94df3d42800 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 2 Nov 2026 01:29:07 +0000 Subject: [PATCH 2/3] Ledger: round 7, exclusions through shared keys The sola fide exclusions 45.0 s to 13.0 s and 3.43 to 1.03 GiB (p = 0.008); the arguments' clean build 204 s at a 10.9 GiB peak, the kernel replay's peak 6.9 GiB. Two wrong first guesses recorded, and the entailments left as they are. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01BC49XsbtehCbmJMavF1K5Q --- docs/src/performance.md | 33 +++++++++++++++++++++++++++++---- 1 file changed, 29 insertions(+), 4 deletions(-) diff --git a/docs/src/performance.md b/docs/src/performance.md index 83aad5a..2eaf78e 100644 --- a/docs/src/performance.md +++ b/docs/src/performance.md @@ -76,6 +76,31 @@ The slowest modules of the arguments' build: `SolaFide.Ratings` (150 s), | 4 | Certify assessments and consistency; in a hearing, weigh a step's rank only once it is attacked (#183) | the hearings and assessments | 3.08 s, 97 MiB | 0.48 s, 16 MiB | 0.008 | kept | | 5 | Compare a citation by its key and locus, a key checked to name one entry | a hearing's rerated strengths | 2.54 s, 83 MiB | 0.86 s, 25 MiB | 0.008 | kept | | 6 | Replay a refutation on bitmasks (#180) | the certified defeat tables | 7.21 s, 94 MiB | 5.99 s, 70 MiB | 0.008 | kept | +| 7 | Find exclusions through shared keys, not every pair | the sola fide joins | 45.0 s, 3.43 GiB | 13.0 s, 1.03 GiB | 0.008 | kept | + +Round 7, `scripts/bench-ab.sh` against `main`, five interleaved rounds. A +profile of `Meanings.SolaFide` put 51 of its 64 seconds in one proof: that the +pinned exclusions are what the meanings contain, which the kernel checked by +testing every one of the 6105 pairs of the argument's 111 claims for a clash. +Two first guesses were wrong, and are recorded so that nobody tries them again: +that the kernel closed each meaning again for every pair (a table of closed +meanings, and one of their coherence, each checked once, changed nothing, +44 s), and that the closing was the cost (it is 0.4 s for every claim). The +cost was the clash check itself, comparing whole facts and terms a field at a +time, some 400,000 comparisons. Two coherent meanings can clash only where they +share a key, a fact or a thing their relations are about +(`Ontology.shares_of_clash`), so the claims are now taken from the last to the +first against an index of the later claims' keys, and each is checked only +against those it shares a key with; `HasMeanings.exclusionsUnder_eq` proves the +list the same, pair for pair and in order. The exclusions fell from 45.0 s to +13.0 s (−71%, p = 0.008) and from 3.43 to 1.03 GiB. The entailments were tried +the same way, indexed by each claim's first literal, and gained only 9.7 s to +8.3 s: their check already stops at the first missing literal, so the pairs +themselves are the cost, and the index does not remove them. They are left as +they are. Measured by hand, clean, on the same machine: the arguments' +`lake build` fell from 225 s to 204 s and its peak from 13.8 to 10.9 GiB, and +the kernel replay's peak from 9.3 to 6.9 GiB, at 226 s: the exclusions proof +was the largest single holder of memory in either. Round 6, `scripts/bench-ab.sh` against `main`, five interleaved rounds. A certified refutation was replayed over lists of settled atoms, each membership @@ -165,7 +190,7 @@ of memory. Two run in 293 s; one in 500 s with about 5.2 GiB. ## Fixed points -None yet. After round 6 the largest benchmarks are still the defeat tables, -about 80 ms a sola fide cell, of which converting each position to clauses and -the search at elaboration are now most; and the slowest modules of the build -are the meanings of sola fide and its dispute. +None yet. After round 7 the sola fide joins take 25 s of their module, of which +the entailments are 9 s; the next candidates are the support and part-of tables, +which still search in the kernel, and the models `satisfied_by` checks with +`simp`. From 9d8772fab82de120f7dfc6afcc3dc251c0c4f842 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 2 Nov 2026 02:34:32 +0000 Subject: [PATCH 3/3] Joins: close each meaning once, before the walk The key-index walk closed each later claim's meaning again for every claim before it. The kernel shares those repeated terms, so the proof was not slowed, but the ontology check runs the same function compiled, once for every definition, and paid for each closing: CI's benchmark gate found it 5% slower than main (p = 0.008). `exclusionsGo` now walks the claims already paired with their closed meanings (`HasMeanings.shapedUnder`), and `exclusionsUnder_eq` still proves the list the pairwise definition's. Against main, five interleaved rounds: the ontology check 3.16 s to 1.69 s (-47%, p = 0.008); the sola fide exclusions 45.4 s to 10.6 s (-77%, p = 0.008), 3.43 to 1.06 GiB. Ledger round 7 updated; the citation check's pin moves to 2319 definitions. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01BC49XsbtehCbmJMavF1K5Q --- Testimony/Semantics/Meaning.lean | 43 ++++++++++++++---------- arguments/TestimonyArguments/Checks.lean | 2 +- docs/src/performance.md | 15 ++++++--- 3 files changed, 37 insertions(+), 23 deletions(-) diff --git a/Testimony/Semantics/Meaning.lean b/Testimony/Semantics/Meaning.lean index e880548..038a730 100644 --- a/Testimony/Semantics/Meaning.lean +++ b/Testimony/Semantics/Meaning.lean @@ -179,32 +179,36 @@ theorem KeyIndex.mem_find_foldl_add (ks : List Ontology.Key) (a b : α) (k : Ont · exact absurd hk.symm h · exact .inr ⟨hk, rfl⟩ -/-- The exclusions among a list of claims, and the index of the coherent ones -by key: the claims from the last to the first, each checked against the later -claims it shares a key with. -/ -def exclusionsGo [DecidableEq α] (O : Ontology) : List α → List (α × α) × KeyIndex α +/-- The exclusions among a list of claims, each with its meaning read under the +ontology, and the index of the coherent ones by key: the claims from the last +to the first, each checked against the later claims it shares a key with. Each +meaning is read once, before the walk, and not once for every pair. -/ +def exclusionsGo [DecidableEq α] (O : Ontology) : + List (α × Shape) → List (α × α) × KeyIndex α | [] => ([], []) - | a :: xs => - match exclusionsGo O xs with + | (a, s) :: ys => + match exclusionsGo O ys with | (acc, ix) => - let s := Ontology.closed O (means a) let c := Ontology.coherent O s let ks := Ontology.keysOf s let near := if c then ks.flatMap (KeyIndex.find ix) else [] - let found := xs.filterMap fun b => - let t := Ontology.closed O (means b) + let found := ys.filterMap fun (b, t) => if near.contains b && a ≠ b && Ontology.clash O (s.lits ++ t.lits) (s.nogoods ++ t.nogoods) then some (a, b) else none (found ++ acc, if c then ks.foldl (fun ix k => KeyIndex.add ix k a) ix else ix) +/-- Each claim with its meaning read under the ontology. -/ +def shapedUnder (O : Ontology) (xs : List α) : List (α × Shape) := + xs.map fun a => (a, Ontology.closed O (means a)) + theorem mem_find_exclusionsGo [DecidableEq α] (O : Ontology) (k : Ontology.Key) (b : α) : - ∀ xs : List α, b ∈ KeyIndex.find (exclusionsGo O xs).2 k ↔ + ∀ xs : List α, b ∈ KeyIndex.find (exclusionsGo O (shapedUnder O xs)).2 k ↔ b ∈ xs ∧ Ontology.coherent O (Ontology.closed O (means b)) = true ∧ k ∈ Ontology.keysOf (Ontology.closed O (means b)) - | [] => by simp [exclusionsGo, KeyIndex.find] + | [] => by simp [shapedUnder, exclusionsGo, KeyIndex.find] | a :: xs => by have ih := mem_find_exclusionsGo O k b xs - simp only [exclusionsGo] + simp only [shapedUnder, List.map_cons, exclusionsGo] at ih ⊢ split · rename_i hc rw [KeyIndex.mem_find_foldl_add, ih] @@ -227,18 +231,21 @@ theorem mem_find_exclusionsGo [DecidableEq α] (O : Ontology) (k : Ontology.Key) · exact ⟨hb, hcb, hkb⟩ theorem exclusionsGo_fst [DecidableEq α] (O : Ontology) : ∀ xs : List α, - (exclusionsGo O xs).1 = - (pairsOf (xs.map fun a => (a, Ontology.closed O (means a)))).filterMap + (exclusionsGo O (shapedUnder O xs)).1 = + (pairsOf (shapedUnder O xs)).filterMap fun ((a, s), (b, t)) => if a ≠ b && Ontology.excludes O s t then some (a, b) else none | [] => rfl | a :: xs => by have ih := exclusionsGo_fst O xs have hmem := fun k b => mem_find_exclusionsGo O k b xs - rcases h : exclusionsGo O xs with ⟨acc, ix⟩ + rcases h : exclusionsGo O (shapedUnder O xs) with ⟨acc, ix⟩ rw [h] at ih hmem simp only at ih hmem - simp only [exclusionsGo, h, List.map_cons, pairsOf, List.filterMap_append, - List.filterMap_map, ← ih] + have hcons : shapedUnder O (a :: xs) = (a, Ontology.closed O (means a)) :: shapedUnder O xs := + rfl + rw [hcons] + simp only [exclusionsGo, h, pairsOf, List.filterMap_append, List.filterMap_map, ← ih] + simp only [shapedUnder, List.filterMap_map] congr 1 apply List.filterMap_congr intro b hb @@ -290,7 +297,7 @@ ontology: `(a, b)`, with `a` listed before `b`, when the two meanings, read for what their words mean, cannot both be held. Computed through shared keys, and the same list as the definition, `exclusionsByPairs` (`exclusionsUnder_eq`). -/ def exclusionsUnder [DecidableEq α] (O : Ontology) : List (α × α) := - (exclusionsGo O (all : List α)).1 + (exclusionsGo O (shapedUnder O (all : List α))).1 /-- **The exclusions through shared keys are the exclusions**, pair for pair and in the same order. -/ diff --git a/arguments/TestimonyArguments/Checks.lean b/arguments/TestimonyArguments/Checks.lean index 0fc1777..fd4161c 100644 --- a/arguments/TestimonyArguments/Checks.lean +++ b/arguments/TestimonyArguments/Checks.lean @@ -101,7 +101,7 @@ The canonical witness #check_refutations under TestimonyArguments using unfoldSets /-- -info: every entry is a tagged definition, and every key names one: 2318 definitions, 176 entries +info: every entry is a tagged definition, and every key names one: 2319 definitions, 176 entries -/ #guard_msgs in #check_citations under Testimony diff --git a/docs/src/performance.md b/docs/src/performance.md index 2eaf78e..80100d4 100644 --- a/docs/src/performance.md +++ b/docs/src/performance.md @@ -76,7 +76,7 @@ The slowest modules of the arguments' build: `SolaFide.Ratings` (150 s), | 4 | Certify assessments and consistency; in a hearing, weigh a step's rank only once it is attacked (#183) | the hearings and assessments | 3.08 s, 97 MiB | 0.48 s, 16 MiB | 0.008 | kept | | 5 | Compare a citation by its key and locus, a key checked to name one entry | a hearing's rerated strengths | 2.54 s, 83 MiB | 0.86 s, 25 MiB | 0.008 | kept | | 6 | Replay a refutation on bitmasks (#180) | the certified defeat tables | 7.21 s, 94 MiB | 5.99 s, 70 MiB | 0.008 | kept | -| 7 | Find exclusions through shared keys, not every pair | the sola fide joins | 45.0 s, 3.43 GiB | 13.0 s, 1.03 GiB | 0.008 | kept | +| 7 | Find exclusions through shared keys, not every pair | the sola fide joins | 45.4 s, 3.43 GiB | 10.6 s, 1.06 GiB | 0.008 | kept | Round 7, `scripts/bench-ab.sh` against `main`, five interleaved rounds. A profile of `Meanings.SolaFide` put 51 of its 64 seconds in one proof: that the @@ -92,12 +92,19 @@ share a key, a fact or a thing their relations are about (`Ontology.shares_of_clash`), so the claims are now taken from the last to the first against an index of the later claims' keys, and each is checked only against those it shares a key with; `HasMeanings.exclusionsUnder_eq` proves the -list the same, pair for pair and in order. The exclusions fell from 45.0 s to -13.0 s (−71%, p = 0.008) and from 3.43 to 1.03 GiB. The entailments were tried +list the same, pair for pair and in order. The first version walked the claims +themselves and closed each later claim's meaning again for every claim before +it. The kernel shares those repeated terms, so its build was not slowed, but +the ontology check runs the same function compiled, once for every +definition, and there each closing was paid again: CI's gate found that check +5% slower (p = 0.008). So each meaning is now closed once, before the walk +(`HasMeanings.shapedUnder`). The exclusions fell from 45.4 s to 10.6 s (−77%, +p = 0.008) and from 3.43 to 1.06 GiB, and the ontology check from 3.16 s to +1.69 s (−47%, p = 0.008). The entailments were tried the same way, indexed by each claim's first literal, and gained only 9.7 s to 8.3 s: their check already stops at the first missing literal, so the pairs themselves are the cost, and the index does not remove them. They are left as -they are. Measured by hand, clean, on the same machine: the arguments' +they are. Measured by hand on the first version, clean, on the same machine: the arguments' `lake build` fell from 225 s to 204 s and its peak from 13.8 to 10.9 GiB, and the kernel replay's peak from 9.3 to 6.9 GiB, at 226 s: the exclusions proof was the largest single holder of memory in either.