Support verifying specifications using multiple triggers with the same name #74

Activity

1. RyanGlScott

   added

   enhancementNew feature or requestNew feature or request

   on Jan 6, 2025
2. RyanGlScott commented on Jan 20, 2025

   

   RyanGlScott

   on Jan 20, 2025

   CollaboratorAuthor

   More actions

   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.
3. RyanGlScott

   added 3 commits that reference this issue on Jan 20, 2025

   Reject multiple triggers with the same name. Refs #74.

   ...

   f694d21

   Document changes in the CHANGELOG. Refs #74.

   67b270e

   Merge pull request #75 from Copilot-Language/T74-reject-multiple-trig…

   ...

   26d5649