Port program_logic/ownp.v


## Summary

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



## Dependencies








**Rocq dependencies:**

- `proofmode/proofmode` (aggregation)
- #219
- #54
- #346
- #348
- #352
- #344