388def captureSiteAdmission =
389 (lambda unrestricted policy : (family CapturePolicy) .
390 (lambda unrestricted site : (family CaptureSite) .
391 (eliminate
392 CaptureSite
393 (lambda unrestricted current : (family CaptureSite) . Nat)
394 site
395 (branch
396 CaptureSiteValue
397 identity
398 name
399 kind
400 reserved
401 dimensions
402 stride
403 .
404 (naturalAnd
405 (capturePolicyAdmission policy)
406 (naturalAnd
407 (aosIsIdentity identity)
408 (naturalAnd
409 (naturalNonzero (bytes-length name))
410 (naturalAnd
411 (naturalLessOrEqual (bytes-length name) 256)
412 (naturalAnd
413 (naturalLessOrEqual reserved 1)
414 (naturalAnd
415 (naturalLessOrEqual dimensions (capturePolicyDimensionLimit policy))
416 (naturalAnd
417 (naturalNonzero stride)
418 (naturalAnd
419 (naturalLessOrEqual stride 18446744073709551615)
420 (naturalAnd
421 (aosChoose
422 Nat
423 (bytes-equal (captureClassName kind) b"health")
424 reserved
425 1)
426 (aosChoose
427 Nat
428 reserved
429 (naturalAnd
430 (naturalEqual (captureClassLevel kind) 0)
431 (naturalEqual stride 1))
432 1))))))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.