CT checker: accept S-CT annotations #773
Conversation
|
TODO: when there are both annotations for CT and S-CT, ignore the S-CT one instead of failing. |
|
Done, and symmetrically ignore CT annotations when a S-CT signature is given. |
compiler/src/sct_checker_forward.ml
Outdated
| @@ -1330,7 +1327,7 @@ let init_constraint fenv f = | |||
| let process_return i x annot = | |||
| let loc = L.loc x and x = L.unloc x in | |||
| let an = Option.bind sig_annot (SecurityAnnotations.get_nth_result i) in | |||
| let ls, _ = parse_var_annot ~kind_allowed:false ~msf:(not export) annot in | |||
| let ls, _ = try parse_var_annot ~kind_allowed:false ~msf:(not export) annot with Annot.AnnotationError _ -> [], Flexible in | |||
There was a problem hiding this comment.
This look suspicious, can you explain it?
There was a problem hiding this comment.
What happens if the variable declaration has an annotation that you don’t know about? Just ignore the parse error and pretends there is no annotation.
There was a problem hiding this comment.
My problem is that you can catch syntax error in the annotation that are recognised.
And this is done silently.
| return r; | ||
| } | ||
|
|
||
| #[sct="{n: a, s: secret} × {n: b, s: secret} → c" |
There was a problem hiding this comment.
I have tried to remove the ct annotation here, I got the following
error:
"CCT/success/sct.jazz", line 10 (0) to line 21 (1):
constant type checker: variable(s) level c should be used in the input security annotations
It may be ok since we have a way to use CT annotation. But I think it is not necessary.
There was a problem hiding this comment.
Is it a bug in the CT checker? Or, to put it differently, should the CT checker accept free level variables in return type annotations?
There was a problem hiding this comment.
My idea, is that we should be able to have a better translation from
constraint to max.
a -> b -> b, a <= b ---> a -> b -> max (a, b)
a -> b -> c, a <= c, b <= c ---> a -> b -> max (a, b)
Since I am not sur that we can always do this translation, and obtain
a type that is valid for CT, we can keep it like this for the moment.
It is just that the actual translation is simply more partial that what I have in mind.
There was a problem hiding this comment.
I had understood that you would prefer doing the translation the other way round: use “max” in annotations and translate that to constraints for use in the actual checker.
Security annotations for the speculative-ct checker are translated (weakened) when handled by the (non-speculative) CT checker.
compiler/src/sct_checker_forward.ml
Outdated
| let ls = | ||
| match parse_var_annot ~kind_allowed:false ~msf:(not export) annot with | ||
| | exception Annot.AnnotationError (loc, _msg) -> | ||
| warn ~loc "ignored annotation"; [] |
There was a problem hiding this comment.
You don't want to add msg in the warning :-)
There was a problem hiding this comment.
I’ve removed all of this: the SCT checker no longer attempt to parse #poly annotations.
Security annotations for the speculative-ct checker are translated (weakened) when handled by the (non-speculative) CT checker.