wikifn-fstar
Z22294: Devanagari digits to Arabic digits
One composition traced end to end, in detail: a selected pinned Wikifunctions composition generated into F*, checked by F*, extracted to OCaml, compiled to JavaScript, and run in the browser. For the whole generated engine, see the engine browser.
What This Shows
Input १२३ becomes 123. The computation is not
handwritten page JavaScript. The page calls JavaScript emitted by
js_of_ocaml from OCaml that was extracted from the checked
F* modules.
| Wikifunctions function | Z22294, Devanagari digits to Arabic digits |
|---|---|
| Selected implementation | Z22295, a Wikifunctions composition |
| Composition dependency | Z14613, replace character set, via recursive composition Z36070 |
| Grounded leaves | Z802, Z10008, Z10075, Z10901, Z14456, and the checked private-use marker helper |
| Claim boundary | Complete for this selected pinned path relative to the current F* primitive kernel; not a general arbitrary-Wikifunctions evaluator. |
Run In Browser
Press the button to run the extracted artifact. Nothing runs before the button press.
Run As A Z7 Call
This uses the current supported canonical-style Wikifunctions call adapter, then lowers the call into the same extracted F* evaluator.
Run In Node
make fstar-call-js
node ./bin/wikifn.js fstar-call --mode generated Z22294 १२३
node ./bin/wikifn.js fstar-call --mode compiled Z22294 १२३
node ./bin/wikifn.js fstar-eval-zobject '{"Z1K1":"Z7","Z7K1":"Z22294","Z22294K1":"१२३"}'What This Is Not
- It is not proof of arbitrary Python or JavaScript
Z16implementations. - It is not yet a full canonical ZObject importer for arbitrary Wikifunctions pages.
- It is not yet Low*/C/Wasm-from-C extraction.