inflate.c.platform.lean

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

1import ZlibF.Proof.PlatformMemory
2import ZlibF.Proof.«public-inflate-init»
3
4/-!
5# inflate.c: successful initialization preserves the platform size scope
6
7The new clause is derived from the actual initialization writes. It is not
8an additional postcondition assumed for the translated initializer.
9-/
10
11namespace ZlibF.Spec.Public.Proofs.InflateInit
12open C Zlib.Inflate Zlib.Inflate.Spec Zlib.Inflate.Proofs ZlibF.Spec
13open ZlibF.PlatformMemory
14set_option autoImplicit false
15
16/-- Initializing the decoder changes no represented byte-view sizes. -/
17theorem initOkHeap_fits {h : Heap} (fit : ByteObjectsFit h)
18    (r : ZStreamRef) (z : ZStream) (wrap wb : Int32) :
19    ByteObjectsFit (initOkHeap h r z wrap wb) := by
20  unfold initOkHeap
21  dsimp only
22  rw [reset2Heap_null _ _ _ rfl]
23  have allocated : ByteObjectsFit (allocIstHeap (r.put h (initStream2 z h.nextBlk)) (initState r)) :=
24    (fit.put_stream r _).of_storage_eq rfl rfl rfl
25  exact (allocated.put_stream r _).with_istates _
26
27/-- `int inflateInit2_(z_streamp strm, int windowBits, const char *version, int stream_size)`.
28For every accepted window parameter and successful state allocation, actual
29initialization establishes the existing initial-state relation and a reachable
30stream, and preserves the explicit LP64 byte-object platform premise.
31Caller storage must already satisfy that premise. This success theorem does
32not discharge the separate invalid-parameter cleanup target. -/
33theorem inflate_domain_general_platform
34    (h : Heap) (r : ZStreamRef) (version : BPtr) (wb : Int32) (wrap : Api.Wrap) (bits : Nat)
35    (domain : InitDomain h r version) (fit : ByteObjectsFit h)
36    (params : Api.inflWbits wb.toInt = some (wrap, bits))
37    (allocation : h.allocOk h.nalloc = true) :
38    ∃ after, C.run (inflateInit2_ (some r) wb version 112) h = .ok (Z_OK, after) ∧
39      InflateInitial h after r wrap bits ∧ StreamReachable .inflate after r ∧
40      ByteObjectsFit after := by
41  obtain ⟨after, run, initial, reachable⟩ :=
42    inflate_domain_general h r version wb wrap bits domain params allocation
43  obtain ⟨fresh, uniq, globals, value, z, get, allocators, rest⟩ := domain
44  obtain ⟨nonnull, read⟩ := version_value_read value
45  have parameters := params_equiv wb
46  rw [params] at parameters
47  change reset2Params wb = some (publicWrap wrap, Int32.ofInt bits) at parameters
48  have actual := inflateInit2_success get fresh allocation allocators.1 allocators.2
49    nonnull read parameters
50  have same : after = initOkHeap h r z (publicWrap wrap) (Int32.ofInt bits) := by
51    have equality := run.symm.trans actual
52    cases equality
53    rfl
54  refine ⟨after, run, initial, reachable, ?_⟩
55  rw [same]
56  exact initOkHeap_fits fit r z _ _
57
58end ZlibF.Spec.Public.Proofs.InflateInit