proofnet-ir/ProofNetIRFutureWorkQueueStatusTests.lean at main · fushanbobfan/proofnet-ir · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
/-
Copyright (c) 2026 ProofNet-IR contributors. All rights reserved.
Released under MIT license as described in the file LICENSE.
Authors: ProofNet-IR contributors
-/

import ProofNetIR.SequentialFigure7FutureWorkQueueStatus

/-!
# Figure-7 future-work queue-status consumer

Reconstructs the public current-state queue classifier, checks the trust
boundary of every new declaration, and executes a kernel-green marker.
-/

namespace ProofNetIRFutureWorkQueueStatusTests

open ProofNetIR
open ProofNetIR.SequentialSchedulerState
open ProofNetIR.SequentialSchedulerState.SequentialStackState
open ProofNetIR.SequentialSchedulerBridge
open ProofNetIR.SequentialFigure7

example {certificate : Certificate} {state : ReservationState}
    (input : ReadyHeadInput state)
    (invariant : SchedulerInvariant certificate state)
    {component : UnificationComponent} {usedLinks owned : List Nat}
    (componentLookup :
      state.core.components[input.rawAge]? = some (some component))
    (occurrence :
      certificate.ComponentOccurrenceWitness component usedLinks owned)
    {boundary : RawTokenAge} {vertex : Vertex}
    (work : FutureWorkAt state boundary vertex)
    (outside : vertex ∉ owned) :
    boundary < input.rawAge := by
  exact work.boundary_lt_active_of_not_owned input invariant componentLookup
    occurrence outside

example {certificate : Certificate} {state : ReservationState}
    (invariant : SchedulerInvariant certificate state)
    {vertex : Vertex} :
    vertex ∈ state.stack.queuedVertices ↔
      ∃ boundary, FutureWorkAt state boundary vertex := by
  exact invariant.mem_queued_iff_exists_futureWorkAt

example {certificate : Certificate} {state : ReservationState}
    (input : ReadyHeadInput state)
    (invariant : SchedulerInvariant certificate state)
    {component : UnificationComponent} {usedLinks owned : List Nat}
    (componentLookup :
      state.core.components[input.rawAge]? = some (some component))
    (occurrence :
      certificate.ComponentOccurrenceWitness component usedLinks owned)
    {vertex : Vertex}
    (unmarked : state.core.marks[vertex]? = some none)
    (outside : vertex ∉ owned) :
    UnmarkedOutsideActiveSchedulerStatus certificate state input owned vertex := by
  exact invariant.unmarkedOutsideActiveSchedulerStatus input componentLookup
    occurrence unmarked outside

#print axioms ProofNetIR.SequentialFigure7.UnmarkedOutsideActiveSchedulerStatus
#print axioms
  ProofNetIR.SequentialFigure7.FutureWorkAt.boundary_lt_active_of_not_owned
#print axioms
  ProofNetIR.SequentialSchedulerBridge.SchedulerInvariant.mem_queued_iff_exists_futureWorkAt
#print axioms
  ProofNetIR.SequentialSchedulerBridge.SchedulerInvariant.unmarkedOutsideActiveSchedulerStatus

end ProofNetIRFutureWorkQueueStatusTests

def main : IO Unit :=
  IO.println "Figure-7 future-work queue status: kernel-green"