Constrain rent parameters to avoid branching on float

[jberthold]

• assume burn_percent <= 100 (true percentage) to avoid underflow
• constrain lamports_per_byteyear to < 2^32 to avoid overflow for small concrete data sizes
• set exempt_threshold to default of 2.0
• add a special rule to implement how the default exempt_threshold is recognised: 2.0f64 as u64 == 4611686018427387904u64

Closes runtimeverification/solana-token#33

[dkcumming]

Nice. I wonder if something we should do is add a section that is ## Assumptions somewhere where we catalog what we are assuming in one place maybe with Ids too. E.g.

Assumptions

• A. a pinocchio Account has a P-Token Account, Mint, Multisig following
• B. Exemption threshold is assumed to be 2.0
• C. ... and so on

[jberthold]

Nice. I wonder if something we should do is add a section that is ## Assumptions somewhere where we catalog what we are assuming in one place maybe with Ids too. E.g.

Assumptions

• A. a pinocchio Account has a P-Token Account, Mint, Multisig following
• B. Exemption threshold is assumed to be 2.0
• C. ... and so on

Good idea!
We can put this into a file in the feature branch, maybe at the top level, or else we just use the p-token.md file and add a summary at the top.

[jberthold]

Nice. I wonder if something we should do is add a section that is ## Assumptions somewhere where we catalog what we are assuming in one place maybe with Ids too. E.g.

Assumptions

• A. a pinocchio Account has a P-Token Account, Mint, Multisig following
• B. Exemption threshold is assumed to be 2.0
• C. ... and so on

Good idea! We can put this into a file in the feature branch, maybe at the top level, or else we just use the p-token.md file and add a summary at the top.

I have added some information in VERIFICATION_GUIDE.md in runtimeverification/solana-token#90 . Not sure what would be the best place for an overview otherwise.