Write a multi-module program where:

1. Module A exports a function with a strong postcondition
2. Module B imports it and relies on that postcondition in its own precondition
3. The full chain verifies end-to-end

Then test what happens when Module A's contract is weakened — does Module B's verification correctly fail?

This stress-tests the cross-module contract propagation path (vera/verifier.py + vera/resolver.py), which is important for any real multi-file program.