diff options
Diffstat (limited to 'docs/content-addressed-phase0.md')
| -rw-r--r-- | docs/content-addressed-phase0.md | 220 |
1 files changed, 0 insertions, 220 deletions
diff --git a/docs/content-addressed-phase0.md b/docs/content-addressed-phase0.md deleted file mode 100644 index 7271674..0000000 --- a/docs/content-addressed-phase0.md +++ /dev/null @@ -1,220 +0,0 @@ -# Content-addressed migration inventory - -This file records the implementation inventory frozen at Phase 0. The -normative contracts remain `design.md`, `syntax.md`, `prelude.md`, -`execution.md`, and `store.md` in the Felix design workspace. - -## Revisions and workload - -- Implementation anchor: - `77d892c3a9213acc1be23ef545f316acb87b8c9a` (`Clean lib`). -- Historical uncached reference: - `108b963ebe395ec7c75234e5069c31732531fc97`. -- Active root: `(MigrationLibrary, everything.tex)`. -- The historical and anchor source closures contain the same 31 modules in - imported-before-importer order: - -```text -set.tex -set/cons.tex -set/symdiff.tex -set/product.tex -set/powerset.tex -set/bipartition.tex -set/partition.tex -relation.tex -relation/uniqueness.tex -function.tex -set/cantor.tex -set/filter.tex -set/fixpoint.tex -relation/properties.tex -order/quasiorder.tex -relation/equivalence.tex -relation/closure.tex -set/regularity.tex -set/suc.tex -ordinal.tex -nat.tex -cardinal.tex -algebra/magma.tex -algebra/semigroup.tex -algebra/monoid.tex -order/order.tex -topology/topological-space.tex -topology/basis.tex -topology/disconnection.tex -topology/separation.tex -everything.tex -``` - -The active source contains 74 abbreviations, 17 axioms, 14 corollaries, -92 definitions, 19 lemmas, 552 propositions, four signatures, nine structures, -and four theorems. It contains no active datatype or inductive declaration. -There are 366 top-level proof environments. These are migration coverage -counts, not semantic identity inputs. - -## Source and path conventions - -`ResolvedSource` carries four separate values: selected canonical file, -invocation-local mount ID, canonical mount root, and validated mount-relative -path. Durable ownership will use only the canonical root and relative path. -The mount ID remains routing and presentation data. - -The absolute and relative path codecs, `SourceNamespaceId`, `ModuleName`, -zero-based `LocalDeclarationOrdinal`, zero-based `GeneratedObjectSlot`, and -the closed declaration-family tags are frozen in `design.md`. Golden path -inputs are `/`, `/a`, `/a/b`, `a`, and `a/b`. No identity is computed in -Phase 0. - -The transitional `Felix.Migration` manifest contains only closed mount roles -and safe relative paths. It must be deleted with the legacy driver. - -## Prelude reservation - -- Reserved source: Cabal/Hpack data file `data/felix-prelude.tex`. -- Reserved logical owner: `PreludeModuleName` from `prelude.md`. -- Diagnostic label: `<felix-prelude>`. -- Bootstrap bytes: the empty byte string. -- Loading seam: generated `Paths_felix.getDataFileName`. - -The checked-in file is a non-authoritative, comment-only skeleton. It exposes -the required definition, abbreviation, proposition, and proof families and the -Empty-to-Omega dependency shape without acting as a builtin, checked module, or -authority source. - -The machine-readable expected public roles are Infinity, the transparent -Omega object and defining equation, the `naturals` alias, and the inductiveness -and minimality theorems. Helper declaration names are not frozen. - -## Literal base syntax and dynamic insertion - -`Syntax.Lexicon.builtinMixfixLevels` is the exact ten-row manifest: - -| Level | Associativity | Entries | -| --- | --- | --- | -| 0 | — | empty | -| 1 | left | `+`, `\union`, `-`, `\rminus`, `\monus` | -| 2 | left | `\relcomp` | -| 3 | left | `\circ` | -| 4 | left | `\mul`, `\inter`, `\rmul` | -| 5 | left | `\setminus` | -| 6 | right | `\times` | -| 7 | — | empty | -| 8 | non-associative | `\rfrac`, `\exp`, `\unions`, `\cumul`, `\fst`, `\snd`, `\pow`, `\neg`, `\inv`, `\abs`, `\cons`, ordered pair | -| 9 | non-associative | `\emptyset`, `\naturals`, `\naturalsPlus`, `\integers`, `\rationals`, `\reals`, `\unit`, `\zero` | - -Current dynamic syntax enters through `Syntax.Adapt.scanSyntaxDelta`, -closure-wide `buildSyntaxWorld`, and `insertScannedItem`. Every scanned -function/mixfix pattern is currently appended to row 9 as non-associative. -`Felix.Parse.parseResolvedSourceGraphMeasuredWith` builds one closure-wide -world before parsing. Phase 1.1 replaces these insertion and composition -points with complete per-module entries and independent interfaces. - -## Legacy publisher and consumer inventory - -`Checking.Legacy.LegacyFactProducer` is the closed current publisher -inventory: - -- declared assumptions, distinguished by `AssumptionKind`; -- direct proof obligations discharged by Vampire or a gap; and -- declaration rules for ordinary theorem finalization, definition equations, - datatype introduction/distinctness/injectivity/cases/induction, structure - introduction/inheritance/assumptions, and inductive - introduction/domain-subset/cases/induction. - -`Checking.checkBlocks` selects the producer at each declaration boundary. -`finalizeLegacyDeclaration` reserves and appends the complete fact batch. -`Checking.Legacy` assigns invocation-local module/fact positions, merges -imported environments and fact registries, and seals modules. The legacy facts -feed proof lookup, premise selection, TPTP task construction, trust reporting, -HTML/checker presentation, and the temporary `Checking.Transition` bridge. -The transition bridge separately publishes the currently typed signatures, -inductive objects/facts, exact typed Vampire results, and kernel facts. - -No publisher outside those inventories may be silently carried into the typed -driver. - -## Checker and builder mutation coverage - -The following state affects later checking and therefore requires an explicit -closed semantic-environment delta or deterministic reconstruction: - -| Current state | Phase-1 classification | -| --- | --- | -| fact statements, aliases, origins, public authority | explicit fact occurrences and aliases; registry indexes derived | -| abbreviations | explicit | -| predicate definitions | explicit | -| symbol dependencies | explicit | -| symbol ownership and object markers | explicit ownership rows; marker set derived where exact | -| frozen symbols | explicit | -| structure graph | explicit structure-family delta | -| defined declaration markers | explicit occurrence/alias collision data | -| typed global bindings and transparent bodies | explicit canonical object records and bindings | -| local typed fact entries and direct axiom kind | explicit canonical facts and authority | -| imported environment/interface lists | explicit ordered direct interface IDs | -| next declaration/fact counters | derived from ordered committed rows | -| fact/global lookup maps | derived from canonical ordered rows | - -The following state is session-local and must not be serialized as semantic -state: local assumptions and goals, direct/indirect proof mode, structure -context, local variables, current block labels and locations, hypothesis and -obligation counters, task preparation callbacks, resolved obligation batches, -current producer list, current declaration handle, mutable legacy/transition -builder handles, source locations, routes, diagnostics, and logging or timing -observations. - -The fixed checked foundation is an explicit module-build input. It is not a -declaration delta. A new declaration family must close this inventory with an -explicit case or a deterministic derivation before migration; no catch-all -checker-state payload is permitted. - -## Operational seam inventory - -- CLI dispatch and options: `CommandLine.run` and `Api.Options`. -- Source graph and parser callbacks: `Felix.Source.Graph`, - `Felix.Parse.parseSourceWorkspaceWith`. -- Cumulative glossing state: `Api.verifyWorkspace`, - `Meaning.GlossState`, and `Meaning.glossStep`. -- Declaration dispatch/finalization: `Checking.checkBlocks`, - `withBlockContext`, and `finalizeLegacyDeclaration`. -- Typed authority/builders: `Checking.Transition` and - `Checking.Typed.*`. -- Task preparation and filter/reconstruction: `Checking.tellTasks`, - `Filter`, `Checking.Backend.*`, `Encoding`, and `Provers`. -- Prover supervision: `Provers.runProver`. -- Separate request dumping: `CommandLine.run`, `Api.prepareDumpTasks`, and - `Api.dumpTask`. -- HTML preparation/routing/publication: `Render.Html.Export`, - `Render.Html.Layout`, and `Render.Html.Output`. - -Dump and HTML paths remain separate today. The target dump boundary is frozen -in `execution.md`: an absent or empty destination is preflighted, then Felix -owns the complete run directory. - -## Measurement protocol - -The frozen historical command is: - -```text -NAPROCHE_LIB=<108b963 worktree>/library \ -stack exec zf -- --log library/everything.tex -t 17 --uncached +RTS -s -RTS -``` - -Record the exact revision, worktree, source closure, result, task count, -accumulated logged Vampire time, wall/user/system time, allocation, peak -residency/RSS, capabilities, compiler/package plan, Vampire revision, OS, -processor, memory, limits, and RTS flags in `changes.md`. - -Later comparison scenarios are: - -1. fresh-store cold verification of the same active root; -2. warm verification without source changes; -3. a proof-only leaf edit; -4. a transparent definition edit; -5. a leaf-module edit; and -6. an edit to a central syntax or semantic interface. - -Each scenario records semantic outcomes and authority first, then wall/CPU -time, peak RSS, Vampire time, cache-hit counts, and effective parallelism. -Phase 0 exposes no store or jobs option. |