Centralize toolchain detection in config.mk; fix BFS postcondition order

nikswamy · Copilot · nikswamy · commit 0ec25a94cdc1 · 2026-04-19T08:43:15.000-07:00
Two fixes:

1. Build system: All 22 chapter Makefiles and autoclrs/Makefile now
   include a shared autoclrs/config.mk that detects binary install
   (fstar/) vs source build (FStar/) using absolute paths. This
   eliminates stale .checked files from PULSE_ROOT path mismatches
   when switching between top-level and standalone chapter builds.

2. BFS.Impl.fst: Reorder postcondition conjuncts (optimality before
   complexity) to match the .fsti interface, fixing a subtyping
   failure with F* 2026.04.17.

Co-authored-by: Copilot &lt;223556219+Copilot@users.noreply.github.com&gt;
diff --git a/autoclrs/Makefile b/autoclrs/Makefile
@@ -4,26 +4,11 @@
 #   make            # verify all chapters
 #   make -j8        # parallel build
 
-# Detect binary install (fstar/) vs source build (FStar/)
-ifneq ($(wildcard $(CURDIR)/../fstar/bin/fstar.exe),)
-  PULSE_ROOT ?= $(CURDIR)/../fstar/pulse
-  ifndef FSTAR_EXE
-    FSTAR_EXE := $(CURDIR)/../fstar/bin/fstar.exe
-  endif
-  KRML_HOME  ?= $(CURDIR)/../fstar/karamel
-else
-  PULSE_ROOT ?= ../FStar/pulse
-  ifndef FSTAR_EXE
-    FSTAR_EXE := $(CURDIR)/../FStar/out/bin/fstar.exe
-  endif
-endif
-STAGE3     ?= 1
+include config.mk
 export STAGE3
 export FSTAR_EXE
 export PULSE_ROOT
-ifdef KRML_HOME
 export KRML_HOME
-endif
 
 SUBDIRS += ch02-getting-started
 SUBDIRS += ch04-divide-conquer
diff --git a/autoclrs/ch02-getting-started/Makefile b/autoclrs/ch02-getting-started/Makefile
@@ -1,7 +1,4 @@
-PULSE_ROOT ?= ../../FStar/pulse
-STAGE3 ?= 1
-export STAGE3
-KRML_HOME ?= ../../FStar/karamel
+include ../config.mk
 OTHERFLAGS += --include ../common
 include $(PULSE_ROOT)/mk/test.mk
 
diff --git a/autoclrs/ch04-divide-conquer/Makefile b/autoclrs/ch04-divide-conquer/Makefile
@@ -1,14 +1,5 @@
-PULSE_ROOT ?= ../../FStar/pulse
-STAGE3     ?= 1
-export STAGE3
-ifndef FSTAR_EXE
-FSTAR_EXE  := $(realpath ../../FStar/out/bin/fstar.exe)
-endif
-export FSTAR_EXE
-
-KRML_HOME  ?= ../../FStar/karamel
+include ../config.mk
 KRML_EXE   ?= $(KRML_HOME)/krml
-
 include $(PULSE_ROOT)/mk/test.mk
 
 # ── C extraction and test targets ───────────────────────────────────────
diff --git a/autoclrs/ch06-heapsort/Makefile b/autoclrs/ch06-heapsort/Makefile
@@ -1,7 +1,4 @@
-PULSE_ROOT ?= ../../FStar/pulse
-STAGE3     ?= 1
-KRML_HOME  ?= ../../FStar/karamel
-export STAGE3
+include ../config.mk
 include $(PULSE_ROOT)/mk/test.mk
 
 # ── C extraction and test targets ──────────────────────────────────────
diff --git a/autoclrs/ch07-quicksort/Makefile b/autoclrs/ch07-quicksort/Makefile
@@ -1,7 +1,4 @@
-PULSE_ROOT ?= ../../FStar/pulse
-KRML_HOME  ?= ../../FStar/karamel
-STAGE3 ?= 1
-export STAGE3
+include ../config.mk
 OTHERFLAGS += --include ../common
 include $(PULSE_ROOT)/mk/test.mk
 
diff --git a/autoclrs/ch08-linear-sorting/Makefile b/autoclrs/ch08-linear-sorting/Makefile
@@ -1,7 +1,5 @@
-PULSE_ROOT ?= ../../FStar/pulse
-KRML_HOME  ?= ../../FStar/karamel
+include ../config.mk
 KRML_EXE   ?= $(KRML_HOME)/krml
-STAGE3     ?= 1
 include $(PULSE_ROOT)/mk/test.mk
 
 # ── C extraction and test targets ──────────────────────────────────
diff --git a/autoclrs/ch09-order-statistics/Makefile b/autoclrs/ch09-order-statistics/Makefile
@@ -1,5 +1,4 @@
-PULSE_ROOT ?= ../../FStar/pulse
-KRML_HOME  ?= ../../FStar/karamel
+include ../config.mk
 include $(PULSE_ROOT)/mk/test.mk
 OTHERFLAGS += --include ../common
 
