CENTL contributor onboarding — Free Computation Foundation

Manual

This is the complete manual learning path for understanding, building, testing, and changing CENTL. It assumes no prior F or OCaml experience. AI tools are optional: every source of truth, command, and readiness exercise needed to work…

Source in the repository

This is the complete manual learning path for understanding, building, testing, and changing CENTL. It assumes no prior F* or OCaml experience. AI tools are optional: every source of truth, command, and readiness exercise needed to work on the project is listed here.

The repository is the authority when this guide and an external tutorial disagree. In particular, use the exact versions in toolchain.lock, not the newest versions from a tutorial.

What fully onboarded means

A contributor is ready to work independently when they can:

build CENTL from a clean checkout and run the appropriate test suites;
explain why 0.1 is exact and why an approximation is displayed as an enclosure rather than an unjustified point value;
trace an expression from the parser, through exact evaluation, to terminal or structured JSON output;
decide whether a change belongs in F*, handwritten OCaml, the C/Arb bridge, the Julia laboratory, or documentation;
change and re-extract the verified F* core without editing generated OCaml;
add unit, CLI, adversarial, metamorphic, and differential coverage in the right places;
preserve CENTL's numerical and verification contracts during review.

You do not have to learn the entire stack before making a documentation or small OCaml contribution. Follow the stages in order, and stop at the readiness gate appropriate to the part of the repository you plan to change.

The system in one picture

calculator / script / JSON Lines / MCP
                    |
                    v
       handwritten OCaml application
 parser, sessions, limits, protocols,
 rendering, precision orchestration, CLI
                    |
                    v
          extracted F* semantic core
 exact values, algebra, calculus, boundary
 validation, proof-backed algorithms
                    |
                    v
          narrow OCaml -> C boundary
              FLINT / Arb / GMP / MPFR

Independent oracle: Julia + Nemo differential tests

The implemented product is currently an exact-first calculator and numerical language. DESIGN_PATH.md describes the longer-term direction toward checking mathematical claims; treat it as product direction, not a claim that every described capability already exists.

Stage 0: orient yourself

Read these project documents in order before changing behavior:

README.md — product promise and user-facing examples.
DESIGN_PATH.md — intended product direction.
DESIGN.md — implemented architecture, ownership, and trust boundary.
NUMERICS.md — exactness, approximation, precision, and resource contracts.
VERIFICATION.md — what is proved, assumed, extracted, and tested.
SYNTAX.md — complete public language surface.
PROTOCOL.md and MCP.md — machine-facing interfaces.
ROADMAP.md — current scope and sequencing.

For feature-level work, also use MATHEMATICS.md, ALGEBRA.md, CALCULUS.md, and ITERATION.md as the implemented mathematical reference sheets.

If a release or local build is already available, run a few expressions from the README and inspect their output. Otherwise, return to these after Stage 1:

./centl '0.1 + 0.2'
./centl '1 / 3'
./centl 'approx(sin(pi / 6), 20)'
./centl 'solve(x^2 - 5*x + 6 = 0, x)'
./centl 'sequence(k^2, k = 1, 5)'

Readiness gate: explain the difference among an exact rational, an exact symbolic value, a real enclosure, a solution set, and an indeterminate result.

Stage 1: install and prove the baseline

Follow CONTRIBUTING.md for operating-system packages and the checksum-verified F* install. The reproducible development sequence is:

scripts/bootstrap-opam
eval "$(opam env --switch=centl)"
make test
make quality

make test verifies and extracts F*, builds the native application, and runs the normal Dune test suite. make quality checks formatting, warnings, the opam manifest, and agreement among pinned versions. Neither quality target rewrites source files.

Install the independent mathematical oracle once:

julia --startup-file=no --project=lab/julia \
  -e 'using Pkg; Pkg.instantiate()'
make differential-test

Run the full defensive suite before high-risk numerical, parser, native, or protocol work:

make hardening-test

Useful references:

Readiness gate: a clean make test and make quality, followed by a successful evaluation through the locally built ./centl launcher.

Stage 2: learn the OCaml used by CENTL

