(S)CT checkers: accept more combinations of annotations

compiler/CCT/success/sct.jazz

@@ -0,0 +1,21 @@
+#[sct="{ ptr: transient, val : { n: d, s: secret } } -> d"]
+export
+fn load(reg ptr u32[1] a) -> reg u32 {
+  _ = #init_msf();
+  reg u32 r;
+  r = a[0];
+  return r;
+}
+
+#[sct="{n: a, s: secret} × {n: b, s: secret} → c"
+, constraints="a <= c, b <= c"]
+export fn sum(
+  #poly=x reg u32 x,
+  #poly=y reg u32 y)
+-> #poly={x, y} reg u32 {
+  _ = #init_msf();
+  reg u32 r;
+  r = x;
+  r += y;
+  return r;
+}

compiler/src/ct_checker_forward.ml

@@ -448,19 +448,15 @@ let get_annot ensure_annot f =
     let lvl =
       match Lvl.parse ~single:true ~kind_allowed:true x.v_annot, Option.bind sig_annot (SecurityAnnotations.get_nth_argument i) with
       | lvl, None -> lvl
-      | (_, Some _), Some _ ->
-         error ~loc:(x.v_dloc)
-           "security annotations for argument %a redundant with security signature" (Printer.pp_var ~debug:false) x
+      | (_, Some _) as lvl, _ -> lvl
       | _, Some t -> Some Flexible, Some (lvl_of_typ t)
     in
     x.v_name, lvl
   in
   let process_result i a =
     match Lvl.parse ~single:false ~kind_allowed:false a, Option.bind sig_annot (SecurityAnnotations.get_nth_result i) with
     | (_, lvl), None -> lvl
-    | (_, Some _), Some _ ->
-       error ~loc:L._dummy
-         "security annotations for result at position %d redundant with security signature" i
+    | (_, (Some _ as lvl)), _ -> lvl
     | _, Some t -> Some (lvl_of_typ t)
   in
   let ain  = List.mapi process_argument f.f_args in

compiler/src/sct_checker_forward.ml

@@ -184,7 +184,7 @@ and modmsf_c fenv c =
 let error ~loc =
   hierror ~loc:(Lone loc) ~kind:"speculative constant type checker"
 
-let warn ~loc = warning SCTchecker loc
+let warn ~loc = warning SCTchecker (L.i_loc0 loc)
 
 (* --------------------------------------------------------- *)
 (* Inference of the variables that need to contain msf       *)
@@ -1270,14 +1270,11 @@ let init_constraint fenv f =
       | _, None ->
         error ~loc:(x.v_dloc)
           "invalid security annotations %a" pp_var x
-      | [], Some n ->
-         Some (n = SecurityAnnotations.Msf), Some (to_vty n)
       | [Msf], Some n ->
          if not msf then error_msf loc;
          Some true, Some (to_vty n)
-      | _ :: _, Some _ ->
-         error ~loc:(x.v_dloc)
-          "security annotations %a redundant with security signature" pp_var x
+      | _, Some n ->
+         Some (n = SecurityAnnotations.Msf), Some (to_vty n)
     in
     let vty =
       match ovty with
@@ -1348,22 +1345,21 @@ let init_constraint fenv f =
         if b <> Sv.mem x msfs then begin
           let loc = x.v_dloc in
           if b
-          then warn ~loc:(L.i_loc0 loc) "%a does not need to be an MSF" pp_var x
+          then warn ~loc:loc "%a does not need to be an MSF" pp_var x
           else error ~loc "%a should be an MSF" pp_var x
         end;
         b in
     if export then
-      begin match vty with
-      | Direct l ->
-        begin
+      begin let lvls = match vty with
+      | Indirect (p, v) -> [ p; v ]
+      | Direct v -> [ v ]
+      in List.iter begin fun l ->
           try VlPairs.add_le (Env.public env, Env.secret env) l
           with Lvl.Unsat _unsat ->
             error ~loc:(x.v_dloc)
               "security annotation for %a should be at least %s"
                  pp_var x stransient
-        end
-
-      | _ -> assert false
+        end lvls
       end;
     let venv = Env.add_var env venv x vk vty in
     let ty = if msf then IsMsf else IsNormal vty in