diff --git a/autoclrs/ch10-elementary-ds/Makefile b/autoclrs/ch10-elementary-ds/Makefile
@@ -1,5 +1,4 @@
-PULSE_ROOT ?= ../../FStar/pulse
-KRML_HOME  ?= ../../FStar/karamel
+include ../config.mk
 include $(PULSE_ROOT)/mk/test.mk
 OTHERFLAGS += --include ../common
 
diff --git a/autoclrs/ch11-hash-tables/Makefile b/autoclrs/ch11-hash-tables/Makefile
@@ -1,5 +1,4 @@
-PULSE_ROOT ?= ../../FStar/pulse
-KRML_HOME  ?= ../../FStar/karamel
+include ../config.mk
 include $(PULSE_ROOT)/mk/test.mk
 
 # ── C extraction and test targets ──────────────────────────────────
diff --git a/autoclrs/ch12-bst/Makefile b/autoclrs/ch12-bst/Makefile
@@ -1,7 +1,4 @@
-PULSE_ROOT ?= ../../FStar/pulse
-KRML_HOME  ?= ../../FStar/karamel
-STAGE3     ?= 1
-export STAGE3
+include ../config.mk
 include $(PULSE_ROOT)/mk/test.mk
 
 # ── C extraction and test for Chapter 12 BSTs ──────────────────────
diff --git a/autoclrs/ch13-rbtree/Makefile b/autoclrs/ch13-rbtree/Makefile
@@ -1,8 +1,4 @@
-PULSE_ROOT ?= ../../FStar/pulse
-KRML_HOME  ?= ../../FStar/karamel
-STAGE3     ?= 1
-export STAGE3
-
+include ../config.mk
 include $(PULSE_ROOT)/mk/test.mk
 
 # ── C extraction and test targets ──────────────────────────────────
diff --git a/autoclrs/ch15-dynamic-programming/Makefile b/autoclrs/ch15-dynamic-programming/Makefile
@@ -1,6 +1,5 @@
-KRML_HOME  ?= ../../FStar/karamel
+include ../config.mk
 KRML_EXE   ?= $(KRML_HOME)/krml
-PULSE_ROOT ?= ../../FStar/pulse
 include $(PULSE_ROOT)/mk/test.mk
 OTHERFLAGS += --include ../common
 
diff --git a/autoclrs/ch16-greedy/Makefile b/autoclrs/ch16-greedy/Makefile
@@ -1,5 +1,4 @@
-PULSE_ROOT ?= ../../FStar/pulse
-KRML_HOME  ?= ../../FStar/karamel
+include ../config.mk
 KRML_EXE   ?= $(KRML_HOME)/krml
 include $(PULSE_ROOT)/mk/test.mk
 
diff --git a/autoclrs/ch21-disjoint-sets/Makefile b/autoclrs/ch21-disjoint-sets/Makefile
@@ -1,7 +1,4 @@
-PULSE_ROOT ?= ../../FStar/pulse
-KRML_HOME  ?= ../../FStar/karamel
-STAGE3     ?= 1
-export STAGE3
+include ../config.mk
 OTHERFLAGS += --include ../common
 include $(PULSE_ROOT)/mk/test.mk
 
