From 5b3c440bf2be3e47f67bc75ab5904bccec5e8434 Mon Sep 17 00:00:00 2001
From: McArthur-Alford <mcarthur.alford@proton.me>
Date: Wed, 8 Jul 2026 14:54:02 +1000
Subject: [PATCH 01/11] Rebased

---
 nix/shell.nix | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/nix/shell.nix b/nix/shell.nix
index 381d54df..5908d05c 100644
--- a/nix/shell.nix
+++ b/nix/shell.nix
@@ -54,7 +54,7 @@ mkShell {
   ++ lib.optional stdenv.hostPlatform.isLinux perf;
 
   inputsFrom = [
-    (bincaml.overrideAttrs { doCheck = true; })
+    (bincaml.overrideAttrs { doCheck = false; })
   ];
 
   shellHook = ''

From eca74c28b2029129ae8125790d2675d849a9930a Mon Sep 17 00:00:00 2001
From: McArthur-Alford <mcarthur.alford@proton.me>
Date: Wed, 8 Jul 2026 11:08:38 +1000
Subject: [PATCH 02/11] undoing a debugging change

---
 nix/shell.nix | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/nix/shell.nix b/nix/shell.nix
index 5908d05c..381d54df 100644
--- a/nix/shell.nix
+++ b/nix/shell.nix
@@ -54,7 +54,7 @@ mkShell {
   ++ lib.optional stdenv.hostPlatform.isLinux perf;
 
   inputsFrom = [
-    (bincaml.overrideAttrs { doCheck = false; })
+    (bincaml.overrideAttrs { doCheck = true; })
   ];
 
   shellHook = ''

From f0366c81bebd8e1b71b9489d5f1aaa504e0a199c Mon Sep 17 00:00:00 2001
From: McArthur-Alford <mcarthur.alford@proton.me>
Date: Wed, 8 Jul 2026 14:52:49 +1000
Subject: [PATCH 03/11] CFA Reduction Skeleton

---
 lib/transforms/cfa_reduction.ml | 117 ++++++++++++++++++++++++++++++++
 1 file changed, 117 insertions(+)
 create mode 100644 lib/transforms/cfa_reduction.ml

diff --git a/lib/transforms/cfa_reduction.ml b/lib/transforms/cfa_reduction.ml
new file mode 100644
index 00000000..29726800
--- /dev/null
+++ b/lib/transforms/cfa_reduction.ml
@@ -0,0 +1,117 @@
+open Lang
+open Lang.Common
+
+(* Assumptions: SSA form probably? seems good to me! *)
+(* Also that the program is pure and lacks loops... *)
+let reduce_procedure (proc : Program.proc) : Program.proc =
+  (* Liveness of variables at start of edge. *)
+  (* let live : (Procedure.Edge.block, VarSet.t) Hashtbl.t = *)
+  (* Procedure.blocks_to_list proc *)
+  (* |> List.map (fun (v, b) -> (b, Block.free_vars b)) *)
+  (* |> Hashtbl.of_list *)
+  (* in *)
+
+  (* Termination condition for each edge. *)
+  let term : (IDSet.elt, Var.t) Hashtbl.t = Hashtbl.create 30 in
+
+  (* Constructed reduced edge to replace procedure edges. *)
+  let final_edge =
+    Procedure.fold_blocks_topo_fwd
+      (fun final_edge id block ->
+        let preds = Procedure.blocks_pred proc id |> Iter.to_list in
+
+        (* Compute reachability of this block. *)
+        let reachable =
+          (* Always reachable if no predecessors. *)
+          if List.is_empty preds then Expr.BasilExpr.boolconst true
+          (* Otherwise, reachability is ANY of the predecessors reachability. *)
+            else
+            Expr.BasilExpr.applyintrin ~op:`OR
+              (preds
+              |> List.filter_map (fst %> Hashtbl.get term)
+              |> List.map Expr.BasilExpr.rvar)
+        in
+
+        (* Create ITE statements from phi nodes. *)
+        let ites : Program.stmt =
+          let al =
+            block.phis
+            |> List.map (function
+              | ({ lhs; rhs = hd :: tl } : Var.t Block.phi) ->
+                  let ite =
+                    List.fold_left
+                      (fun acc (in_edge, var) ->
+                        Expr.BasilExpr.ifthenelse
+                          (Expr.BasilExpr.rvar @@ Hashtbl.find term in_edge)
+                          (Expr.BasilExpr.rvar var) acc)
+                      (Expr.BasilExpr.rvar @@ snd hd)
+                      tl
+                  in
+                  (lhs, ite)
+              | _ -> failwith "Encountered phi node with no rhs.")
+          in
+          Stmt.Instr_Assign { attrib = Attrib.empty; al }
+        in
+
+        (* Construct our termination condition by combining
+          initial reachability with any assumes along this edge. *)
+        let termination_var =
+          Procedure.fresh_var proc ~pure:true Types.Boolean
+        in
+        Hashtbl.add term id termination_var;
+        let termination_cond = reachable in
+        let termination =
+          Stmt.Instr_Assign
+            {
+              attrib = Attrib.empty;
+              al = [ (termination_var, termination_cond) ];
+            }
+        in
+
+        final_edge
+        @ List.concat
+            [ [ ites ]; block.stmts |> Vector.to_list; [ termination ] ])
+      List.empty proc
+  in
+
+  failwith ""
+
+(* module Reduction = struct *)
+(* type t = { *)
+(* Variables live at the start of an edge. *)
+(* TODO: should be Edge -> Varset.t *)
+(* live : (Procedure.Edge.block, VarSet.t) Hashtbl.t; *)
+(* Terminating condition variable for each edge. *)
+(* term : (Procedure.Edge.block, Var.t) Hashtbl.t; *)
+(* Variable renaming at termination of an edge. *)
+(* names : (Procedure.Edge.block, Var.t) Hashtbl.t; *)
+(* Statement list of the new single-edge procedure. *)
+(* final_edge : Program.stmt list; *)
+(* } *)
+
+(* let create (proc : Program.proc) : t = *)
+(* { *)
+(* live = *)
+(* Procedure.blocks_to_list proc *)
+(* |> List.map (fun (v, b) -> (b, Block.free_vars b)) *)
+(* |> Hashtbl.of_list; *)
+(* term = Hashtbl.create 30; *)
+(* names = Hashtbl.create 30; *)
+(* final_edge = List.empty; *)
+(* } *)
+(* end *)
+
+(* Assumptions: SSA form probably? seems good to me! *)
+(* Also that the program is pure and lacks loops... *)
+(* let reduce_procedure (proc : Program.proc) : Program.proc = *)
+(* let reduction = Reduction.create proc in *)
+(* let reduction = *)
+(* Procedure.fold_blocks_topo_fwd *)
+(* (fun final_edge id block -> *)
+(* let preds = () in *)
+(* let reachable = () in *)
+(* Hashtbl.add (reduction.live) *)
+(* final_edge) *)
+(* reduction proc *)
+(* in *)
+(* failwith "" *)

From 5ecb87f5267c5458ad6ca352271a2231987b6ae5 Mon Sep 17 00:00:00 2001
From: McArthur-Alford <mcarthur.alford@proton.me>
Date: Wed, 8 Jul 2026 15:41:30 +1000
Subject: [PATCH 04/11] Reduction is working

---
 lib/passes.ml                   |  10 ++
 lib/transforms/cfa_reduction.ml | 172 +++++++++++++-------------------
 2 files changed, 82 insertions(+), 100 deletions(-)

diff --git a/lib/passes.ml b/lib/passes.ml
index 49168f62..03c3fdd0 100644
--- a/lib/passes.ml
+++ b/lib/passes.ml
@@ -199,6 +199,15 @@ module PassManager = struct
       invariants = Invariants.presupposes [ Params ] ~establishes:[ SSA ];
     }
 
+  let cfa_reduction =
+    {
+      name = "cfa-reduction";
+      apply = Proc Transforms.Cfa_reduction.reduce_procedure;
+      doc =
+        "Performs reduction of acyclic CFA";
+      invariants = Invariants.presupposes [ SSA ];
+    }
+
   let remove_unreachable_blocks =
     {
       name = "remove-unreachable-block";
@@ -453,6 +462,7 @@ module PassManager = struct
       read_uninit false;
       read_uninit true;
       sssa;
+      cfa_reduction;
       sva;
       full_ssa;
       chc_infer_invariants;
diff --git a/lib/transforms/cfa_reduction.ml b/lib/transforms/cfa_reduction.ml
index 29726800..dbc0ec53 100644
--- a/lib/transforms/cfa_reduction.ml
+++ b/lib/transforms/cfa_reduction.ml
@@ -3,115 +3,87 @@ open Lang.Common
 
 (* Assumptions: SSA form probably? seems good to me! *)
 (* Also that the program is pure and lacks loops... *)
-let reduce_procedure (proc : Program.proc) : Program.proc =
-  (* Liveness of variables at start of edge. *)
-  (* let live : (Procedure.Edge.block, VarSet.t) Hashtbl.t = *)
-  (* Procedure.blocks_to_list proc *)
-  (* |> List.map (fun (v, b) -> (b, Block.free_vars b)) *)
-  (* |> Hashtbl.of_list *)
-  (* in *)
-
+let construct_final_edge proc =
   (* Termination condition for each edge. *)
   let term : (IDSet.elt, Var.t) Hashtbl.t = Hashtbl.create 30 in
+  Procedure.fold_blocks_topo_fwd
+    (fun final_edge id block ->
+      let preds = Procedure.blocks_pred proc id |> Iter.to_list in
 
-  (* Constructed reduced edge to replace procedure edges. *)
-  let final_edge =
-    Procedure.fold_blocks_topo_fwd
-      (fun final_edge id block ->
-        let preds = Procedure.blocks_pred proc id |> Iter.to_list in
+      (* Compute reachability of this block. *)
+      let reachable =
+        (* Always reachable if no predecessors. *)
+        if List.is_empty preds then Expr.BasilExpr.boolconst true
+        (* Otherwise, reachability is ANY of the predecessors reachability. *)
+          else
+          Expr.BasilExpr.applyintrin ~op:`OR
+            (preds
+            |> List.filter_map (fst %> Hashtbl.get term)
+            |> List.map Expr.BasilExpr.rvar)
+      in
 
-        (* Compute reachability of this block. *)
-        let reachable =
-          (* Always reachable if no predecessors. *)
-          if List.is_empty preds then Expr.BasilExpr.boolconst true
-          (* Otherwise, reachability is ANY of the predecessors reachability. *)
-            else
-            Expr.BasilExpr.applyintrin ~op:`OR
-              (preds
-              |> List.filter_map (fst %> Hashtbl.get term)
-              |> List.map Expr.BasilExpr.rvar)
+      (* Create ITE statements from phi nodes. *)
+      let ites : Program.stmt =
+        let al =
+          block.phis
+          |> List.map (function
+            | ({ lhs; rhs = hd :: tl } : Var.t Block.phi) ->
+                let ite =
+                  List.fold_left
+                    (fun acc (in_edge, var) ->
+                      Expr.BasilExpr.ifthenelse
+                        (Expr.BasilExpr.rvar @@ Hashtbl.find term in_edge)
+                        (Expr.BasilExpr.rvar var) acc)
+                    (Expr.BasilExpr.rvar @@ snd hd)
+                    tl
+                in
+                (lhs, ite)
+            | _ -> failwith "Encountered phi node with no rhs.")
         in
+        Stmt.Instr_Assign { attrib = Attrib.empty; al }
+      in
 
-        (* Create ITE statements from phi nodes. *)
-        let ites : Program.stmt =
-          let al =
-            block.phis
-            |> List.map (function
-              | ({ lhs; rhs = hd :: tl } : Var.t Block.phi) ->
-                  let ite =
-                    List.fold_left
-                      (fun acc (in_edge, var) ->
-                        Expr.BasilExpr.ifthenelse
-                          (Expr.BasilExpr.rvar @@ Hashtbl.find term in_edge)
-                          (Expr.BasilExpr.rvar var) acc)
-                      (Expr.BasilExpr.rvar @@ snd hd)
-                      tl
-                  in
-                  (lhs, ite)
-              | _ -> failwith "Encountered phi node with no rhs.")
-          in
-          Stmt.Instr_Assign { attrib = Attrib.empty; al }
-        in
+      (* Add a fresh termination variable to assign the condition. *)
+      let termination_var = Procedure.fresh_var proc ~pure:true Types.Boolean in
+      Hashtbl.add term id termination_var;
 
-        (* Construct our termination condition by combining
+      (* Construct our termination condition by combining
           initial reachability with any assumes along this edge. *)
-        let termination_var =
-          Procedure.fresh_var proc ~pure:true Types.Boolean
-        in
-        Hashtbl.add term id termination_var;
-        let termination_cond = reachable in
-        let termination =
-          Stmt.Instr_Assign
-            {
-              attrib = Attrib.empty;
-              al = [ (termination_var, termination_cond) ];
-            }
-        in
+      let termination_cond =
+        Expr.BasilExpr.applyintrin ~op:`AND
+          ([ reachable ]
+          @ (Block.stmts_iter block
+            |> Iter.filter_map (function
+              | Stmt.Instr_Assume { body; branch } -> Some body
+              | _ -> None)
+            |> Iter.to_list))
+      in
+      let termination =
+        Stmt.Instr_Assign
+          {
+            attrib = Attrib.empty;
+            al = [ (termination_var, termination_cond) ];
+          }
+      in
 
-        final_edge
-        @ List.concat
-            [ [ ites ]; block.stmts |> Vector.to_list; [ termination ] ])
-      List.empty proc
-  in
+      (* Final edge is existing statements plus:
+          1. the ites for the new edge being merged in.
+          2. the statements for the new edge body.
+          3. an assignment to the termination variable.
+        *)
+      final_edge
+      @ List.concat [ [ ites ]; block.stmts |> Vector.to_list; [ termination ] ])
+    List.empty proc
 
-  failwith ""
-
-(* module Reduction = struct *)
-(* type t = { *)
-(* Variables live at the start of an edge. *)
-(* TODO: should be Edge -> Varset.t *)
-(* live : (Procedure.Edge.block, VarSet.t) Hashtbl.t; *)
-(* Terminating condition variable for each edge. *)
-(* term : (Procedure.Edge.block, Var.t) Hashtbl.t; *)
-(* Variable renaming at termination of an edge. *)
-(* names : (Procedure.Edge.block, Var.t) Hashtbl.t; *)
-(* Statement list of the new single-edge procedure. *)
-(* final_edge : Program.stmt list; *)
-(* } *)
+let reduce_procedure (proc : Program.proc) : Program.proc =
+  (* Constructed reduced edge to replace procedure blocks. *)
+  let final_edge = construct_final_edge proc in
 
-(* let create (proc : Program.proc) : t = *)
-(* { *)
-(* live = *)
-(* Procedure.blocks_to_list proc *)
-(* |> List.map (fun (v, b) -> (b, Block.free_vars b)) *)
-(* |> Hashtbl.of_list; *)
-(* term = Hashtbl.create 30; *)
-(* names = Hashtbl.create 30; *)
-(* final_edge = List.empty; *)
-(* } *)
-(* end *)
+  let out_proc, id = Procedure.fresh_block proc ~stmts:final_edge () in
 
-(* Assumptions: SSA form probably? seems good to me! *)
-(* Also that the program is pure and lacks loops... *)
-(* let reduce_procedure (proc : Program.proc) : Program.proc = *)
-(* let reduction = Reduction.create proc in *)
-(* let reduction = *)
-(* Procedure.fold_blocks_topo_fwd *)
-(* (fun final_edge id block -> *)
-(* let preds = () in *)
-(* let reachable = () in *)
-(* Hashtbl.add (reduction.live) *)
-(* final_edge) *)
-(* reduction proc *)
-(* in *)
-(* failwith "" *)
+  (* Make this the entry and return block. *)
+  let out_proc = Procedure.set_entry_block out_proc id in
+  Procedure.PG.map_graph
+    (fun g ->
+      Procedure.G.add_edge g (Procedure.Vert.End id) Procedure.Vert.Return)
+    out_proc

From 12154f31a5935bca38e18d47883cc57928f8bc08 Mon Sep 17 00:00:00 2001
From: McArthur-Alford <mcarthur.alford@proton.me>
Date: Wed, 8 Jul 2026 15:56:21 +1000
Subject: [PATCH 05/11] Clean up the graph to prevent errors

---
 lib/transforms/cfa_reduction.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/lib/transforms/cfa_reduction.ml b/lib/transforms/cfa_reduction.ml
index dbc0ec53..ce723c43 100644
--- a/lib/transforms/cfa_reduction.ml
+++ b/lib/transforms/cfa_reduction.ml
@@ -79,7 +79,11 @@ let reduce_procedure (proc : Program.proc) : Program.proc =
   (* Constructed reduced edge to replace procedure blocks. *)
   let final_edge = construct_final_edge proc in
 
-  let out_proc, id = Procedure.fresh_block proc ~stmts:final_edge () in
+  let out_proc =
+    proc |> Procedure.iter_blocks |> Iter.map fst
+    |> Iter.fold (fun acc id -> Procedure.remove_block acc id) proc
+  in
+  let out_proc, id = Procedure.fresh_block out_proc ~stmts:final_edge () in
 
   (* Make this the entry and return block. *)
   let out_proc = Procedure.set_entry_block out_proc id in

From 8a6c59b410b58820f7f46950b069d0b8754a3b6b Mon Sep 17 00:00:00 2001
From: McArthur-Alford <mcarthur.alford@proton.me>
Date: Wed, 8 Jul 2026 16:01:17 +1000
Subject: [PATCH 06/11] Test case

---
 test/cram/cfa_reduction.il   | 23 +++++++++++++++++++++++
 test/cram/cfa_reduction.sexp |  6 ++++++
 test/cram/cfa_reduction.t    |  2 ++
 test/cram/dune               |  2 ++
 4 files changed, 33 insertions(+)
 create mode 100644 test/cram/cfa_reduction.il
 create mode 100644 test/cram/cfa_reduction.sexp
 create mode 100644 test/cram/cfa_reduction.t

diff --git a/test/cram/cfa_reduction.il b/test/cram/cfa_reduction.il
new file mode 100644
index 00000000..aa2fadd6
--- /dev/null
+++ b/test/cram/cfa_reduction.il
@@ -0,0 +1,23 @@
+prog entry @f1;
+
+proc @f1(a:bv64) -> (c:bv64)
+[
+ block %a [
+  var x:bv64 := a;
+  goto(%b, %c);
+ ];
+ block %b [
+  guard(bvuge(x,0:bv64));
+  var x := bvadd(x:bv64,1:bv64);
+  goto(%exit);
+ ];
+ block %c [
+  guard(bvult(x,0:bv64));
+  var x := bvsub(x:bv64,1:bv64);
+  goto(%exit);
+ ];
+ block %exit [
+  var c:bv64 := x;
+  return;
+ ];
+];
diff --git a/test/cram/cfa_reduction.sexp b/test/cram/cfa_reduction.sexp
new file mode 100644
index 00000000..5c2c9d03
--- /dev/null
+++ b/test/cram/cfa_reduction.sexp
@@ -0,0 +1,6 @@
+(load-il "./cfa_reduction.il")
+(run-transforms "ssa")
+(run-transforms "cfa-reduction")
+(run-transforms "simplify")
+(dump-il "./out.il")
+
diff --git a/test/cram/cfa_reduction.t b/test/cram/cfa_reduction.t
new file mode 100644
index 00000000..f06d9481
--- /dev/null
+++ b/test/cram/cfa_reduction.t
@@ -0,0 +1,2 @@
+  $ bincaml script ./cfa_reduction.sexp
+  $ cat ./out.il
diff --git a/test/cram/dune b/test/cram/dune
index 83a26539..769da30e 100644
--- a/test/cram/dune
+++ b/test/cram/dune
@@ -62,6 +62,8 @@
   ll_spec.sexp
   repeated_ssa.il
   repeated_ssa.sexp
+  cfa_reduction.il
+  cfa_reduction.sexp
   ../../bin/main.exe))
 
 (cram

From 16f2b653d05b356b39453da704e08a05d1f92ff1 Mon Sep 17 00:00:00 2001
From: McArthur-Alford <mcarthur.alford@proton.me>
Date: Wed, 8 Jul 2026 16:01:45 +1000
Subject: [PATCH 07/11] formatting

---
 lib/passes.ml                | 3 +--
 test/cram/cfa_reduction.sexp | 1 -
 2 files changed, 1 insertion(+), 3 deletions(-)

diff --git a/lib/passes.ml b/lib/passes.ml
index 03c3fdd0..9fea3352 100644
--- a/lib/passes.ml
+++ b/lib/passes.ml
@@ -203,8 +203,7 @@ module PassManager = struct
     {
       name = "cfa-reduction";
       apply = Proc Transforms.Cfa_reduction.reduce_procedure;
-      doc =
-        "Performs reduction of acyclic CFA";
+      doc = "Performs reduction of acyclic CFA";
       invariants = Invariants.presupposes [ SSA ];
     }
 
diff --git a/test/cram/cfa_reduction.sexp b/test/cram/cfa_reduction.sexp
index 5c2c9d03..02b038d7 100644
--- a/test/cram/cfa_reduction.sexp
+++ b/test/cram/cfa_reduction.sexp
@@ -3,4 +3,3 @@
 (run-transforms "cfa-reduction")
 (run-transforms "simplify")
 (dump-il "./out.il")
-

From efdaaeb6d5923cfbb46bd1b80d9bb4435a682f20 Mon Sep 17 00:00:00 2001
From: McArthur-Alford <mcarthur.alford@proton.me>
Date: Wed, 8 Jul 2026 16:02:32 +1000
Subject: [PATCH 08/11] cram promotion

---
 test/cram/cfa_reduction.t | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/test/cram/cfa_reduction.t b/test/cram/cfa_reduction.t
index f06d9481..a7fd24ac 100644
--- a/test/cram/cfa_reduction.t
+++ b/test/cram/cfa_reduction.t
@@ -1,2 +1,23 @@
   $ bincaml script ./cfa_reduction.sexp
+  (load-il ./cfa_reduction.il)
+  (run-transforms ssa)
+  (run-transforms cfa-reduction)
+  (run-transforms simplify)
+  (dump-il ./out.il)
   $ cat ./out.il
+  proc @f1(a:bv64)  -> (c:bv64) {  }
+    
+  
+  [
+     block %block [
+       var v:bool := true;
+       guard bvult(a:bv64, 0x0:bv64);
+       guard boolnot(bvult(a:bv64, 0x0:bv64));
+       var v_2:bool := booland(v:bool, boolnot(bvult(a:bv64, 0x0:bv64)));
+       var x_6:bv64 := if v_2:bool then bvadd(a:bv64, 0x1:bv64) else bvsub(a:bv64,
+        0x1:bv64);
+       var c:bv64 := x_6:bv64;
+       return;
+     ]
+  ];
+  prog entry @f1;

From 6268b66bdfeae9d81c0caad3594dfb3c003311a4 Mon Sep 17 00:00:00 2001
From: McArthur-Alford <mcarthur.alford@proton.me>
Date: Wed, 8 Jul 2026 16:04:35 +1000
Subject: [PATCH 09/11] Cleaned up a comment :)

