Port program_logic/adequacy.v


## Summary

Port [`program_logic/adequacy.v`](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris/program_logic/adequacy.v).



## Dependencies








**Rocq dependencies:**

- `proofmode/proofmode` (aggregation)
- #254
- #220
- #243
- #277
- #346