summaryrefslogtreecommitdiff
path: root/source/Checking/Transition.hs
AgeCommit message (Collapse)Author
3 daysRemove obsolete verification machineryadelon
5 daysCorrect exact semantic resolutionadelon
7 daysEstablish canonical identity codecsadelon
9 daysFall back after reconstruction exhaustionadelon
9 daysBound deterministic Horn reconstructionadelon
9 daysMove fact selection into transition inventoryadelon
9 daysBind typed fact admission to module buildersadelon
9 daysMeasure sequential verification workadelon
9 daysAuthorize reconstructed Horn obligationsadelon
9 daysPlan typed tasks from admitted factsadelon
9 daysAuthorize exact typed Vampire requestsadelon
9 daysClassify complete typed prover problemsadelon
9 daysCheck direct inductives through fixed-point replayadelon
9 daysDefine bounded fixed-point kernel rulesadelon
9 daysAuthorize atomic facts through exact typed importsadelon
9 daysReplay scoped HOL derivations independentlyadelon
Replay rechecks stored terms against the current global signature and bounds nodes, lexical depth, and conversion. Import-bearing trees remain replay-only until exact transition-inventory authorization alignment lands.
9 daysAuthorize ground reflexivity through kernel replayadelon
The first typed fact family is deliberately dependency-free. Its rows remain outside the legacy fact registry, so unmigrated declarations cannot consume or reauthorize them.
9 daysAssign nominal identities to predicate signaturesadelon