---
 lib/transforms/cfa_reduction.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/lib/transforms/cfa_reduction.ml b/lib/transforms/cfa_reduction.ml
index ce723c43..b3678963 100644
--- a/lib/transforms/cfa_reduction.ml
+++ b/lib/transforms/cfa_reduction.ml
@@ -1,8 +1,7 @@
 open Lang
 open Lang.Common
 
-(* Assumptions: SSA form probably? seems good to me! *)
-(* Also that the program is pure and lacks loops... *)
+(* Assumes program is in SSA, acyclic and pure. *)
 let construct_final_edge proc =
   (* Termination condition for each edge. *)
   let term : (IDSet.elt, Var.t) Hashtbl.t = Hashtbl.create 30 in

From 73a44b073ab487b176d6717e1ef68032a889f6fc Mon Sep 17 00:00:00 2001
From: McArthur-Alford <mcarthur.alford@proton.me>
Date: Wed, 8 Jul 2026 16:18:53 +1000
Subject: [PATCH 10/11] simplify removed

---
 test/cram/cfa_reduction.sexp |  2 +-
 test/cram/cfa_reduction.t    | 22 +++++++++++++++-------
 2 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/test/cram/cfa_reduction.sexp b/test/cram/cfa_reduction.sexp
index 02b038d7..f9ef09af 100644
--- a/test/cram/cfa_reduction.sexp
+++ b/test/cram/cfa_reduction.sexp
@@ -1,5 +1,5 @@
 (load-il "./cfa_reduction.il")
 (run-transforms "ssa")
 (run-transforms "cfa-reduction")
