Add syntactic to whitelist

[Scott-Guest]

Part of #4579

Adds the syntactic attribute to the whitelist, and checks that it is only applied to simplification rules.

Notably, we still need to:

• Check that the arguments actually refer to existing clauses
• Tag the underlying clauses and re-construct the attribute at the end of the compilation pipeline because the requires clauses may be manipulated during compilation

[PetarMax]

@Scott-Guest Were you meaning to add @geo2a and myself as reviewers?

[geo2a]

LGTM!

Just curios: does the frontend has any unit tests for this sort of functionality?

[Scott-Guest]

@geo2a We have tests for the attribute whitelist infrastructure in general (buried somewhere in regression-new), but don't specifically test each entry. I'll add a small test for the "only on simplification rules" part though.