OCaml is the host language. It owns parsing, sessions, iteration orchestration, resource limits, the CLI, history, JSON Lines, MCP, and the bridge to extracted semantics and native numerics.

Required OCaml concepts

Learn these in this order:

expressions, immutable let bindings, functions, recursion, and pipelines;
tuples, records, variants, pattern matching, lists, arrays, and option;
modules, signatures (.mli), namespaces, and compilation units;
labelled and optional arguments;
exceptions, result, mutable references, hash tables, and queues;
bytes versus strings and UTF-8 boundary awareness;
higher-order functions and tail recursion;
foreign function declarations for the C boundary.

Use the free official material:

OCaml learning hub
Tour of OCaml
OCaml 4.14 reference manual
Labelled and optional arguments
Interfacing C with OCaml
Zarith 1.14 API for exact integers and rationals
Yojson 2.2.2 API for JSON

Read CENTL's OCaml in this order

centl_syntax.ml — small catalogue of public syntax, examples, and completion names.
centl_request_queue.mli and centl_request_queue.ml — compact interface/implementation example with bounded state.
centl_history.ml — persistence, validation, locking, and bounded storage.
centl_parser.ml — tokens, source spans, precedence, statements, and located errors.
centl_iteration.ml — finite iteration, recurrences, budgets, and stack-aware execution.
centl_protocol.ml — a small structured interface around the engine.
centl_engine.ml — the main bridge; read one feature vertically rather than attempting the whole file at once.
main.ml — CLI flags, input modes, REPL behavior, and top-level error handling.

Readiness exercise: add a harmless completion or syntax example, add/update its test, run the focused test and make quality, and explain every line of the diff. Revert the exercise if it is not a real product improvement.

Stage 3: understand Dune and the test ecosystem

CENTL uses Dune to compile OCaml, link foreign stubs, format source, and run several kinds of tests.

Required references:

Study src/dune, src/native/dune, and tests/dune. Then map the suites:

test_centl.ml covers the general semantic surface.
test_iteration.ml and test_sequence.ml cover bounded iteration.
test_adversarial.ml attacks resource and numerical boundaries.
test_history.ml and test_request_queue.ml cover stateful host infrastructure.
cli.t and installer.t are end-to-end Cram transcripts.
tests/corpus/ contains deterministic malformed and edge inputs.
tests/hardening/ contains fuzz-corpus, metamorphic, sanitizer, and performance checks.

Focused loops after the baseline has passed include:

dune exec tests/test_sequence.exe
dune runtest tests/cli.t
make adversarial-test
make fuzz-test
make metamorphic-test
make performance-test

Use make format-fix only when you intend to rewrite formatting, and inspect its diff afterward.

Readiness exercise: find one public behavior in tests/cli.t, identify the unit test beneath it, and describe what the Cram test catches that the unit test does not.

Stage 4: learn F* and the verified core

F is a proof-oriented functional language. CENTL uses it for the semantic model and mathematical operations whose invariants should be explicit and machine checked. F asks Z3 to discharge verification conditions, then extracts executable OCaml.

No previous proof-assistant experience is required. Follow the official free Proof-Oriented Programming in F* in this order:

When a proof fails, use the official Z3 material to understand the solver rather than treating solver settings as magic:

Read CENTL's F* in this order

Centl.Gcd.fst — the smallest complete local example of definitions, specifications, verification, and extraction.
The type and value definitions near the beginning of Centl.Core.fst.
Rational normalization and arithmetic.
Dyadic bounds and outward-rounded enclosure construction.
symbolic expression substitution and variable handling;
algebra, differentiation, integration, solving, validation, and rendering.

Use tests and documentation to choose a vertical slice before reading the large core file. For example, trace rational addition or differentiation from a test, into OCaml engine dispatch, into the F* definition, then back through the renderer.

The only safe F* edit loop

make verify
make extract
git diff -- src/generated
make native-test
make quality

Never hand-edit src/generated/. Those files are a checked-in build artifact produced from F. An F change includes the reviewed generated diff. CI re-extracts with the pinned verifier and rejects a stale snapshot.