-(run-transforms "simplify")
+; (run-transforms "simplify")
 (dump-il "./out.il")
diff --git a/test/cram/cfa_reduction.t b/test/cram/cfa_reduction.t
index a7fd24ac..4891c20d 100644
--- a/test/cram/cfa_reduction.t
+++ b/test/cram/cfa_reduction.t
@@ -2,7 +2,6 @@
   (load-il ./cfa_reduction.il)
   (run-transforms ssa)
   (run-transforms cfa-reduction)
-  (run-transforms simplify)
   (dump-il ./out.il)
   $ cat ./out.il
   proc @f1(a:bv64)  -> (c:bv64) {  }
@@ -10,13 +9,22 @@
   
   [
      block %block [
-       var v:bool := true;
-       guard bvult(a:bv64, 0x0:bv64);
-       guard boolnot(bvult(a:bv64, 0x0:bv64));
-       var v_2:bool := booland(v:bool, boolnot(bvult(a:bv64, 0x0:bv64)));
-       var x_6:bv64 := if v_2:bool then bvadd(a:bv64, 0x1:bv64) else bvsub(a:bv64,
-        0x1:bv64);
+       nop;
+       var x_1:bv64 := a:bv64;
+       var v:bool := booland(true);
+       nop;
+       var x_2:bv64 := x_1:bv64;
+       guard bvult(x_2:bv64, 0x0:bv64);
+       var x_3:bv64 := bvsub(x_2:bv64, 0x1:bv64);
+       var v_1:bool := booland(boolor(v:bool), bvult(x_2:bv64, 0x0:bv64));
+       nop;
+       var x_4:bv64 := x_1:bv64;
+       guard boolnot(bvult(x_4:bv64, 0x0:bv64));
+       var x_5:bv64 := bvadd(x_4:bv64, 0x1:bv64);
+       var v_2:bool := booland(boolor(v:bool), boolnot(bvult(x_4:bv64, 0x0:bv64)));
+       var x_6:bv64 := if v_2:bool then x_5:bv64 else x_3:bv64;
        var c:bv64 := x_6:bv64;
+       var v_3:bool := booland(boolor(v_2:bool, v_1:bool));
        return;
      ]
   ];