diff --git a/autoclrs/ch22-elementary-graph/CLRS.Ch22.BFS.Impl.fst b/autoclrs/ch22-elementary-graph/CLRS.Ch22.BFS.Impl.fst
@@ -1441,12 +1441,12 @@ fn queue_bfs
         Seq.index spred' v >= 0 /\ Seq.index spred' v < SZ.v n ==>
         Seq.index scolor' (Seq.index spred' v) <> 0 /\
         Seq.index sdist' v == Seq.index sdist' (Seq.index spred' v) + 1) /\
-      // Complexity: at most 2 * n² ticks
-      cf >= reveal c0 /\
-      cf - reveal c0 <= 2 * (SZ.v n * SZ.v n) /\
       // Shortest-path optimality: dist[w] is optimal for every reachable vertex
       (forall (w: nat) (k: nat). w < SZ.v n /\ reachable_in sadj (SZ.v n) (SZ.v source) w k ==>
-        Seq.index sdist' w <= k)
+        Seq.index sdist' w <= k) /\
+      // Complexity: at most 2 * n² ticks
+      cf >= reveal c0 /\
+      cf - reveal c0 <= 2 * (SZ.v n * SZ.v n)
     )
 //SNIPPET_END: queue_bfs_sig
 {
diff --git a/autoclrs/ch22-elementary-graph/Makefile b/autoclrs/ch22-elementary-graph/Makefile
@@ -1,6 +1,4 @@
-PULSE_ROOT ?= ../../FStar/pulse
-KRML_HOME  ?= ../../FStar/karamel
-STAGE3     ?= 1
+include ../config.mk
 include $(PULSE_ROOT)/mk/test.mk
 OTHERFLAGS += --include ../common
 
diff --git a/autoclrs/ch23-mst/Makefile b/autoclrs/ch23-mst/Makefile
@@ -1,5 +1,4 @@
-PULSE_ROOT ?= ../../FStar/pulse
-KRML_HOME  ?= ../../FStar/karamel
+include ../config.mk
 include $(PULSE_ROOT)/mk/test.mk
 OTHERFLAGS += --include ../common
 
diff --git a/autoclrs/ch24-sssp/Makefile b/autoclrs/ch24-sssp/Makefile
@@ -1,5 +1,4 @@
-PULSE_ROOT ?= ../../FStar/pulse
-KRML_HOME  ?= ../../FStar/karamel
+include ../config.mk
 OTHERFLAGS += --split_queries always
 include $(PULSE_ROOT)/mk/test.mk
 
diff --git a/autoclrs/ch25-apsp/Makefile b/autoclrs/ch25-apsp/Makefile
@@ -1,6 +1,4 @@
-PULSE_ROOT ?= ../../FStar/pulse
-KRML_HOME  ?= ../../FStar/karamel
-
+include ../config.mk
 include $(PULSE_ROOT)/mk/test.mk
 
 # ── C extraction and test targets ──────────────────────────────────
diff --git a/autoclrs/ch26-max-flow/Makefile b/autoclrs/ch26-max-flow/Makefile
@@ -1,6 +1,4 @@
-PULSE_ROOT ?= ../../FStar/pulse
-STAGE3     ?= 1
-KRML_HOME  ?= ../../FStar/karamel
+include ../config.mk
 include $(PULSE_ROOT)/mk/test.mk
 
 # ========== C extraction and test targets for ImplTest ==========
diff --git a/autoclrs/ch31-number-theory/Makefile b/autoclrs/ch31-number-theory/Makefile
@@ -1,5 +1,4 @@
-PULSE_ROOT ?= ../../FStar/pulse
-KRML_HOME  ?= ../../FStar/karamel
+include ../config.mk
 OTHERFLAGS += --include ../common
 include $(PULSE_ROOT)/mk/test.mk
 
diff --git a/autoclrs/ch32-string-matching/Makefile b/autoclrs/ch32-string-matching/Makefile
@@ -1,5 +1,4 @@
-PULSE_ROOT ?= ../../FStar/pulse
-KRML_HOME  ?= ../../FStar/karamel
+include ../config.mk
 include $(PULSE_ROOT)/mk/test.mk
 OTHERFLAGS += --include ../common
 
diff --git a/autoclrs/ch33-comp-geometry/Makefile b/autoclrs/ch33-comp-geometry/Makefile
@@ -1,5 +1,4 @@
-PULSE_ROOT ?= ../../FStar/pulse
-KRML_HOME  ?= ../../FStar/karamel
+include ../config.mk
 include $(PULSE_ROOT)/mk/test.mk
 
 # ── C extraction and test targets ──────────────────────────────────
diff --git a/autoclrs/ch35-approximation/Makefile b/autoclrs/ch35-approximation/Makefile
@@ -1,7 +1,4 @@
-PULSE_ROOT ?= ../../FStar/pulse
-KRML_HOME  ?= ../../FStar/karamel
-STAGE3     ?= 1
-
+include ../config.mk
 include $(PULSE_ROOT)/mk/test.mk
 
 # ── C extraction and test targets ──────────────────────────────────
diff --git a/autoclrs/common/Makefile b/autoclrs/common/Makefile
@@ -1,2 +1,2 @@
-PULSE_ROOT ?= ../../FStar/pulse
+include ../config.mk
 include $(PULSE_ROOT)/mk/test.mk
diff --git a/autoclrs/config.mk b/autoclrs/config.mk
@@ -0,0 +1,28 @@
+# autoclrs/config.mk — Shared toolchain detection for all chapter Makefiles
+#
+# Usage: include this file BEFORE including $(PULSE_ROOT)/mk/test.mk
+#   From chapter dirs:  include ../config.mk
+#   From autoclrs/:     include config.mk
+#
+# Detects binary install (fstar/) vs source build (FStar/) and sets:
+#   PULSE_ROOT, FSTAR_EXE, KRML_HOME, STAGE3
+
+_CONFIG_MK_DIR := $(dir $(lastword $(MAKEFILE_LIST)))
+_REPO_ROOT     := $(abspath $(_CONFIG_MK_DIR)/..)
+
+ifneq ($(wildcard $(_REPO_ROOT)/fstar/bin/fstar.exe),)
+  # Binary install
+  PULSE_ROOT ?= $(_REPO_ROOT)/fstar/pulse
+  ifndef FSTAR_EXE
+    FSTAR_EXE := $(_REPO_ROOT)/fstar/bin/fstar.exe
+  endif
+  KRML_HOME  ?= $(_REPO_ROOT)/fstar/karamel
+else
+  # Source build
+  PULSE_ROOT ?= $(_REPO_ROOT)/FStar/pulse
+  ifndef FSTAR_EXE
+    FSTAR_EXE := $(_REPO_ROOT)/FStar/out/bin/fstar.exe
+  endif
+  KRML_HOME  ?= $(_REPO_ROOT)/FStar/karamel
+endif
+STAGE3     ?= 1
