feat(lenses): the commit-truth lens, repo-facts, as Gate 4
Every claim in every commit message, and in the documentation the range adds or changes, proven or gone. The lens's block kinds are text, doc and slot: a message unit is keyed on its text, the base and the code up to its commit (MessageDeps); a documentation unit on its file, its normalised text, the base and the code of the whole range (DocKeyParts); a diffstat on its text alone; whole:order and whole:absent are asked in slot passes of its own, never stored. A documentation file's diff header and a part the commit writes nothing in are a mechanical n/a. Budgets 60/40 for a text or doc block, 50/35 for a slot; one read. Gate 4, after the proofs, so the messages and documents are read once the code they describe has settled; the owner's gate is 5. The goldens that follow from the lens table are derived by tests/Goldens/derive.py, which asserts that the recorded table still reproduces the recorded entries before it writes. Proven, with the opt-in commit after this one: the suite (26 passed); a dry run of a scratch range (2 commits, a README with sections) by the previous binary and this one with the three static lenses on and the rest off, 25 prompts and 4 system files byte for byte; with repo-facts on as well, those files unchanged and 10 passes and 1 system file added. The lens's firing proof in this pipeline is owed (the owner's go).
This commit is contained in:
parent
61ee4602f4
commit
febbfc3fcc
19 changed files with 2564 additions and 646 deletions
|
|
@ -109,37 +109,45 @@ int main() {
|
|||
const auto g = Gates(Plan::GatesFor());
|
||||
std::vector<std::string> gateNames;
|
||||
for (const auto& [title, lenses] : g) gateNames.push_back(Dyn::Split(title, " — ")[0]);
|
||||
Check("gates: 1 approach, 2 functional, 3 proof - the bug-prover and the security lens side by side (2026-10-22), the owner stays Gate 4",
|
||||
gateNames == std::vector<std::string>{"Gate 1", "Gate 2", "Gate 3"} && g[0].second == std::vector<std::string>{"repo-better-solution.md"} && g[1].second == std::vector<std::string>{Fn}
|
||||
&& g[2].second == std::vector<std::string>{"repo-bug-prover.md", "repo-security.md"});
|
||||
const std::string Facts(Plan::FactsLens);
|
||||
Check("gates: 1 approach, 2 functional, 3 proof - the bug-prover and the security lens side by side (2026-10-22) - 4 commit truth (2026-10-31); the owner is Gate 5",
|
||||
gateNames == std::vector<std::string>{"Gate 1", "Gate 2", "Gate 3", "Gate 4"} && g[0].second == std::vector<std::string>{"repo-better-solution.md"} && g[1].second == std::vector<std::string>{Fn}
|
||||
&& g[2].second == std::vector<std::string>{"repo-bug-prover.md", "repo-security.md"} && g[3] == std::pair<std::string, std::vector<std::string>>{"Gate 4 — Commit truth", {Facts}});
|
||||
const std::vector<std::string> onlyFn = {Fn};
|
||||
const std::vector<std::string> security = {"repo-security.md"};
|
||||
std::set<std::string> lensSet;
|
||||
for (const Plan::Lens& lens : Plan::Lenses) lensSet.emplace(lens.file);
|
||||
using GateList = std::vector<std::pair<std::string, std::vector<std::string>>>;
|
||||
Check("mode_lenses = the four; --only keeps, --without drops, an emptied gate disappears; Gate 3 with one of its lenses dropped keeps the other",
|
||||
Check("mode_lenses = the five; --only keeps, --without drops, an emptied gate disappears; Gate 3 with one of its lenses dropped keeps the other",
|
||||
Set(Plan::ModeLenses()) == lensSet && Gates(Plan::GatesFor(onlyFn)) == GateList{{"Gate 2 — Functional", {Fn}}}
|
||||
&& Titles(Plan::GatesFor({}, onlyFn)) == std::vector<std::string>{"Gate 1 — Approach", "Gate 3 — Proof"} && Plan::GatesFor(onlyFn, onlyFn).empty()
|
||||
&& Gates(Plan::GatesFor({}, security)).back() == std::pair<std::string, std::vector<std::string>>{"Gate 3 — Proof", {"repo-bug-prover.md"}}
|
||||
&& Titles(Plan::GatesFor({}, onlyFn)) == std::vector<std::string>{"Gate 1 — Approach", "Gate 3 — Proof", "Gate 4 — Commit truth"} && Plan::GatesFor(onlyFn, onlyFn).empty()
|
||||
&& Gates(Plan::GatesFor({}, security))[2] == std::pair<std::string, std::vector<std::string>>{"Gate 3 — Proof", {"repo-bug-prover.md"}}
|
||||
&& Gates(Plan::GatesFor(security)) == GateList{{"Gate 3 — Proof", {"repo-security.md"}}});
|
||||
const std::vector<std::string> threeOff = {"repo-better-solution.md", "repo-bug-prover.md", "repo-security.md"};
|
||||
const std::vector<std::string> bugOff = {"repo-bug-prover.md"};
|
||||
Check("lenses off by config: gates_for drops the lens and its gate; --only cannot bring it back", Titles(Plan::GatesFor({}, {}, onlyFn)) == std::vector<std::string>{"Gate 1 — Approach", "Gate 3 — Proof"}
|
||||
&& Plan::GatesFor(onlyFn, {}, onlyFn).empty() && Gates(Plan::GatesFor({}, {}, threeOff)) == GateList{{"Gate 2 — Functional", {Fn}}}
|
||||
&& Gates(Plan::GatesFor({}, {}, bugOff)).back() == std::pair<std::string, std::vector<std::string>>{"Gate 3 — Proof", {"repo-security.md"}});
|
||||
const std::vector<std::string> onlyFacts = {Facts};
|
||||
Check("lenses off by config: gates_for drops the lens and its gate; --only cannot bring it back", Titles(Plan::GatesFor({}, {}, onlyFn)) == std::vector<std::string>{"Gate 1 — Approach", "Gate 3 — Proof", "Gate 4 — Commit truth"}
|
||||
&& Plan::GatesFor(onlyFn, {}, onlyFn).empty() && Gates(Plan::GatesFor({}, {}, threeOff)) == GateList{{"Gate 2 — Functional", {Fn}}, {"Gate 4 — Commit truth", {Facts}}}
|
||||
&& Gates(Plan::GatesFor({}, {}, bugOff))[2] == std::pair<std::string, std::vector<std::string>>{"Gate 3 — Proof", {"repo-security.md"}}
|
||||
&& Gates(Plan::GatesFor(onlyFacts)) == GateList{{"Gate 4 — Commit truth", {Facts}}} && Titles(Plan::GatesFor({}, {}, onlyFacts)).size() == 3);
|
||||
const std::vector<std::string> allLenses(lensSet.begin(), lensSet.end());
|
||||
const std::set<std::string> textAndDoc = {"p1:subject", "p1:diffstat", "p2:subject", "p2:msg", "p2:diffstat", "p2:README.md#hdr", "p2:README.md#1"};
|
||||
const std::set<std::string> nrAll = Set(Plan::NotReviewed(units, lines, Plan::ModeLenses()));
|
||||
Check("not reviewed (every lens runs): the text units and the documentation units", nrAll == std::set<std::string>{"p1:subject", "p1:diffstat", "p2:subject", "p2:msg", "p2:diffstat", "p2:README.md#hdr", "p2:README.md#1"},
|
||||
Show(nrAll));
|
||||
std::vector<std::string> withoutFacts;
|
||||
for (const Plan::Lens& lens : Plan::Lenses) {
|
||||
if (lens.file != Facts) withoutFacts.emplace_back(lens.file);
|
||||
}
|
||||
Check("not reviewed (every lens runs): only the documentation file's header, a mechanical n/a of the commit-truth lens; without that lens the text units and the documentation units",
|
||||
nrAll == std::set<std::string>{"p2:README.md#hdr"} && Set(Plan::NotReviewed(units, lines, withoutFacts)) == textAndDoc, Show(nrAll));
|
||||
std::vector<std::string> statics;
|
||||
for (const Plan::Lens& lens : Plan::Lenses) {
|
||||
if (lens.file != Fn) statics.emplace_back(lens.file);
|
||||
}
|
||||
std::set<std::string> plusBehaviour = nrAll;
|
||||
plusBehaviour.insert("whole:behaviour");
|
||||
std::set<std::string> plusStatic = nrAll;
|
||||
std::set<std::string> plusStatic = textAndDoc;
|
||||
plusStatic.insert({"whole:order", "whole:absent", "p1:outside", "p1:absent", "p2:outside", "p2:absent", "p1:hello.py#hdr", "p2:hello.py#hdr"});
|
||||
Check("not reviewed is derived from the lenses that run: the functional lens off adds whole:behaviour; only the functional lens adds the static slots and the file headers (a mechanical n/a is no reading)",
|
||||
Check("not reviewed is derived from the lenses that run: the functional lens off adds whole:behaviour; only the functional lens adds the static slots, the file headers and the prose (a mechanical n/a is no reading)",
|
||||
Set(Plan::NotReviewed(units, lines, statics)) == plusBehaviour && Set(Plan::NotReviewed(units, lines, onlyFn)) == plusStatic, Show(Set(Plan::NotReviewed(units, lines, onlyFn))));
|
||||
std::set<std::string> codeIds;
|
||||
for (const std::string& id : ids) {
|
||||
|
|
@ -166,6 +174,36 @@ int main() {
|
|||
Check("repo-security: the bug-prover's shape - no whole pass, the same code units, static blocks keyed on the code, three reads, none by default, not empirical",
|
||||
sec.whole.is_null() && unitsOf(sec.blocks) == codeIds && sameShape && s.gate == 3
|
||||
&& std::ranges::all_of(sec.blocks, [](const Json& j) { return j.at("maxTurns") == 60 && j.at("timeoutMin") == 40 && j.at("model") == Plan::ModelFor("opus"); }));
|
||||
// The commit-truth lens (2026-10-31): the prose of the range and its two
|
||||
// whole slots, in passes of their own.
|
||||
const Plan::LensPlan truth = Plan::PlanLens(Facts, units, lines);
|
||||
std::map<std::string, std::string> truthKinds;
|
||||
for (const Json& j : truth.blocks) truthKinds[j.at("unit").get<std::string>()] = j.at("kind").get<std::string>();
|
||||
const std::map<std::string, std::string> wantTruth = {{"p1:subject", "block"}, {"p1:diffstat", "block"}, {"p2:subject", "block"}, {"p2:msg", "block"}, {"p2:diffstat", "block"},
|
||||
{"p2:README.md#hdr", "auto-na"}, {"p2:README.md#1", "block"}, {"whole:order", "slot"}, {"whole:absent", "slot"}};
|
||||
const Json& truthMsg = Job(truth.blocks, "block", "p2:msg");
|
||||
const Json& truthDoc = Job(truth.blocks, "block", "p2:README.md#1");
|
||||
const Json& truthOrder = Job(truth.blocks, "slot", "whole:order");
|
||||
const Plan::Lens& t = Plan::LensOf(Facts);
|
||||
Check("repo-facts: no whole pass; the text units, the documentation units and its two whole slots (whole:behaviour is the functional lens's); a doc file header is a mechanical n/a with its own basis; "
|
||||
"text and doc blocks 60/40, a slot 50/35, one read, opus, Gate 4, none by default",
|
||||
truth.whole.is_null() && truthKinds == wantTruth && Job(truth.blocks, "auto-na", "p2:README.md#hdr").at("basis") == "mechanical: diff header of a documentation file"
|
||||
&& truthMsg.at("unitKind") == "text" && truthMsg.at("maxTurns") == 60 && truthMsg.at("timeoutMin") == 40 && truthDoc.at("unitKind") == "doc" && truthDoc.at("maxTurns") == 60
|
||||
&& truthOrder.at("unitKind") == "slot" && truthOrder.at("maxTurns") == 50 && truthOrder.at("timeoutMin") == 35 && truthOrder.at("label") == "repo-facts:slot:whole:order"
|
||||
&& truthOrder.at("expectedIds") == Json::array({"whole:order"}) && !t.reads && t.gate == 4 && t.model == "opus" && t.env == "none" && !t.empirical && t.whole.empty()
|
||||
&& std::ranges::all_of(truth.blocks, [](const Json& j) { return j.at("kind") == "auto-na" || j.at("model") == Plan::ModelFor("opus"); }),
|
||||
Dyn::ReprValue(Json(truthKinds)));
|
||||
const Plan::Budget textElsewhere = Plan::BudgetFor("block", "text", "repo-bug-prover.md");
|
||||
const Plan::Budget docBudget = Plan::BudgetFor("block", "doc", Facts);
|
||||
Check("budgets: a text block of another lens 50/30, a doc block 60/40, a slot 50/35; an unknown unit kind is still a KeyError", textElsewhere.maxTurns == 50 && textElsewhere.timeoutMin == 30
|
||||
&& docBudget.maxTurns == 60 && docBudget.timeoutMin == 40 && Plan::BudgetFor("slot", "slot", Facts).maxTurns == 50 && [] {
|
||||
try {
|
||||
Plan::BudgetFor("block", "nope", "repo-bug-prover.md");
|
||||
return false;
|
||||
} catch (const Dyn::Error&) {
|
||||
return true;
|
||||
}
|
||||
}());
|
||||
const std::vector<std::string> exclude = {"**/*.test.*", "docs/**"};
|
||||
const Plan::LensPlan functional = Plan::PlanLens(Fn, units, lines, {}, exclude);
|
||||
std::map<std::string, std::string> kinds;
|
||||
|
|
@ -223,9 +261,22 @@ int main() {
|
|||
const std::string tailFunctional = Prompt::Tail(functional.whole, units, lines);
|
||||
Check("whole tails: the approach text lists order+absent; the functional text lists behaviour and names the APPLICATION UNDER TEST", tailApproach.contains("for THIS repository")
|
||||
&& tailApproach.contains("whole:order") && tailFunctional.contains("as a USER") && tailFunctional.contains("whole:behaviour") && !tailFunctional.contains("whole:order"));
|
||||
const std::string hunkTail = Prompt::Tail(Job(prover.blocks, "block", "p2:hello.py#1"), units, lines);
|
||||
Check("block tails: the functional hint on a functional block, none on a static hunk, the repo hints on the slots",
|
||||
Prompt::Tail(functionalBlock, units, lines).contains("judges ONE hunk in the running application") && !Prompt::Tail(Job(prover.blocks, "block", "p2:hello.py#1"), units, lines).contains("judges ONE hunk")
|
||||
Prompt::Tail(functionalBlock, units, lines).contains("judges ONE hunk in the running application") && !hunkTail.contains("judges ONE hunk")
|
||||
&& Prompt::Tail(Job(prover.blocks, "block", "p1:absent"), units, lines).contains("body-less commit") && Prompt::Tail(Job(prover.blocks, "block", "p1:outside"), units, lines).contains("users and callers"));
|
||||
const std::string msgTail = Prompt::Tail(truthMsg, units, lines);
|
||||
const std::string docTail = Prompt::Tail(truthDoc, units, lines);
|
||||
const std::string orderTail = Prompt::Tail(truthOrder, units, lines);
|
||||
const std::string absentTail = Prompt::Tail(Job(truth.blocks, "slot", "whole:absent"), units, lines);
|
||||
Check("repo-facts tails: a message block judges a claim at its source with the text hint, a doc block with the documentation hint, each slot pass the slot's question with this lens's duty; "
|
||||
"a code block's tail stays a hunk against the standard, and a slot of another lens would carry no duty",
|
||||
msgTail.contains("a claim at its source, a sentence against its proof obligation") && msgTail.contains("verify every claim against this commit's diff") && !msgTail.contains("a hunk against the standard")
|
||||
&& docTail.contains("a claim at its source") && docTail.contains("This unit is documentation the commit adds or changes") && docTail.contains("UNIT TEXT (verbatim")
|
||||
&& orderTail.starts_with("SCOPE - SLOT PASS, unit \"whole:order\"") && orderTail.contains("Answer it for your lens; for this lens that means each message describes its own commit alone")
|
||||
&& absentTail.contains("documentation the range leaves stale") && absentTail.ends_with(Prompt::GenericVocab)
|
||||
&& hunkTail.contains("a hunk against the standard") && !hunkTail.contains("a claim at its source") && Prompt::SlotDuty("repo-bug-prover.md", "whole:order").empty()
|
||||
&& Prompt::SlotDuty(Facts, "whole:behaviour").empty());
|
||||
const std::string ll = Prompt::LensLayer(Fn, "CHARTER TEXT", "DISPOSITIONS BLOCK", ab, "SUMMARY");
|
||||
const std::string sp = Prompt::SystemPrompt(st, rl, ll);
|
||||
const std::string up = Prompt::UserPrompt(tailFunctional, {{"maxTurns", 220}});
|
||||
|
|
|
|||
Loading…
Reference in a new issue