[Verif] Add contract examples to dialect doc (#7723)

Add a few examples of how contracts can be used to modularize formal
verification. These will likely become integration tests once the
machinery to execute them is in place.