Refactor simps in fsFFIProps

Tasks:
- Make theorems such as `nextFD_numchars` into simps
- Group simps such as `bumpFD_inode_tbl` and `bumpFD_files` into a single lemma
- Prove other direction of lemmas such as `validFD_bumpFD` and add them into simps

Locate the fsFFIProps definitions and the named lemmas nextFD_numchars, bumpFD_inode_tbl, bumpFD_files, and validFD_bumpFD. Read their existing proofs and simp attributes first; done means the requested theorem directions and grouped simplifications are registered as simps and the relevant HOL proofs still pass.

Written by the indexing model from the issue text.