The adapters in src/runtime/ map the F* extraction runtime to OCaml and Zarith. They are part of the executable trust path and should stay small.

Readiness exercise: state a simple invariant in Centl.Gcd.fst, verify it, inspect its extracted OCaml, and explain which fact was proved versus merely tested. Do not keep a tutorial-only change.

Stage 5: learn exact and rigorous numerics

CENTL's core promise is not just “many digits.” It distinguishes exact values from certified enclosures, rounds bounds outward, and refuses to print digits that are not justified.

Learn these concepts:

arbitrary-precision integers and normalized rational numbers;
exact symbolic values versus numeric approximations;
interval/ball arithmetic and outward rounding;
absolute versus relative precision and cancellation;
real versus complex enclosures;
indeterminate values and explicit resource exhaustion;
why converting an enclosure to a floating-point midpoint can destroy the public contract.

Authoritative references:

Trace one native call through all three layers:

its declaration in centl_arb.ml;
its OCaml use in centl_engine.ml;
its implementation and allocation/error cleanup in centl_arb_stubs.c.

The OCaml C interface manual is required reading before editing the stubs. Pay particular attention to GC roots, ownership, blocking sections, exception boundaries, and allocation failure paths.

If C is new, first complete the relevant parts of the free GNU C Language Introduction and Reference Manual. Use the SEI CERT C Coding Standard as the defensive reference for native-boundary work.

Readiness exercise: trace approx(sin(pi / 6), 20) and explain where precision is requested, where outward bounds are established, how failure is classified, and why the displayed endpoints are safe.

Stage 6: understand parsing, scope, and resource limits

The handwritten parser is inside the trusted application boundary. A parser bug can change the meaning of user mathematics before verified semantics sees it, so parser work requires semantic and adversarial tests.

Read in this order:

the grammar and precedence contract in SYNTAX.md;
tokens, source locations, and precedence in centl_parser.ml;
immutable definitions, functions, lookup, substitution, and rendering in centl_engine.ml;
finite iteration budgets in centl_iteration.ml;
parser and multiline cases in tests/ and tests/corpus/.

For every new syntax form, test at least precedence, whitespace, multiline input, source locations, malformed input, nesting, budget limits, terminal output, and structured output. Avoid unbounded recursion on user-controlled input.

Readiness exercise: trace a multiline function definition and one malformed variant from bytes to token, AST/statement, engine evaluation, and caret error.

Stage 7: understand machine protocols and MCP

CENTL's human and machine interfaces must expose the same typed mathematical result. JSON must not silently collapse exact values or enclosures into ordinary floating-point numbers.

Start with PROTOCOL.md, centl_protocol.ml, MCP.md, and centl_mcp.ml. Then read the request queue because long-running MCP work depends on bounded scheduling and cancellation: centl_request_queue.mli.

Protocol references:

Manual JSON Lines smoke test:

printf '%s\n' '{"version":1,"expression":"0.1 + 0.2"}' | ./centl --serve

Readiness exercise: explain how invalid JSON, an invalid expression, a limit failure, cancellation, and a valid exact result differ on the wire. Confirm each case is bounded and machine distinguishable.

Stage 8: understand the independent Julia/Nemo oracle

The Julia laboratory is intentionally independent of CENTL's F*/OCaml implementation. It catches shared-assumption bugs that ordinary example tests may miss. It is required before merging changes to mathematical behavior.

Learn only the Julia needed for the laboratory:

Then read lab/julia/README.md, Project.toml, and differential.jl. The checked-in manifest pins the oracle environment. Random cases are seeded and must remain reproducible.

Readiness exercise: add a temporary deterministic oracle case, observe both sides' structured values, force a harmless mismatch, and understand the failure report. Remove the forced mismatch afterward.

Stage 9: hardening, packaging, and release work

Read PERFORMANCE.md, INSTALL.md, TOOLCHAIN.md, the root Makefile, and scripts/ before changing build or release behavior.

The defensive suites have different jobs:

