Iface.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Spec.Api.Run
2
3/-!
4# API model: the placeholder interface to the heap
5
6**This file is a placeholder.** The goals about the heap-level library (`Goals.lean`) are
7stated for an *abstract* `HeapApi`: a type of heaps, the relation `Matches` between a heap
8object and a model state, and the translated functions seen as relations from the heap before to
9the outcomes. Nothing here is defined from the runtime: the integration step instantiates
10`HeapApi` with the object heap of `ZlibF/Runtime` and the translations of `ZlibF/Zlib`, and
11`Matches` with the relation generated from the schema (`docs/runtime-schema.md`). Until then no
12goal that mentions `HeapApi` is proved.
13
14What each field must mean is written in `docs/design/api-model.md` (the interface and concrete-boundary sections), not here: the types only fix the shape that the goals use.
15-/
16
17namespace ZlibF.Spec.Api
18
19/-- The result of running a translated function: it faulted (undefined behaviour reached, or a
20missing allocation handled badly: `docs/spec/safety.md`), or it returned the heap after and a value. -/
21inductive Outcome (H α : Type) where
22  | fault : Outcome H α
23  | ret (h : H) (a : α) : Outcome H α
24
25/-- The abstract heap-level API. All `*Run`/`*Init`/... fields are relations: they list *every*
26outcome of the translated function from the given heap (nondeterminism: allocation failure,
27file failure). The arguments that are not heap objects (buffers' contents, flush values) are
28passed in model form; the `*Args` fields say that the heap holds them as `zlib.h` requires:
29`strm->next_in` points to the input bytes, `avail_out` is the room, buffers do not overlap
30each other or the state (`A-stream-*`). -/
31structure HeapApi where
32  Heap : Type
33  Strm : Type
34  GzFile : Type
35  -- Inflate
36  inflMatches : Heap → Strm → InflState → Prop
37  inflArgs : Heap → Strm → InflOp → Prop
38  inflRun : Heap → Strm → InflOp → Outcome Heap InflRes → Prop
39  inflNoState : Heap → Strm → Prop
40  inflInitArgs : Heap → Strm → Prop
41  inflInit : Heap → Strm → Int → Bool → Outcome Heap Int → Prop
42  inflEnd : Heap → Strm → Outcome Heap Int → Prop
43  inflCopy : Heap → Strm → Strm → Outcome Heap Int → Prop
44  inflDisjoint : Heap → Strm → Strm → Prop
45  inflBack : Heap → Strm → Nat → List UInt8 → BackCallbacks → Outcome Heap BackResult → Prop
46  -- Deflate
47  deflMatches : Heap → Strm → DeflState → Prop
48  deflArgs : Heap → Strm → DeflOp → Prop
49  deflRun : Heap → Strm → DeflOp → Outcome Heap DeflRes → Prop
50  deflNoState : Heap → Strm → Prop
51  deflInitArgs : Heap → Strm → Prop
52  deflInit : Heap → Strm → Int → Int → Int → Int → Int → Bool → Outcome Heap Int → Prop
53  deflEnd : Heap → Strm → Outcome Heap Int → Prop
54  deflCopy : Heap → Strm → Strm → Outcome Heap Int → Prop
55  deflDisjoint : Heap → Strm → Strm → Prop
56  -- One-call functions
57  utilArgs : Heap → Bool → List UInt8 → Nat → Prop
58  compress2 : Heap → Bool → Int → List UInt8 → Nat → Outcome Heap (Int × List UInt8) → Prop
59  compress : Heap → Bool → List UInt8 → Nat → Outcome Heap (Int × List UInt8) → Prop
60  uncompress2 : Heap → Bool → List UInt8 → Nat → Outcome Heap (Int × List UInt8 × Nat) → Prop
61  uncompress : Heap → Bool → List UInt8 → Nat → Outcome Heap (Int × List UInt8) → Prop
62  -- gz files
63  gzMatches : Heap → GzFile → GzHandle → Prop
64  gzArgs : Heap → GzFile → GzOp → Prop
65  gzRun : Heap → GzFile → GzOp → Outcome Heap GzRes → Prop
66  gzOpen : Heap → List Char → Option (List UInt8) → Outcome Heap (Option GzFile) → Prop
67  gzClose : Heap → GzFile → Outcome Heap (Int × List UInt8) → Prop
68
69end ZlibF.Spec.Api