Improve assumptions in AllocateDeallocateInputValidation spec

CVL does not allow function calls within quantifiers. Hence, we explicitly list the requires for each id. The workaround suggested [here](https://github.com/morpho-org/vault-v2/pull/877#discussion_r2732524163) fails with prover error. Look into the cause and create a certora issue if necessary.