A sweep consumes every unwind that does not leave its level.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.Generic.bound_resume
{n : Nat}
{σ γ : Type}
[Policy σ n]
{fuel cfuel : Nat}
{next : SweepFn σ n}
(hnext : exitContract.sweepValid fuel cfuel next)
(inf : Nat)
(first : Bool)
(level numcells tc tv1 tv : Nat)
(cell : VSet n)
(index : Nat)
(st : σ)
(target : Nat)
(short : Bool)
:
(resume inf next first level numcells tc tv1 tv cell index st).fst = Exit.unwind target short → target < level
Resuming preserves the remaining sweep's bound on its exit.
theorem
Hex.GraphIso.Nauty.Generic.bound_advance
{n : Nat}
{σ γ : Type}
[Policy σ n]
{fuel cfuel : Nat}
{next : SweepFn σ n}
(hnext : exitContract.sweepValid fuel cfuel next)
(inf : Nat)
(first : Bool)
(level numcells tc tv1 tv : Nat)
(cell : VSet n)
(index : Nat)
(st : σ)
(exit : Exit)
(target : Nat)
(short : Bool)
:
(advance inf next first level numcells tc tv1 tv cell index st exit).fst = Exit.unwind target short → target < level
Only an unwind below this level can pass through a receiving sweep.
theorem
Hex.GraphIso.Nauty.Generic.bound_node
{n : Nat}
{σ γ : Type}
[Policy σ n]
{fuel : Nat}
{next : SweepFn σ n}
(hnext : exitContract.sweepValid fuel (n + 1) next)
(ctx : γ)
(tcLevel : Nat)
(first : Bool)
(level numcells : Nat)
(st : σ)
(hlevel : 1 ≤ level)
(hleaf :
first = false →
have r := Policy.visit ctx level numcells st;
have p :=
Policy.chooseTarget first ctx tcLevel level r.fst
(if first = true then Policy.recordFirst level r.snd.fst r.snd.snd
else Policy.compareCodes level r.snd.fst r.snd.snd);
have c := Policy.classify ctx level r.fst p.snd.snd.snd;
∀ (target : Nat) (short : Bool),
(Policy.leafExit c.fst level c.snd).fst = Exit.unwind target short → target < level)
(target : Nat)
(short : Bool)
:
(nodeStep ctx tcLevel next first level numcells st).fst = Exit.unwind target short → target < level
A positive node returns below its level when its local leaf action does. The sweep bound is independent of the state passed to the continuation.
theorem
Hex.GraphIso.Nauty.Generic.exitPolicy
{n : Nat}
{σ γ : Type}
[Policy σ n]
(ctx : γ)
(inf tcLevel : Nat)
:
SoundPolicy ctx inf tcLevel exitContract
The unwind bound depends only on the generic sweep's control flow.
theorem
Hex.GraphIso.Nauty.Generic.sweep_bound
{n : Nat}
{σ γ : Type}
[Policy σ n]
(first : Bool)
(ctx : γ)
(inf tcLevel fuel cfuel level numcells tc tv1 : Nat)
(cursor : Option Nat)
(cell : VSet n)
(index : Nat)
(st : σ)
(target : Nat)
(short : Bool)
:
(sweep first ctx inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).fst = Exit.unwind target short →
target < level
Every sweep returns an unwind strictly below its own level, regardless of the child policies, input state, or recursion bounds.