Wikifunctions compositions, checked by F*

What works now

• An F* evaluator with lists, pairs, function references, and the LISP core: cons, car, cdr, null?, if, map, filter, fold.
• A ZObject model, identifier parsing, and canonical-form normalisation, all as checked F* definitions rather than assumptions.
• A generator that translates pinned Z14K2 compositions into F*, recording revision and digest for each.
• A fixpoint closure analysis over the whole corpus in under a second.
• Every generated body also printed as an s-expression by a checked F* module, and rendered back to canonical Wikifunctions composition data.
• Any function exportable as a self-contained Scheme program that runs in an off-the-shelf Scheme.
• A vendored 20260801 dump, local SQLite composition graph index, and digest-pinned object cache.

What it is not

• It is not a proof that arbitrary Python or JavaScript `Z16` implementations are correct.
• Completing evaluator coverage is the current priority; unsupported ZObject forms and foreign-code boundaries are still reported explicitly.
• The primitives are authored F*, not derived from Wikifunctions. They are a claim about what Wikifunctions means, checked against its own testers rather than proved.
• There is no object store, so references in argument position are refused rather than resolved.
• Records, errors, and monolingual text are not yet values.
• Deep recursion exhausts fuel rather than returning an answer.
• It is not yet a Low*/KaRaMeL C extraction target.
• The deliberately named junk JavaScript composition evaluator is a pre-F* prototype, not extracted F* code.
• Closure claims are relative to the fetched corpus and the selected primitive policy.

Runnable demos

The homepage does not run the extracted JavaScript or tree browser. Use the separate demo pages for interactive browser artifacts and composition graph browsing.

• Engine browser: search, read, and run the whole engine
• How the engine works, and what is generated versus authored
• Focused demo: Z22294 through extracted F*
• Demos menu
• Extraction notes and CLI commands
• All compositions as one loadable Scheme file, prelude included
• The same definitions without the prelude
• All rendered back as canonical Wikifunctions data
• Function catalogue with provenance

Next grounding frontier

These numbers were wrong and are now measured. This table used to say what each primitive “blocks”, taken from the closure analysis’s ranking. That ranking counts a function once for every leaf blocking it, and those sets overlap almost entirely — so four different primitives each appeared to block about 1,400 of the same functions. The honest question is what grounding one actually unlocks, measured by adding it and re-running make closure. That number is thirty times smaller and it reorders the list.

The last row is the point. Z10249 looked like the seventh most important thing to do and grounding it would change nothing at all, because everything it gates is gated by something else as well.

Done since this list was last written: errors as values (Z5, Z851, Z850, Z853), case conversion, Z803 value by key, Z16829 type of object, Z13052 and Z29294 object equality and equivalence, the codepoint conversions, reverse and append, and natural division.

Local setup

git clone https://github.com/danbri/wikifn-fstar.git
cd wikifn-fstar
make setup-fstar
make doctor

Demos, setup notes, debugging notes, cache notes, primitive notes, and extraction notes are included in the repo.