From 367c7f93ca0bc0fe4864d38a5aaf9f9015e491a1 Mon Sep 17 00:00:00 2001
From: McArthur-Alford <mcarthur.alford@proton.me>
Date: Wed, 8 Jul 2026 16:25:49 +1000
Subject: [PATCH 11/11] filter out guards

---
 lib/transforms/cfa_reduction.ml | 16 ++++++++++++++--
 test/cram/cfa_reduction.sexp    |  2 +-
 test/cram/cfa_reduction.t       | 20 +++++---------------
 3 files changed, 20 insertions(+), 18 deletions(-)

diff --git a/lib/transforms/cfa_reduction.ml b/lib/transforms/cfa_reduction.ml
index b3678963..77411e3b 100644
--- a/lib/transforms/cfa_reduction.ml
+++ b/lib/transforms/cfa_reduction.ml
@@ -53,7 +53,7 @@ let construct_final_edge proc =
           ([ reachable ]
           @ (Block.stmts_iter block
             |> Iter.filter_map (function
-              | Stmt.Instr_Assume { body; branch } -> Some body
+              | Stmt.Instr_Assume { body; branch = true } -> Some body
               | _ -> None)
             |> Iter.to_list))
       in
@@ -71,7 +71,19 @@ let construct_final_edge proc =
           3. an assignment to the termination variable.
         *)
       final_edge
