Support verifying specifications using multiple triggers with the same name

[RyanGlScott]

Now that Copilot-Language/copilot#572 has landed, a copilot-c99–generated trigger can fire multiple times in a single time step. We will need to update copilot-verifier to account for this, as the verifier currently assumes that a trigger can only fire at most once in a single time step:

copilot-verifier/copilot-verifier/src/Copilot/Verifier.hs

Lines 728 to 737 in 9021bcc

	-- Assert that the trigger functions were called exactly once iff the
	-- associated guard condition was true.
	-- See Note [Global variables for trigger functions].
	forM_ triggerGlobals $ \(nm, gv, guard) ->
	do expectedCount <- liftIO $ do
	one <- natLit sym 1
	zero <- natLit sym 0
	natIte sym guard one zero
	actualCount <- readGlobal gv
	eq <- liftIO $ natEq sym expectedCount actualCount

[RyanGlScott]

The more I think about this, the less sure I am how to support this. To explain what I mean, let me first recap what copilot-verifier does today in order to verify trigger functions. For each trigger function, it checks two properties:

1. The trigger function fires in the original Copilot specification iff the trigger function is called in the C code. That is to say, either the trigger function is fired in both the specification and the C code, or the trigger function is not called at all in the specification and the C code.
2. If the trigger function is fired, then it is passed the same arguments in both the original Copilot specification and the C code.

Both of these properties assume that a trigger function is fired at most once, but this assumption no longer holds in general after Copilot-Language/copilot#572, which allows for a trigger function to be fired multiple times. How, then, should the properties above be updated to reflect this?

I think there is a reasonable story for updating property (1). Rather than checking if each trigger is invoked one or zero times, we would record the total number of times each trigger function is invoked and check that that number is the same in both the original Copilot specification and the C code.

I am much less sure of how to update property (2). Consider this example:

x :: Stream Word8
x = extern "x" Nothing

spec :: Spec
spec = do
  trigger "t" true [arg x]
  trigger "t" true [arg (x * 2)]

Note that the "t" trigger is called twice, but each time with different arguments (x and x * 2, respectively). How do we ensure that the C code also calls the "t" trigger with the same arguments? The answer to this question isn't entirely obvious to me, given the approach that we use to track trigger function arguments. To recap:

• For each trigger function, we register an override that is run whenever copilot-verifier's simulator calls the trigger function.
• When the override is run, it checks that the actual arguments it was supplied (i.e., the arguments in the C code) match the expected arguments (i.e., the arguments in the specification). If they do not match, raise an assertion failure.

This approach works perfectly well when there is exactly one set of expected and actual arguments, but what if there are multiple sets? In that case, the override may be run multiple times, and it's not obvious which invocations of the override corresponds to which sets of arguments. I suppose we could check if the actual arguments equals one of the expected sets of arguments, but this could be more expensive than we want if there are many invocations of a single trigger. Figuring out how to do this precisely requires some more thought.

For now, I think I am going to add a check to copilot-verifier that simply disallows multiple invocations of the same trigger for now, as there is not yet a clear story for how to handle them. I'll keep this issue open as a reminder to lift this restriction.