inffast.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.Spec.InflateFastPlatform
2import ZlibF.Proof.PlatformMemory
3import ZlibF.Proof.«inffast.c.final»
4
5/-!
6# inffast.c: discharge size premises from the platform scope
7
8The actual fast call keeps its existing safety and accounting conclusion.
9Its returned heap also satisfies the explicit platform size condition.
10-/
11
12namespace Zlib.Inffast.Proofs
13open C Zlib.Inffast Zlib.Inffast.Spec ZlibF.PlatformMemory
14set_option autoImplicit false
15
16/-- The existing exact fast-call frame establishes preservation of the
17platform scope; a post-state size premise is not assumed. -/
18theorem PlatformEntry.fit_after (entry : PlatformEntry) {after : Heap}
19    (post : FastPost entry.toEnv after) : ByteObjectsFit after := by
20  obtain ⟨used, produced, buffered, bytes, msg, mode, bits, hold,
21    _, _, _, size, _, _, heap, _⟩ := post
22  rw [heap]
23  apply ByteObjectsFit.put_stream
24  have bound : bytes.size < byteObjectLimit := by
25    change bytes.size < 2 ^ 63
26    rw [size]
27    exact entry.toEnv.hAbig
28  exact (entry.platform.with_bytes (block := entry.ob) bound).with_istates _
29
30/-- `void inflate_fast(z_streamp strm, unsigned start)`.
31The explicit LP64 platform scope bounds all represented byte objects by
32`PTRDIFF_MAX`. The other internal fast-entry restrictions are retained.
33Execution, termination, frame and exact writeback follow from the proved
34translated callee; no callee contract is a hypothesis. The returned heap
35preserves the platform condition. This is not the public inflate goal. -/
36theorem inflate_fast_safe_platform (entry : PlatformEntry) :
37    ∃ after, C.run (inflate_fast entry.strm entry.start) entry.h0 = .ok ((), after) ∧
38      FastPost entry.toEnv after ∧ ByteObjectsFit after := by
39  obtain ⟨after, run, post⟩ := inflate_fast_safe entry.toEnv
40  exact ⟨after, run, post, PlatformEntry.fit_after entry post⟩
41
42end Zlib.Inffast.Proofs