-      @ List.concat [ [ ites ]; block.stmts |> Vector.to_list; [ termination ] ])
+      @ List.concat
+          [
+            [ ites ];
+            (* Filter out the now unnecessary guards. *)
+            block.stmts |> Vector.to_list
+            |> List.filter (fun s ->
+                not
+                @@
+                match s with
+                | Stmt.Instr_Assume { branch = true } -> true
+                | _ -> false);
+            [ termination ];
+          ])
     List.empty proc
 
 let reduce_procedure (proc : Program.proc) : Program.proc =
diff --git a/test/cram/cfa_reduction.sexp b/test/cram/cfa_reduction.sexp
index f9ef09af..02b038d7 100644
--- a/test/cram/cfa_reduction.sexp
+++ b/test/cram/cfa_reduction.sexp
@@ -1,5 +1,5 @@
 (load-il "./cfa_reduction.il")
 (run-transforms "ssa")
 (run-transforms "cfa-reduction")
-; (run-transforms "simplify")
+(run-transforms "simplify")
 (dump-il "./out.il")
diff --git a/test/cram/cfa_reduction.t b/test/cram/cfa_reduction.t
index 4891c20d..8e8dda7b 100644
--- a/test/cram/cfa_reduction.t
+++ b/test/cram/cfa_reduction.t
@@ -2,6 +2,7 @@
   (load-il ./cfa_reduction.il)
   (run-transforms ssa)
   (run-transforms cfa-reduction)
