def
Hex.GraphIso.Nauty.Generic.nodeCall
{n : Nat}
{σ γ : Type}
[Policy σ n]
(ctx : γ)
(inf tcLevel fuel : Nat)
:
NodeFn σ
A node continuation at a fixed recursion bound.
Equations
- Hex.GraphIso.Nauty.Generic.nodeCall ctx inf tcLevel fuel first level numcells st = Hex.GraphIso.Nauty.Generic.node first ctx inf tcLevel fuel level numcells st
Instances For
def
Hex.GraphIso.Nauty.Generic.callContract
{n : Nat}
{σ γ : Type}
[Policy σ n]
(ctx : γ)
(inf tcLevel : Nat)
(C : Contract σ n)
:
Contract σ n
Call equations are unconditional; the desired postcondition follows when the original precondition holds.
Equations
- One or more equations did not get rendered due to their size.
Instances For
structure
Hex.GraphIso.Nauty.Generic.CallPolicy
{n : Nat}
{σ γ : Type}
[Policy σ n]
(ctx : γ)
(inf tcLevel : Nat)
(C : Contract σ n)
:
Local induction rules expressed using the actual recursive calls.
- node_step (fuel : Nat) : C.sweepValid fuel (n + 1) (sweepCall ctx inf tcLevel fuel (n + 1)) → ∀ (first : Bool) (level numcells : Nat) (st : σ), C.nodePre (fuel + 1) first level numcells st → C.nodePost (fuel + 1) first level numcells st (nodeStep ctx tcLevel (sweepCall ctx inf tcLevel fuel (n + 1)) first level numcells st)
- sweep_step (fuel cfuel : Nat) : C.nodeValid fuel (nodeCall ctx inf tcLevel fuel) → C.sweepValid fuel cfuel (sweepCall ctx inf tcLevel fuel cfuel) → ∀ (first : Bool) (level numcells tc tv1 tv : Nat) (cell : VSet n) (index : Nat) (st : σ), C.sweepPre fuel (cfuel + 1) first level numcells tc tv1 (some tv) cell index st → C.sweepPost fuel (cfuel + 1) first level numcells tc tv1 (some tv) cell index st (sweepStep inf (nodeCall ctx inf tcLevel fuel) (sweepCall ctx inf tcLevel fuel cfuel) first level numcells tc tv1 tv cell index st)
Instances For
theorem
Hex.GraphIso.Nauty.Generic.callContract.node_eq
{n : Nat}
{σ γ : Type}
[Policy σ n]
{ctx : γ}
{inf tcLevel : Nat}
{C : Contract σ n}
{fuel : Nat}
{next : NodeFn σ}
(h : (callContract ctx inf tcLevel C).nodeValid fuel next)
:
The call equations expose the actual node continuation and its contract.
theorem
Hex.GraphIso.Nauty.Generic.callContract.sweep_eq
{n : Nat}
{σ γ : Type}
[Policy σ n]
{ctx : γ}
{inf tcLevel : Nat}
{C : Contract σ n}
{fuel cfuel : Nat}
{next : SweepFn σ n}
(h : (callContract ctx inf tcLevel C).sweepValid fuel cfuel next)
:
The call equations expose the actual sweep continuation and its contract.
theorem
Hex.GraphIso.Nauty.Generic.CallPolicy.sound
{n : Nat}
{σ γ : Type}
[Policy σ n]
{ctx : γ}
{inf tcLevel : Nat}
{C : Contract σ n}
(h : CallPolicy ctx inf tcLevel C)
:
SoundPolicy ctx inf tcLevel (callContract ctx inf tcLevel C)
Rules for actual calls satisfy the original generic induction principle.
theorem
Hex.GraphIso.Nauty.Generic.node_calls
{n : Nat}
{σ γ : Type}
[Policy σ n]
{ctx : γ}
{inf tcLevel : Nat}
{C : Contract σ n}
(h : CallPolicy ctx inf tcLevel C)
(first : Bool)
(fuel level numcells : Nat)
(st : σ)
(hin : C.nodePre fuel first level numcells st)
:
Actual-call rules prove the node postcondition under its precondition.
theorem
Hex.GraphIso.Nauty.Generic.sweep_calls
{n : Nat}
{σ γ : Type}
[Policy σ n]
{ctx : γ}
{inf tcLevel : Nat}
{C : Contract σ n}
(h : CallPolicy ctx inf tcLevel C)
(first : Bool)
(fuel cfuel level numcells tc tv1 : Nat)
(cursor : Option Nat)
(cell : VSet n)
(index : Nat)
(st : σ)
(hin : C.sweepPre fuel cfuel first level numcells tc tv1 cursor cell index st)
:
Actual-call rules prove the sweep postcondition under its precondition.