module Observe.Capture

import Observe.Value
import Std.Natural

-- Memory capture is not persistence. Result codes: 0 excluded, 1 queued,
-- 2 selected but dropped, 3 pending at a declared safe boundary, 4 refused.
-- Exclusions have no sequence. Optional loss does have a sequence, so AOS
-- coverage can distinguish unselected quantities from selected records lost.
-- Reserved health/terminal records never consume ordinary event capacity and
-- never drop: an exhausted reserve requires a safe-boundary decision.
def aosCaptureAdmission =
  (lambda unrestricted version : Nat .
    (lambda unrestricted selected : Nat .
      (lambda unrestricted reserved : Nat .
        (lambda unrestricted required : Nat .
          (lambda unrestricted ordinaryCapacity : Nat .
            (lambda unrestricted reservedCapacity : Nat .
              (lambda unrestricted ordinaryUsed : Nat .
                (lambda unrestricted reservedUsed : Nat .
                  (aosChoose
                    Nat
                    (naturalAnd
                      (naturalEqual version 1)
                      (naturalAnd
                        (naturalLessOrEqual selected 1)
                        (naturalAnd
                          (naturalLessOrEqual reserved 1)
                          (naturalAnd
                            (naturalLessOrEqual required 1)
                            (naturalAnd
                              (naturalLessOrEqual 2 reservedCapacity)
                              (naturalAnd
                                (naturalLessOrEqual ordinaryUsed ordinaryCapacity)
                                (naturalLessOrEqual reservedUsed reservedCapacity)))))))
                    (aosChoose
                      Nat
                      (naturalIsZero selected)
                      (aosChoose Nat (naturalIsZero reserved) 0 4)
                      (aosChoose
                        Nat
                        (naturalIsZero reserved)
                        (aosChoose
                          Nat
                          (naturalLess ordinaryUsed ordinaryCapacity)
                          1
                          (aosChoose Nat (naturalIsZero required) 2 3))
                        (aosChoose Nat (naturalLess reservedUsed reservedCapacity) 1 3)))
                    4)))))))))

-- Exact room flags come from the bounded runtime counters. Refuse before any
-- mutation if a required counter would wrap; never record an invented zero.
def aosCaptureCounterAdmission =
  (lambda unrestricted decision : Nat .
    (lambda unrestricted sequenceRoom : Nat .
      (lambda unrestricted droppedRoom : Nat .
        (lambda unrestricted excludedRoom : Nat .
          (aosChoose
            Nat
            (naturalAnd
              (naturalLessOrEqual decision 4)
              (naturalAnd
                (naturalLessOrEqual sequenceRoom 1)
                (naturalAnd (naturalLessOrEqual droppedRoom 1) (naturalLessOrEqual excludedRoom 1))))
            (aosChoose
              Nat
              (naturalEqual decision 0)
              (aosChoose Nat excludedRoom 0 4)
              (aosChoose
                Nat
                (naturalEqual decision 1)
                (aosChoose Nat sequenceRoom 1 4)
                (aosChoose
                  Nat
                  (naturalEqual decision 2)
                  (aosChoose Nat (naturalAnd sequenceRoom droppedRoom) 2 4)
                  decision)))
            4)))))