+  (run-transforms simplify)
   (dump-il ./out.il)
   $ cat ./out.il
   proc @f1(a:bv64)  -> (c:bv64) {  }
@@ -9,22 +10,11 @@
   
   [
      block %block [
-       nop;
-       var x_1:bv64 := a:bv64;
-       var v:bool := booland(true);
-       nop;
-       var x_2:bv64 := x_1:bv64;
-       guard bvult(x_2:bv64, 0x0:bv64);
-       var x_3:bv64 := bvsub(x_2:bv64, 0x1:bv64);
-       var v_1:bool := booland(boolor(v:bool), bvult(x_2:bv64, 0x0:bv64));
-       nop;
-       var x_4:bv64 := x_1:bv64;
-       guard boolnot(bvult(x_4:bv64, 0x0:bv64));
-       var x_5:bv64 := bvadd(x_4:bv64, 0x1:bv64);
-       var v_2:bool := booland(boolor(v:bool), boolnot(bvult(x_4:bv64, 0x0:bv64)));
-       var x_6:bv64 := if v_2:bool then x_5:bv64 else x_3:bv64;
+       var v:bool := true;
+       var v_2:bool := booland(v:bool, boolnot(bvult(a:bv64, 0x0:bv64)));
+       var x_6:bv64 := if v_2:bool then bvadd(a:bv64, 0x1:bv64) else bvsub(a:bv64,
+        0x1:bv64);
        var c:bv64 := x_6:bv64;
-       var v_3:bool := booland(boolor(v_2:bool, v_1:bool));
        return;
      ]
   ];