adversarial tests target known dangerous boundaries;
the deterministic fuzz corpus mutates parsers and protocols;
metamorphic tests check relationships that should remain true across inputs;
native sanitizers look for C memory and undefined-behavior failures;
performance smoke tests protect explicit resource envelopes;
differential tests compare mathematical results with an independent system.

Release artifacts use exact native dependency pins, while ordinary local development may use compatible distribution packages. Do not change a version in only one file: update the canonical lock and all intentionally mirrored locations, then run scripts/check-toolchain-pins through make quality.

FCF-owned CENTL software is licensed under Apache-2.0, while project documentation and branding follow the path-specific terms in LICENSING.md and .reuse/dep5. Preserve SPDX, copyright, NOTICE, and valid third-party notices. Contributions must also carry the DCO sign-off described in CONTRIBUTING.md.

Readiness gate: explain what each CI/release job protects and successfully run the local suite appropriate to the proposed packaging or dependency change.

Repository map

Path	Responsibility	Change risk
`src/fstar/`	Verified semantic model and mathematical operations	High: proof and semantic contract
`src/generated/`	Checked-in F* extraction output	Generated; never edit manually
`src/runtime/`	F* extraction runtime adapters	High: execution/trust boundary
`src/ocaml/`	Parser, engine bridge, sessions, limits, protocols, CLI	Medium to high by feature
`src/native/`	OCaml/C/Arb foreign interface	High: memory and numeric safety
`tests/`	Unit, Cram, adversarial, corpus, hardening tests	Required evidence
`lab/julia/`	Independent Nemo oracle	Keep independent and deterministic
`docs/`	Product, syntax, numerical, protocol, and verification contracts	User-visible contract
`scripts/`	Bootstrap, pin checks, sanitizers, packaging	High: developer/release integrity
`.github/workflows/`	CI and release enforcement	High: repository-wide safety net

Route a change before writing it

Change	Primary location	Minimum validation
Documentation only	`README.md`, `docs/`	`make quality` where toolchain is available; review links/examples
CLI, REPL, history, queue	`src/ocaml/`, focused tests	`make native-test`, `make quality`
Parser or syntax	parser, syntax catalogue, docs, unit/Cram/corpus tests	`make native-test`, `make fuzz-test`, `make quality`
Exact semantic or algebraic behavior	`src/fstar/`, generated snapshot, tests	`make test`, `make differential-test`, `make quality`
Approximation/native numerics	F* plus `src/native/` as needed	`make test`, `make hardening-test`, `make differential-test`, `make quality`
JSON Lines or MCP	protocol/MCP/queue, docs, corpus tests	`make native-test`, `make fuzz-test`, `make adversarial-test`, `make quality`
Dependency or toolchain pin	`toolchain.lock` and intentional mirrors	clean bootstrap/build, `make test`, `make quality`
Packaging/release	scripts, installer tests, workflows, release docs	installer/package smoke tests plus complete build

“Minimum” is not a ceiling. Run the broader suite whenever a change crosses layers or could affect mathematical correctness, trust boundaries, memory safety, untrusted input, or resource use.

A reliable vertical-slice workflow

For any behavior change:

Write down the user-visible input, typed result, rendering, error behavior, and resource limit before editing.
Locate an existing neighboring test and trace it through the system.
Choose the owning layer using the routing table above.
Add the smallest failing test at the lowest useful layer.
Implement the change without weakening the numerical or verification contract.
If F* changed, verify, extract, and review generated output.
Add an end-to-end test for user-visible behavior and a structured-protocol test where applicable.
Add adversarial, metamorphic, sanitizer, performance, or differential evidence when the risk calls for it.
Update every affected contract document and syntax example.
Run focused checks, then the required full targets from the routing table.
Review git diff for generated noise, accidental formatting, secrets, temporary fixtures, and unrelated user changes.

Common failures and where to look

