law fin_cleanup_tests

bend-kube-runtime@0.2.0.0 · LAWS.bend:204

import Base
import bend-kube-runtime@0.2.0.0/src/finalizer.bend as F

204# A deleted object that still carries it is cleaned up, and the finalizer
205# is removed only through a patch that tests it is still ours, at its index.
206law fin_cleanup_tests:
207  for fs: List<&2, String>
208  for name: String
209  for i: U32
210  {F.Fin.state.go(fs, name, Some{i}, True{}) == F.FCleanup{F.Fin.remove_patch(i, name)} : F.FState}