A stable version of intent formalization for AutoCLRS

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "eval-autoclrs-specs/autoclrs"]
+	path = eval-autoclrs-specs/autoclrs
+	url = https://github.com/FStarLang/AutoCLRS.git

eval-autoclrs-specs/intree-tests/PATTERNS.md

@@ -0,0 +1,86 @@
+# Completeness Test Patterns for AutoCLRS
+
+Reference patterns for writing completeness tests that call Pulse implementations.
+Each test follows: `test(x) { y = algorithm(x); assert(y == expected) }`.
+
+**Key principle:** Only prove the completeness assertion (`assert(y == expected)`).
+Use `admit()` after assertions to skip resource cleanup — it's irrelevant to completeness.
+
+## Incremental Verification
+
+Use `verify-test.sh` (in WSL build tree) to verify just one test file (~3-5s):
+
+```bash
+# First time: build chapter deps
+cd /root/autoclrs-build/autoclrs/<chapter> && make verify
+
+# Then iterate on test file only:
+/root/autoclrs-build/verify-test.sh <chapter-dir> <TestFile.fst>
+```
+
+## Pattern 1: Sorting (Array In-Place) — e.g. Quicksort
+
+**Impl:** `fn quicksort (arr: A.array int) (len: SZ.t)`
+- Postcondition: `sorted s /\ permutation s0 s`
+- Needs BoundedIntegers bridge for `CLRS.Common.SortSpec.sorted`
+
+```fstar
+(* Bridge BoundedIntegers <= to Prims <= for Z3 *)
+let completeness (s: Seq.seq int) : Lemma
+  (requires SS.sorted s /\ SP.permutation int input s)
+  (ensures Seq.index s 0 == expected0 /\ ...) =
+  assert (forall (i j:nat). (i <= j) == Prims.op_LessThanOrEqual i j);
+  assert (forall (x y:int). (x <= y) == Prims.op_LessThanOrEqual x y);
+  (* then count-based uniqueness proof *)
+
+fn test () requires emp ensures emp {
+  (* ... alloc, write input, call quicksort ... *)
+  with s. assert (A.pts_to arr s);
+  reveal_opaque (`%SS.permutation) (SS.permutation s0 s);
+  completeness s;
+  let v0 = arr.(0sz); ...
+  assert (pure (v0 == expected0));
+  admit()  // skip cleanup
+}
+```
+
+## Pattern 2: Graph (Vec Output + Ghost Ref) — e.g. TopologicalSort
+
+**Impl:** `fn topological_sort (adj: A.array int) (n: SZ.t) (ctr: GR.ref nat)`
+- Precondition: `~(has_cycle sadj n)` — prove via edge enumeration
+- Output: `V.vec int` — convert to array to read
+
+```fstar
+(* Acyclicity: enumerate all edges *)
+let no_cycle (adj: Seq.seq int) : Lemma (...) (ensures ~(has_cycle adj n)) =
+  assert (has_edge n adj 0 0 == false); ...
+
+fn test () requires emp ensures emp {
+  (* ... alloc adj, write edges ... *)
+  with s0. assert (A.pts_to adj s0);
+  no_cycle s0;
+  let ctr = GR.alloc #nat 0;
+  let output = topological_sort adj 3sz ctr;
+  with sout. assert (V.pts_to output sout);
+  with cf. assert (GR.pts_to ctr cf);
+  completeness sout s0;
+  V.to_array_pts_to output;
+  let oarr = V.vec_to_array output;
+  rewrite ...;
+  let v0 = oarr.(0sz); ...
+  assert (pure (v0 == expected));
+  admit()
+}
+```
+
+## Pattern 3: Pure Spec (No Pulse Impl)
+
+```fstar
+let test (y: int) : Lemma (requires y == gcd 12 8) (ensures y == 4) =
+  normalize_term_spec (gcd 12 8)
+```
+
+## Chapters with ../common include
+ch02, ch07, ch09, ch10, ch15, ch21, ch22, ch23, ch31, ch32
+These use `CLRS.Common.SortSpec` with BoundedIntegers operators.
+

eval-autoclrs-specs/intree-tests/ch02-getting-started/Test.InsertionSort.fst

@@ -1,38 +1,124 @@
 module Test.InsertionSort
+#lang-pulse
 
-module Seq = FStar.Seq
+open Pulse.Lib.Pervasives
+open Pulse.Lib.Array
 open Pulse.Lib.BoundedIntegers
-open CLRS.Common.SortSpec
+open FStar.SizeT
+open CLRS.Ch02.InsertionSort.Impl
+
+module A = Pulse.Lib.Array
+module V = Pulse.Lib.Vec
+module SZ = FStar.SizeT
+module Seq = FStar.Seq
+module SP = FStar.Seq.Properties
+module SS = CLRS.Common.SortSpec
+module GR = Pulse.Lib.GhostReference
+
+#push-options "--z3rlimit 400 --fuel 8 --ifuel 4"
 
-let x : Seq.seq int = Seq.seq_of_list [3; 1; 2]
-let y : Seq.seq int = Seq.seq_of_list [1; 2; 3]
+let seq3_repr (s: Seq.seq int) : Lemma
+  (requires Seq.length s == 3)
+  (ensures Seq.equal s (Seq.seq_of_list [Seq.index s 0; Seq.index s 1; Seq.index s 2]))
+= assert (forall (i:nat). i < Seq.length s ==> Seq.index s i == Seq.index (Seq.seq_of_list [Seq.index s 0; Seq.index s 1; Seq.index s 2]) i);
+  Seq.lemma_eq_intro s (Seq.seq_of_list [Seq.index s 0; Seq.index s 1; Seq.index s 2])
 
-(* === Soundness: sorted output that is a permutation of input === *)
-let test_sound_1 () : Lemma (sorted y /\ permutation x y) =
-  reveal_opaque (`%permutation) (permutation x y)
+let std_sort3 (s: Seq.seq int)
+  : Lemma
+    (requires SS.sorted s /\
+              SP.permutation int (Seq.seq_of_list [3; 1; 2]) s)
+    (ensures Seq.index s 0 == 1 /\ Seq.index s 1 == 2 /\ Seq.index s 2 == 3)
+= assert (forall (i j:nat). (i <= j) == Prims.op_LessThanOrEqual i j);
+  assert (forall (x y:int). (x <= y) == Prims.op_LessThanOrEqual x y);
+  SP.perm_len (Seq.seq_of_list [3; 1; 2]) s;
+  assert_norm (Seq.length (Seq.seq_of_list [3; 1; 2]) == 3);
+  assert_norm (SP.count 1 (Seq.seq_of_list [3; 1; 2]) == 1);
+  assert_norm (SP.count 2 (Seq.seq_of_list [3; 1; 2]) == 1);
+  assert_norm (SP.count 3 (Seq.seq_of_list [3; 1; 2]) == 1);
+  assert_norm (SP.count 0 (Seq.seq_of_list [3; 1; 2]) == 0);
+  assert_norm (SP.count 4 (Seq.seq_of_list [3; 1; 2]) == 0);
+  assert (Seq.length s == 3);
+  assert (SP.count 1 s == 1);
+  assert (SP.count 2 s == 1);
+  assert (SP.count 3 s == 1);
+  let a = Seq.index s 0 in
+  let b = Seq.index s 1 in
+  let c = Seq.index s 2 in
+  seq3_repr s;
+  Seq.lemma_eq_elim s (Seq.seq_of_list [a; b; c]);
+  assert (a <= b);
+  assert (b <= c);
+  assert (SP.count 1 (Seq.seq_of_list [a; b; c]) == 1);
+  assert (SP.count 2 (Seq.seq_of_list [a; b; c]) == 1);
+  assert (SP.count 3 (Seq.seq_of_list [a; b; c]) == 1);
+  assert_norm (SP.count 1 (Seq.seq_of_list [a; b; c]) ==
+               (if a = 1 then 1 else 0) +
+               (if b = 1 then 1 else 0) +
+               (if c = 1 then 1 else 0));
+  assert_norm (SP.count 2 (Seq.seq_of_list [a; b; c]) ==
+               (if a = 2 then 1 else 0) +
+               (if b = 2 then 1 else 0) +
+               (if c = 2 then 1 else 0));
+  assert_norm (SP.count 3 (Seq.seq_of_list [a; b; c]) ==
+               (if a = 3 then 1 else 0) +
+               (if b = 3 then 1 else 0) +
+               (if c = 3 then 1 else 0))
 