Symptom	First checks
`dune` or an OCaml package is missing	Run `eval "$(opam env --switch=centl)"`; inspect `opam switch` and `centl.opam`
F* cannot find the expected Z3	Recheck the pinned F* install in `CONTRIBUTING.md`; use `fstar.exe --locate_z3 4.13.3`
Generated files changed unexpectedly	Confirm the pinned F* version, run `make extract` once, and inspect only `src/generated/`
Native link/load error for FLINT/GMP/MPFR	Check `pkg-config`, installed development/runtime libraries, `src/native/dune`, and platform loader paths
F* proof times out	Reduce to the failing definition, inspect the verification condition, relevant refinements, quantifiers, and solver limits; do not simply raise limits first
Correct-looking numeric point disagrees with the contract	Check whether the value should be exact or an outward enclosure; never discard the radius/bounds
Cram output changed	Decide whether behavior or only presentation changed; inspect terminal color, source locations, ordering, and protocol stability
Fuzz/metamorphic failure	Preserve the input and seed, minimize the case, then add it to the deterministic corpus or focused unit tests
Differential disagreement	Compare typed exact structures before text rendering; check whether CENTL or the oracle is outside its supported domain
Slow or nonterminating input	Identify the explicit budget, recursion depth, queue bound, or native-call limit before optimizing

A low-risk first-contribution ladder

Fix an inaccurate explanation or add a missing tested example in docs/.
Improve a diagnostic or completion in handwritten OCaml with a focused test.
Add a deterministic regression case for an already-understood behavior.
Make a bounded parser, history, queue, or protocol improvement.
Add a proved helper or small semantic change in F* and inspect extraction.
Change rigorous numerical or native behavior only after completing the numerics and FFI readiness exercises.

Non-negotiable review checklist

Decimal input never enters binary floating-point implicitly.
Exact results stay exact; approximation is visible and intentional.
Enclosures remain enclosures and are rounded outward.
No displayed digit claims more precision than has been established.
Human and machine interfaces represent the same typed result.
Invalid or oversized user input is rejected predictably and with bounded resource use.
Parser, protocol, queue, and history state have explicit size/depth limits.
F* assumptions remain reported as errors and generated OCaml is current.
C stubs preserve OCaml GC rules and native allocation ownership on every path.
Tests are deterministic; randomized failures include reproducible seeds.
The Julia oracle remains implementation-independent.
Public behavior changes update syntax, protocol, numerical, or verification documentation as appropriate.
No generated artifact, formatter rewrite, pin update, or unrelated worktree change is included accidentally.

Glossary

Exact value

: A value represented without approximation, such as an arbitrary-precision integer, normalized rational, or supported symbolic expression.

Enclosure

: A certified interval or ball known to contain the mathematical value. Its width records uncertainty.

Outward rounding

: Rounding a lower bound downward and an upper bound upward so the true value remains contained.

Refinement type

: A type restricted by a logical predicate, allowing F* to verify properties of values accepted or returned by a function.

Verification condition

: A logical obligation produced by F* and discharged by its type checker and SMT solver.

Extraction

: Translation of verified F* definitions into executable OCaml. Extraction preserves the program, not a runtime proof checker.

Trusted boundary

: Code or assumptions that verification relies on but does not itself prove, including parsing, runtime adapters, native libraries, and parts of the host application. See VERIFICATION.md for the exact boundary.

Differential test

: A test that evaluates the same mathematical case in CENTL and an independent implementation, then compares structured results.

Metamorphic test

: A test of a relation between multiple executions, such as an identity or an invariance, when a complete expected output is inconvenient.

Final readiness checklist

Before claiming full-stack readiness, complete all of the following:

[ ] Read the project contract documents in Stage 0.
[ ] Bootstrap the pinned OCaml/F*/native toolchain from a clean checkout.
[ ] Pass make test and make quality.
[ ] Complete the OCaml, Dune/testing, and F* readiness exercises.
[ ] Trace one exact and one approximate expression end to end.
[ ] Trace one malformed parser input and one machine-protocol error.
[ ] Explain the verification and native trust boundaries.
[ ] Instantiate and run the Julia/Nemo differential suite.
[ ] Run the hardening suite relevant to the target contribution.
[ ] Make one small reviewed change using the vertical-slice workflow.
[ ] Demonstrate that the change preserves the non-negotiable checklist.

Once these boxes are complete, a contributor can work on CENTL manually without depending on an AI subscription or undocumented project knowledge.