Add symbolic tests with Halmos

This adds symbolic tests using Halmos. (This post explains more about the benefit of symbolic testing.)

The tested (or verified) properties for mint(), burn(), and transfer() are:

They revert for invalid inputs (e.g., minting zero quantity; minting or transferring to zero address; burning or transferring non-existing tokens or without approvals; etc.)
Only mint() updates nextTokenId, and it does so properly.
They update the token balance and ownership properly for relevant users.
They never alters the token balance and ownership for irrelevant users.

Note:

The tests currently need to refer to private functions and storage variables to describe the above properties, thus running these tests requires temporarily change their visibility from private to internal during testing. This is currently handled in the CI, but may need more scripting to be run locally.
Running these symbolic tests is added in the CI, but it currently takes >30min in the Github Actions (~15min in my laptop), so it may be considered to trigger it less frequently, if time is an issue. The running time can be improved later once Halmos supports utilizing multiple cores.

chiru-labs / ERC721A