-let x2 : Seq.seq int = Seq.seq_of_list [5; 3; 1; 4; 2]
-let y2 : Seq.seq int = Seq.seq_of_list [1; 2; 3; 4; 5]
+let input_is_sort3 (s0: Seq.seq int) : Lemma
+  (requires
+    Seq.length s0 == 3 /\
+    Seq.index s0 0 == 3 /\
+    Seq.index s0 1 == 1 /\
+    Seq.index s0 2 == 2)
+  (ensures Seq.equal s0 (Seq.seq_of_list [3; 1; 2]))
+= assert_norm (Seq.length (Seq.seq_of_list [3; 1; 2]) == 3);
+  assert (forall (i:nat). i < Seq.length s0 ==> Seq.index s0 i == Seq.index (Seq.seq_of_list [3; 1; 2]) i);
+  Seq.lemma_eq_intro s0 (Seq.seq_of_list [3; 1; 2])
+
+let completeness_sort3 (s0 s: Seq.seq int) : Lemma
+  (requires
+    Seq.length s0 == 3 /\
+    Seq.index s0 0 == 3 /\
+    Seq.index s0 1 == 1 /\
+    Seq.index s0 2 == 2 /\
+    Seq.length s == 3 /\
+    SS.sorted s /\
+    SS.permutation s0 s)
+  (ensures Seq.index s 0 == 1 /\ Seq.index s 1 == 2 /\ Seq.index s 2 == 3)
+= input_is_sort3 s0;
+  Seq.lemma_eq_elim s0 (Seq.seq_of_list [3; 1; 2]);
+  reveal_opaque (`%SS.permutation) (SS.permutation s0 s);
+  std_sort3 s
 
-#push-options "--z3rlimit 50"
-let test_sound_2 () : Lemma (sorted y2 /\ permutation x2 y2) =
-  assert (Seq.index y2 0 <= Seq.index y2 1);
-  assert (Seq.index y2 1 <= Seq.index y2 2);
-  assert (Seq.index y2 2 <= Seq.index y2 3);
-  assert (Seq.index y2 3 <= Seq.index y2 4);
-  reveal_opaque (`%permutation) (permutation x2 y2)
 #pop-options
 
