REFERENCE / ZLIB × LEAN
Memory, translation and external-I/O semantics
Source snapshot ·
00a7fbc60cc0c90b · Source at the matching commit ↗The project proves statements about an executable Lean translation of C. This section explains what that translation represents, how specifications describe it, and where the connection to C still depends on review. It is not a progress report; progress holds that record.
Start with architecture. Then use the page that answers your question:
| Question | Read |
|---|---|
| How do C, the runtime, specifications and proofs fit together? | Architecture |
| How must a C statement be translated? | Translation rules |
| What do the heap-free API relations describe? | API model and concrete boundary |
| Where are internal helper preconditions specified? | Internal-call specifications |
| What file, formatting and error behaviors does the external world represent? | External I/O |
| Which records and pointer kinds exist? | Generated runtime schema |
The API manual describes public calls. The proof guide explains how to establish their properties. The checking guide explains how a result is accepted. Read safety, trusted base and representation limits when assessing the scope of any theorem.