mitls-fstar
mitls-fstar copied to clipboard
Idealization coverage
Make sure that tests go into both of ideal's branches.
you mean into both ideal and concrete/non-ideal branches? I agree, this is important.
One could even have tests that ideal and concrete cannot be trivially distinguished via simple strategies. E.g. keys that are the same concretely should also be the same ideally.
Yes, that's what I meant.
Let me know once you get started and whenever you need domain knowledge for this.
Related to crypto code review https://github.com/mitls/mitls-fstar/issues/80
We made progress on the use of idealization flags and their handling in Kremlin. Can someone summarize? @protz @fournet
Should this issue be assigned to a milestone?