Concrete.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Spec.Api.Compress
2import ZlibF.Spec.Api.Iface
3import ZlibF.Zlib.«compress.c»
4
5/-!
6# Concrete execution at the API boundary
7
8`execute` is the graph of the translated computation on the actual runtime heap. It has no
9replaceable run relation and does not assume that a callee obeys a contract. An allocation oracle
10is part of the input heap; the specification must hold for every allowed oracle.
11
12The existing `HeapApi` is still an abstract interface. These definitions do not instantiate its
13history relation or establish stream safety. They provide a concrete boundary that later
14refinement statements can use without an empty abstract relation hiding a fault.
15-/
16
17namespace ZlibF.Spec.Api.Concrete
18
19/-- Execute the translated computation, preserving every returned heap and exposing every fault.
20The abstraction forgets the reason for a fault, never the fact that it happened. -/
21def execute {α : Type} (program : C.M α) (h : C.Heap) : Outcome C.Heap α :=
22  match C.run program h with
23  | .error _ => .fault
24  | .ok (value, after) => .ret after value
25
26/-- Total correctness for this particular translated computation: for every permitted input heap,
27it returns without a runtime fault and satisfies the postcondition, including any frame and
28ownership clauses supplied there. The successful run is required explicitly. Non-vacuity of the
29precondition still needs an initialisation theorem or a concrete permitted input. -/
30def Correct {α : Type} (program : C.M α) (pre : C.Heap → Prop)
31    (post : C.Heap → α → C.Heap → Prop) : Prop :=
32  ∀ before, pre before → ∃ value after,
33    C.run program before = .ok (value, after) ∧ post before value after
34
35/-- The concrete `_z` compressor entry, including argument-error ordering and the stored length.
36`none` models a null `destLen` pointer in this translation; the scalar-pointer abstraction does
37not model aliasing that pointer with caller buffers. No success or safety claim is built in. -/
38def compress2_z (dest : C.BPtr) (capacity : Option UInt64) (source : C.BPtr)
39    (sourceLen : UInt64) (level : Int32) (before : C.Heap) :
40    Outcome C.Heap (Int32 × Option UInt64) :=
41  execute (Zlib.Compress.compress2_z dest capacity source sourceLen level) before
42
43/-- The concrete compatibility wrapper. Unlike `_z`, a null `destLen` is dereferenced by the
44wrapper before `_z` can validate arguments, so the resulting fault must remain observable. -/
45def compress2 (dest : C.BPtr) (capacity : Option UInt64) (source : C.BPtr)
46    (sourceLen : UInt64) (level : Int32) (before : C.Heap) :
47    Outcome C.Heap (Int32 × UInt64) :=
48  execute (Zlib.Compress.compress2 dest capacity source sourceLen level) before
49
50end ZlibF.Spec.Api.Concrete
51
52namespace ZlibF.Spec.Api
53
54/-- `compressBound` and `compressBound_z` on the default LP64 target equal the natural-number
55formula, saturated to `2^64 - 1` on overflow, for every representable argument. This goal mentions
56the actual translated functions. It assumes no compressor contract and no abstract `HeapApi`. -/
57def Goal.compress_bound_value : Prop :=
58  ∀ sourceLen : UInt64,
59    (Zlib.Compress.compressBound sourceLen).toNat = compressBound sourceLen.toNat ∧
60    (Zlib.Compress.compressBound_z sourceLen).toNat = compressBound sourceLen.toNat
61
62/-- With valid pointer shapes, failure of the first default-allocator call in `compress2_z`
63returns the memory error and stores zero. Automatic local storage does not consume that call.
64No new block stays live after the failure. The caller's byte blocks are unchanged. The hypotheses
65allow arbitrary input contents, sizes and static tables: this path returns before reading them.
66This is a concrete error-path goal, not an assumed initialisation contract. -/
67def Goal.compress2_z_first_alloc_failure : Prop :=
68  ∀ (before : C.Heap) (dest source : C.BPtr) (capacity sourceLen : UInt64),
69    C.Fresh before → before.allocOk before.nalloc = false →
70    (0 < capacity → dest ≠ .null) → (0 < sourceLen → source ≠ .null) →
71    ∃ after, C.run (Zlib.Compress.compress2_z dest (some capacity) source sourceLen
72        C.Z_DEFAULT_COMPRESSION) before = .ok ((C.Z_MEM_ERROR, some 0), after) ∧
73      after.nalloc = before.nalloc + 1 ∧ after.bytes = before.bytes ∧
74      (∀ block, after.live block ↔ before.live block)
75
76end ZlibF.Spec.Api