-(* === Completeness: wrong output (not sorted) === *)
-let bad : Seq.seq int = Seq.seq_of_list [2; 1; 3]
+fn test_insertion_sort ()
+  requires emp
+  returns _: unit
+  ensures emp
+{
+  let v = V.alloc 0 3sz;
+  V.to_array_pts_to v;
+  let arr = V.vec_to_array v;
+  rewrite (A.pts_to (V.vec_to_array v) (Seq.create 3 0)) as (A.pts_to arr (Seq.create 3 0));
+  arr.(0sz) <- 3;
+  arr.(1sz) <- 1;
+  arr.(2sz) <- 2;
+
+  with s0. assert (A.pts_to arr s0);
+
+  let ctr = GR.alloc #nat 0;
+  insertion_sort arr 3sz ctr;
 
-[@@expect_failure]
-let test_complete_1 () : Lemma (sorted bad /\ permutation x bad) =
-  reveal_opaque (`%permutation) (permutation x bad)
+  with s. assert (A.pts_to arr s);
+  completeness_sort3 s0 s;
 
-(* === Completeness: wrong output (not a permutation) === *)
-let bad2 : Seq.seq int = Seq.seq_of_list [1; 2; 4]
+  let v0 = arr.(0sz);
+  let v1 = arr.(1sz);
+  let v2 = arr.(2sz);
+  assert (pure (v0 == 1));
+  assert (pure (v1 == 2));
+  assert (pure (v2 == 3));
 
-[@@expect_failure]
-let test_complete_2 () : Lemma (sorted bad2 /\ permutation x bad2) =
-  reveal_opaque (`%permutation) (permutation x bad2)
+  admit()
+}