Add branch optimization pass for Venom IR

AGENTS.md

@@ -20,6 +20,8 @@ Only use Bash for:
 
 **Don't prepend commands:** If you chain commands with `&&`, the permission is matched against the first command. Don't prepend `cd`, `touch`, `export`, etc. before allowed commands - it breaks permission matching.
 
+**No `time` or `timeout` wrappers:** The Bash tool already reports execution time in its output and has a `timeout` parameter. Don't use `time` or `timeout` commands - they break permission matching.
+
 ## Completion Standard
 
 If you are working on a proof, your task is NOT complete until:
@@ -139,12 +141,26 @@ For commands with HOL term quotations (backquotes), **always use a temp file**:
 
 ```sml
 (* .hol_cmd.sml *)
-g `!n. n + 0 = n`;
-e (Induct_on `n`);
+gt `!n. n + 0 = n`;
+etq "Induct_on `n`";
 ```
 
 Then: `~/hol-agents/hol-agent-helper.sh send:.hol_cmd.sml`
 
+### Use Goaltree Mode (gt/etq)
+
+**Always use goaltree mode** instead of goalstack for interactive proofs:
+
+| Command | Purpose |
+|---------|---------|
+| `gt \`tm\`` | Start proof (not `g`) |
+| `etq "tac"` | Apply tactic as string (not `e`) |
+| `p()` | Show proof tree with tactic names |
+| `backup()` | Undo last tactic |
+| `top_goals()` | List remaining goals |
+
+**Why?** `etq` records tactics as strings. When done, `p()` outputs the exact proof script ready to paste into your `Theorem ... Proof ... QED` block.
+
 ### File Naming Conventions
 
 Local test/scratch files should use **dot prefixes** to keep them gitignored:

Holmakefile

@@ -1 +1 @@
-INCLUDES=$(HOLDIR)/examples/Crypto/Keccak $(VFMDIR)/util $(VFMDIR)/spec venom
+INCLUDES=$(HOLDIR)/examples/Crypto/Keccak $(VFMDIR)/util $(VFMDIR)/spec venom venom/passes/branch_opt

venom/passes/branch_opt/Holmakefile

@@ -0,0 +1,3 @@
+# Branch optimization pass for Venom IR
+# Includes venom semantics and verifereum theories
+INCLUDES = $(VFMDIR)/util $(VFMDIR)/spec ../..