GzTrace.lean

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

1import ZlibF.Spec.Public.Domains
2
3namespace ZlibF.Spec.Public
4open C Zlib.GzFs
5
6/-- Input bytes supplied by the caller, independently of what the implementation accepts.
7Oversized requests are rejected before their pointer is read. -/
8def GzInputBytes (h : Heap) : Call → List UInt8 → Prop
9  | .gzwrite _ p n, bytes => if n.toNat < 2 ^ 31 then Bytes h p n.toNat bytes else bytes = []
10  | .gzfwrite p size n _, bytes =>
11      if size.toNat * n.toNat < 2 ^ 64 then Bytes h p (size.toNat * n.toNat) bytes else bytes = []
12  | .gzputc _ c, bytes => bytes = [c.toUInt32.toUInt8]
13  | .gzputs _ p, bytes => CString h p bytes
14  | .gzprintf _ p args, bytes | .gzvprintf _ p args, bytes => Formatted h p args bytes
15  | _, bytes => bytes = []
16
17def MayFillZeros : Call → Bool
18  | .gzwrite _ _ _ | .gzfwrite _ _ _ _ | .gzputc _ _ | .gzputs _ _
19  | .gzprintf _ _ _ | .gzvprintf _ _ _ | .gzflush _ _ | .gzsetparams _ _ _ => true
20  | _ => false
21
22/-- Record accepted bytes from observable position and pending-seek changes. This is not an
23assumed write contract. The sequence goal must show that those bytes are actually encoded. -/
24def writtenBy (call : Call) (before after : GzState) (input : List UInt8) : List UInt8 :=
25  let zeros := if MayFillZeros call then before.skip.toInt.toNat - after.skip.toInt.toNat else 0
26  List.replicate zeros 0 ++ input.take ((after.x.pos.toInt - before.x.pos.toInt).toNat - zeros)
27
28/-- A complete writer history begins at a new handle. It includes every public gz operation,
29so flushes, parameter changes, queries and forward seeks can be interleaved with writes.
30The file-system state and the actual calls are fixed by the translation. -/
31inductive GzWriterTrace (start : Heap) (world : Fs) (i : Nat) : Heap → Fs → List UInt8 → Prop
32  | initial {s} : GzReachable start world i → start.gzstates i = some s →
33      s.mode = GZ_WRITE → s.size = 0 → s.x.pos = 0 → s.skip = 0 →
34      GzWriterTrace start world i start world []
35  | caller {h after fs input s} : GzWriterTrace start world i h fs input →
36      h.gzstates i = some s → GzCallerFrame h after i s →
37      GzWriterTrace start world i after fs input
38  | step {h after fs fs' input s s' call value bytes} : GzWriterTrace start world i h fs input →
39      h.gzstates i = some s → GzOperation i call → GzArguments h i s call → GzInputBytes h call bytes →
40      call.execute fs h = .ok ((value, fs'), after) → after.gzstates i = some s' →
41      GzWriterTrace start world i after fs' (input ++ writtenBy call s s' bytes)
42
43/-- Closing a successful writer produces exactly the accepted data and any final seek zeros.
44Compression may create concatenated members; transparent writing copies bytes. Existing file
45prefixes and any tail beyond an overwritten segment are retained exactly. -/
46def GzWriterFormat : Prop :=
47  ∀ start world i h fs input initial file node s after fs',
48    GzWriterTrace start world i h fs input → start.gzstates i = some initial →
49    0 ≤ initial.fd.toInt → world.fds[initial.fd.toInt.toNat]? = some (some file) →
50    world.nodes[file.node]? = some node → h.gzstates i = some s →
51    Zlib.Gzclose.gzclose (some (.in_gzstate_x i)) fs h = .ok ((Z_OK, fs'), after) →
52    ∃ encoded final,
53      fs'.nodes[file.node]? = some final ∧ final.isDir = false ∧
54      let offset := if file.append then node.data.size else file.pos
55      let plain := input ++ List.replicate s.skip.toInt.toNat 0
56      (if initial.direct ≠ 0 then encoded = plain else GzipMembers encoded plain) ∧
57      final.data.toList = node.data.toList.take offset ++
58        List.replicate (offset - node.data.size) 0 ++ encoded ++
59        node.data.toList.drop (offset + encoded.length)
60
61end ZlibF.Spec.Public