Documentation

Start with the illustrated reading path. The website offers English and 简体中文 through the header language menu, including diagram labels.

Use these sections for detail:

• Specifications: platform scope, safety, input ranges, public API contracts, internal helper contracts and compressed-byte meaning.
• Model: translation and memory semantics, abstract relations and external I/O.
• Implementation arguments: the common method and detailed reasoning for each C component, reached from the illustrated chapters.
• Checking: acceptance rules, with earlier review records grouped separately from the reading path and current status.
• Progress: the all-target dependency graph, exact proof evidence, blockers and remaining work.

Trusted base and deviations state assumptions and model limits. Findings records source reports with their scope. Runtime schema is a field reference. Earlier arguments is a reference appendix, not a second specification or status report.