Solve TODO in the SCT-checker for conditional expressions

Solve TODO for conditional expressions in the SCT checker

compiler/src/sct_checker_forward.ml

@@ -729,7 +729,7 @@ let rec ty_expr env venv loc (e:expr) : vty =
         let do_indirect lp2 le2 lp3 le3 =
           let lp = Env.fresh2 env in
           let le = Env.fresh2 env in
-          (* TODO why is condition expression also added to constraints? *)
+          (* The condition expression is also added to the constraints because it can be deduced from the result value*)
           VlPairs.add_le l1 lp; VlPairs.add_le lp2 lp; VlPairs.add_le lp3 lp;
           VlPairs.add_le l1 le; VlPairs.add_le le2 le; VlPairs.add_le le3 le;
           Indirect(lp, le) in

compiler/tests/sct-checker/accept.expected

@@ -161,6 +161,14 @@ output corruption: #public
  constraints:
 
 
+File conditional-expr.jazz:
+nomodmsf leak_cond : #secret * #[ptr = public, val = public] *
+                     #[ptr = public, val = public] ->
+#[ptr = secret, val = secret]
+output corruption: #public
+ constraints:
+
+
 File corruption.jazz:
 nomodmsf corrupts_memory : #public * #secret *
                            #[ptr = public, val = secret] *

compiler/tests/sct-checker/fail/conditional-expr.jazz

@@ -0,0 +1,11 @@
+// After running, the return type for x must be #[ptr = secret, val = secret] because leaking the values will leak the result of the condition
+
+#sct="
+    secret *
+    { ptr: public, val: public } *
+    { ptr: public, val: public } ->
+    { ptr: secret, val: public }"
+fn leak_cond(reg u64 sec, reg ptr u64[1] x y) -> reg ptr u64[1] {
+    x = sec == 0 ? x : y;
+    return x;
+}

compiler/tests/sct-checker/reject.expected

@@ -30,6 +30,9 @@ Failed as expected leak_transient: "fail/basic.jazz", line 1 (42-50):
 File bug_887.jazz:
 Failed as expected test_venv: "fail/bug_887.jazz", line 13 (3-4):
                               speculative constant type checker: r has type #secret but should be at most #public
+File conditional-expr.jazz:
+Failed as expected leak_cond: "fail/conditional-expr.jazz", line 6 (11-12):
+                              speculative constant type checker: return type for x is #[ptr = secret, val = secret] it should be less than #[ptr = secret, val = public]
 File corruption.jazz:
 Failed as expected does_corrupt_memory: "fail/corruption.jazz", line 26 (12-13):
                                         speculative constant type checker: return type for y is #[ptr = public, val = transient] it should be less than #[ptr = public, val = public]

compiler/tests/sct-checker/success/conditional-expr.jazz

@@ -0,0 +1,9 @@
+#sct="
+    secret *
+    { ptr: public, val: public } *
+    { ptr: public, val: public } ->
+    { ptr: secret, val: secret }"
+fn leak_cond(reg u64 sec, reg ptr u64[1] x y) -> reg ptr u64[1] {
+    x = sec == 0 ? x : y;
+    return x;
+}