Logic.juvix

module Logic;

-- Imports
import Stdlib.Prelude open;
import Stdlib.Data.Set as Set open using {Set};
import Anoma open;
import Applib open;

import Interface.Projection open using {getCount};

-- Resource Logic
counterLogic
  (publicInputs : Logic.Instance) (privateInputs : Logic.Witness) : Bool :=
  let
    consumed := privateInputs |> Logic.Witness.consumed |> Set.toList;
    created := privateInputs |> Logic.Witness.created |> Set.toList;
  in case consumed, created of
       | [consumedCounter], [createdCounter] :=
         sameKindCheck@{
           consumedCounter;
           createdCounter;
         }
           && case
                both HasEphemerality.get (consumedCounter, createdCounter)
              of {
                | Ephemeral, NonEphemeral :=
                  creationCheck@{
                    createdCounter;
                  }
                | NonEphemeral, NonEphemeral :=
                  incrementationCheck@{
                    consumedCounter;
                    createdCounter;
                  }
                | _, _ := false
              }
       | _, _ := false;

sameKindCheck (consumedCounter createdCounter : Resource) : Bool :=
  kind consumedCounter == kind createdCounter;

creationCheck (createdCounter : Resource) : Bool :=
  getCount createdCounter == 0 && HasQuantity.get createdCounter == 1;

incrementationCheck (consumedCounter createdCounter : Resource) : Bool :=
  let
    expected := getCount consumedCounter + 1;
    actual := getCount createdCounter;
  in expected == actual;