CakeML · talsewell · Feb 12, 2026 · Mar 3, 2026 · Mar 4, 2026 · Jan 27, 2026
diff --git a/basis/Holmakefile b/basis/Holmakefile
@@ -1,7 +1,7 @@
 INCLUDES = $(CAKEMLDIR)/developers $(CAKEMLDIR)/misc\
 					 $(CAKEMLDIR)/semantics $(CAKEMLDIR)/characteristic\
 					 $(CAKEMLDIR)/translator $(CAKEMLDIR)/translator/monadic\
-					 $(CAKEMLDIR)/compiler/printing  pure
+					 $(CAKEMLDIR)/compiler/printing  pure monadic
 
 all: $(DEFAULT_TARGETS) README.md basis_ffi.o
 .PHONY: all

diff --git a/basis/ListProgScript.sml b/basis/ListProgScript.sml
@@ -6,6 +6,7 @@ Ancestors
   mergesort std_prelude mllist ml_translator OptionProg
 Libs
   preamble ml_translatorLib ml_progLib cfLib basisFunctionsLib
+  ml_monad_translator_interfaceLib
 
 val _ = translation_extends "OptionProg"
 
@@ -339,6 +340,14 @@ val result = translate LUPDATE_eq;
 val _ = (next_ml_names := ["compare"]);
 val _ = translate mllistTheory.list_compare_def;
 
+(* Translation of conventional merge-sort.
+
+ * This is also List.sort, but is given the "mergesort" name too.
+
+ * (The mergesort name was used in an experiment to allow the Candle kernel
+ * to specifically request this sort, and not an array-based alternative whose
+ * use of stateful features clashes with the Candle proofs.)
+ *)
 val _ = ml_prog_update open_local_block;
 
 val result = translate sort2_tail_def;
@@ -347,6 +356,7 @@ val result = translate REV_DEF;
 val result = translate merge_tail_def;
 val result = translate DIV2_def;
 val result = translate DROP_def;
+
 val result = translate_no_ind mergesortN_tail_def;
 
 Theorem mergesortn_tail_ind[local]:
@@ -391,11 +401,15 @@ val result = translate mergesort_tail_def
 
 val _ = ml_prog_update open_local_in_block;
 
+val _ = next_ml_names := ["mergesort"];
+val result = translate mergesort_def;
+
 val _ = next_ml_names := ["sort"];
 
-val result = translate sort_def;
+val sort_v_thm = mllistTheory.sort_thm |> translate;
 
 val _ =  ml_prog_update close_local_blocks;
+
 val _ =  ml_prog_update (close_module NONE);
 
 (* finite maps -- depend on lists *)

diff --git a/basis/README.md b/basis/README.md
@@ -149,6 +149,9 @@ Logical model of filesystem and I/O streams
 [mlbasicsProgScript.sml](mlbasicsProgScript.sml):
 Translates a variety of basic constructs.
 
+[monadic](monadic):
+Monadic definitions of stateful functions used in the basis
+
 [pure](pure):
 HOL definitions of the pure functions used in the CakeML basis.
 

diff --git a/basis/monadic/Holmakefile b/basis/monadic/Holmakefile
@@ -0,0 +1,14 @@
+INCLUDES = $(CAKEMLDIR)/misc \
+    $(CAKEMLDIR)/translator/monadic/ $(CAKEMLDIR)/translator/
+
+all: $(DEFAULT_TARGETS) README.md
+.PHONY: all
+
+README_SOURCES = $(wildcard *Script.sml) $(wildcard *Lib.sml) $(wildcard *Syntax.sml)
+DIRS = $(wildcard */)
+README.md: $(CAKEMLDIR)/developers/readme_gen readmePrefix $(patsubst %,%readmePrefix,$(DIRS)) $(README_SOURCES)
+	$(CAKEMLDIR)/developers/readme_gen $(README_SOURCES)
+
+ifdef POLY
+HOLHEAP = $(CAKEMLDIR)/misc/cakeml-heap
+endif
diff --git a/basis/monadic/README.md b/basis/monadic/README.md
@@ -0,0 +1,16 @@
+Monadic definitions of stateful functions used in the basis
+
+These functions are generated and verified using a monad type, and are then
+translated to imperative CakeML code by the monadic translator.
+
+[heap_list_sort_monadicScript.sml](heap_list_sort_monadicScript.sml):
+Monadic variants of the heap-list sort functions, and proofs of equivalence.
+
+[heap_list_sort_translationScript.sml](heap_list_sort_translationScript.sml):
+Post-translation of heap_list_sort
+
+[merge_run_sort_monadicScript.sml](merge_run_sort_monadicScript.sml):
+Monadic variants of the merge-run-sort functions, and proofs of equivalence.
+
+[merge_run_sort_translationScript.sml](merge_run_sort_translationScript.sml):
+Post-translation of merge_run_sort
diff --git a/basis/monadic/readmePrefix b/basis/monadic/readmePrefix
@@ -0,0 +1,4 @@
+Monadic definitions of stateful functions used in the basis
+
+These functions are generated and verified using a monad type, and are then
+translated to imperative CakeML code by the monadic translator.
diff --git a/basis/pure/README.md b/basis/pure/README.md
@@ -6,6 +6,12 @@ from these by the translator.
 [basis_cvScript.sml](basis_cvScript.sml):
 Translation of basis types and functions for use with cv_compute.
 
+[heap_list_sortScript.sml](heap_list_sortScript.sml):
+A heap-sort variant that builds a list of exactly-balanced heaps.
+
+[merge_run_sortScript.sml](merge_run_sortScript.sml):
+Verified run-finding (natural) merge sort.
+
 [mlintScript.sml](mlintScript.sml):
 Pure functions for the Int module.
 

diff --git a/basis/pure/mllistScript.sml b/basis/pure/mllistScript.sml
@@ -277,6 +277,10 @@ Proof
 QED
 (* ^^^^^ TO BE PORTED TO HOL ^^^^^ *)
 
+Definition mergesort_def:
+  mergesort = mergesort$mergesort_tail
+End
+
 Definition sort_def:
   sort = mergesort$mergesort_tail
 End
@@ -287,26 +291,31 @@ Proof
   rw[sort_def]
 QED
 
-Theorem sort_SORTED:
-  !R L. transitive R ∧ total R ==> sorting$SORTED R (sort R L)
+Theorem total_reflexive[local]:
+  total R ==> reflexive R
 Proof
-  simp[sort_def, mergesort_tail_def, mergesortN_correct, mergesortN_sorted]
+  simp [total_def, reflexive_def]
+  \\ metis_tac []
 QED
 
-Theorem sort_MEM[simp]:
-  !R L. MEM x (sort R L) ⇔ MEM x L
+Theorem sort_SORTED:
+  !R L. transitive R ∧ total R ==> sorting$SORTED R (sort R L)
 Proof
-  simp[sort_def, mergesort_tail_MEM]
+  simp [mergesort_tail_correct, sort_def, mergesort_sorted]
 QED
 
 Theorem sort_PERM:
   !R L. sorting$PERM L (sort R L)
 Proof
-  simp[sort_def, mergesort_tail_def]
-  \\ rpt strip_tac
-  \\ `L = TAKE (LENGTH L) L` by rw[]
-  \\ pop_assum (fn x => pure_rewrite_tac [Once $ x])
-  \\ rw[mergesortN_tail_PERM]
+  rw [sort_def, mergesort_tail_def]
+  \\ irule PERM_TRANS \\ irule_at Any mergesortN_tail_PERM
+  \\ simp []
+QED
+
+Theorem sort_MEM[simp]:
+  !R L. MEM x (sort R L) ⇔ MEM x L
+Proof
+  metis_tac [sort_PERM, PERM_MEM_EQ]
 QED
 
 Theorem sort_LENGTH[simp]:

diff --git a/candle/overloading/monadic/holKernelProofScript.sml b/candle/overloading/monadic/holKernelProofScript.sml
@@ -1684,31 +1684,50 @@ Proof
   \\ IMP_RES_TAC TERM_Var \\ FULL_SIMP_TAC std_ss [pred_setTheory.IN_UNION]
 QED
 
-Theorem sort_type_vars_in_term:
-  (sort $<= (MAP explode (type_vars_in_term P)) = STRING_SORT (MAP explode (tvars P)))
+Overload candle_sort[local] = ``mllist$mergesort``
+
+Theorem string_le_ok[local]:
+  total string_le /\ antisymmetric string_le /\ transitive string_le
 Proof
-  REPEAT STRIP_TAC \\
-  MATCH_MP_TAC (MP_CANON sortingTheory.SORTED_PERM_EQ) \\
-  qexists_tac`$<=` >>
-  conj_asm1_tac >- (
-    simp[relationTheory.transitive_def,relationTheory.antisymmetric_def,stringTheory.string_le_def] >>
-    METIS_TAC[stringTheory.string_lt_antisym,stringTheory.string_lt_trans] ) >>
-  conj_tac >- (
-    MATCH_MP_TAC sort_SORTED >>
-    simp[relationTheory.total_def,stringTheory.string_le_def] >>
-    METIS_TAC[stringTheory.string_lt_cases] ) >>
-  conj_tac >- (
+  simp[relationTheory.total_def, relationTheory.transitive_def,
+    relationTheory.antisymmetric_def, stringTheory.string_le_def] >>
+  METIS_TAC[stringTheory.string_lt_cases, stringTheory.string_lt_antisym,
+    stringTheory.string_lt_trans]
+QED
+
+Theorem candle_sort_ok[local]:
+  SORTED string_le (candle_sort string_le xs) /\
+  (PERM (candle_sort string_le xs) ys = PERM xs ys)
+Proof
+  simp [mllistTheory.mergesort_def, mergesortTheory.mergesort_tail_correct,
+    string_le_ok, mergesortTheory.mergesort_sorted]
+  \\ metis_tac [mergesortTheory.mergesort_perm, sortingTheory.PERM_TRANS,
+        sortingTheory.PERM_SYM]
+QED
+
+Theorem LENGTH_candle_sort[local]:
+  LENGTH (candle_sort string_le xs) = LENGTH xs
+Proof
+  irule sortingTheory.PERM_LENGTH
+  \\ simp [candle_sort_ok]
+QED
+
+Theorem candle_sort_type_vars_in_term[local]:
+  TERM defs P ==>
+    (candle_sort $<= (MAP explode (type_vars_in_term P)) = STRING_SORT (MAP explode (tvars P)))
+Proof
+  rw []
+  \\ irule sortingTheory.SORTED_PERM_EQ
+  \\ irule_at Any (hd (BODY_CONJUNCTS candle_sort_ok))
+  \\ simp [string_le_ok, candle_sort_ok]
+  \\ reverse conj_tac >- (
     MATCH_MP_TAC sortingTheory.SORTED_weaken >>
     qexists_tac`$<` >>
     simp[STRING_SORT_SORTED,stringTheory.string_le_def] ) >>
-  MATCH_MP_TAC (MP_CANON sortingTheory.PERM_ALL_DISTINCT) >>
-  conj_tac >- (
-    METIS_TAC[sortingTheory.ALL_DISTINCT_PERM
-             ,sort_PERM
-             ,ALL_DISTINCT_type_vars_in_term
-             ,ALL_DISTINCT_MAP_explode] ) >>
-  simp[ALL_DISTINCT_STRING_SORT] >>
-  METIS_TAC[MEM_type_vars_in_term,MEM_MAP]
+     irule sortingTheory.PERM_ALL_DISTINCT
+  \\ simp [ALL_DISTINCT_MAP_explode, ALL_DISTINCT_type_vars_in_term]
+  \\ simp [MEM_MAP]
+  \\ metis_tac [MEM_type_vars_in_term]
 QED
 
 (* ------------------------------------------------------------------------- *)
@@ -3545,7 +3564,7 @@ Proof
   impl_tac >- METIS_TAC[STATE_def,TERM_Comb,THM] >>
   simp[] >> disch_then kall_tac >>
   simp[Once st_ex_bind_def] >>
-  Q.PAT_ABBREV_TAC`vs:string list = sort R X` >>
+  Q.PAT_ABBREV_TAC`vs:string list = candle_sort R X` >>
   simp[add_type_def,can_def,otherwise_def,st_ex_return_def] >>
   ntac 2 (simp[Once st_ex_bind_def]) >>
   simp[Once st_ex_bind_def,get_the_type_constants_def] >>
@@ -3556,6 +3575,7 @@ Proof
   `get_type_arity tyname s1 = (M_success (LENGTH vs), s1)` by (
     simp[get_type_arity_def,st_ex_bind_def,Abbr`s1`] >>
     simp[Abbr`vs`]>>
+    simp[LENGTH_candle_sort]>>
     EVAL_TAC)>>
   simp[mk_type_def,try_def,otherwise_def,raise_Fail_def,st_ex_return_def,Once st_ex_bind_def] >>
   simp[mk_fun_ty_def] >>
@@ -3601,12 +3621,10 @@ Proof
       rfs[TERM_def] >> METIS_TAC[]) >>
     imp_res_tac THM >> rfs[TERM_Comb] >>
     imp_res_tac THM_term_ok_bool >>
-    fs[term_ok_def,sort_type_vars_in_term] >>
+    fs[term_ok_def, candle_sort_type_vars_in_term] >>
     rfs[WELLTYPED] >>
     simp[Abbr`s2`,Abbr`s1`,Abbr`vs`,Abbr`l1`] >>
-    CONJ_TAC >- (
-      qspec_then ‘P’ (mp_tac o Q.AP_TERM ‘LENGTH’) (GEN_ALL sort_type_vars_in_term) >>
-      simp[sort_LENGTH])>>
+    fsrw_tac [SFY_ss] [candle_sort_type_vars_in_term, sort_LENGTH] >>
     METIS_TAC[term_type]) >>
   qmatch_assum_abbrev_tac`Abbrev(l1 = [(absname,absty);(repname,repty)])` >>
   `mk_const (repname,[]) s2 = (M_success (Const repname repty), s2)` by (
@@ -3782,15 +3800,16 @@ Proof
     \\ conj_tac
     >- METIS_TAC[STATE_def,CONTEXT_def,extends_theory_ok,init_theory_ok]
     \\ simp [Abbr`s2`,conexts_of_upd_def]
-    \\ imp_res_tac sort_type_vars_in_term
-    \\ simp [equation_def,Abbr`vs`,MAP_MAP_o,combinTheory.o_DEF,ETA_AX,sort_type_vars_in_term])
+    \\ imp_res_tac candle_sort_type_vars_in_term
+    \\ simp [equation_def,Abbr`vs`,MAP_MAP_o,combinTheory.o_DEF,ETA_AX])
   \\ conj_tac
   >-
    (match_mp_tac (List.nth(CONJUNCTS proves_rules,9))
     \\ conj_tac
     >- METIS_TAC[STATE_def,CONTEXT_def,extends_theory_ok,init_theory_ok]
     \\ simp [Abbr`s2`,conexts_of_upd_def]
-    \\ simp [sort_type_vars_in_term,equation_def,Abbr`vs`,MAP_MAP_o,combinTheory.o_DEF,ETA_AX])
+    \\ fsrw_tac [SFY_ss] [candle_sort_type_vars_in_term]
+    \\ simp [equation_def,Abbr`vs`,MAP_MAP_o,combinTheory.o_DEF,ETA_AX])
   \\ Cases
   \\ once_rewrite_tac [THM_def]
   \\ strip_tac

diff --git a/candle/overloading/monadic/holKernelScript.sml b/candle/overloading/monadic/holKernelScript.sml
@@ -1347,7 +1347,7 @@ Definition new_basic_type_definition_def:
     do (P,x) <- try dest_comb c (strlit "new_basic_type_definition: Not a combination") ;
     if ~(freesin [] P) then
       failwith (strlit "new_basic_type_definition: Predicate is not closed") else
-    let tyvars = MAP Tyvar (MAP implode (sort string_le (MAP explode (type_vars_in_term P)))) in
+    let tyvars = MAP Tyvar (MAP implode (mergesort string_le (MAP explode (type_vars_in_term P)))) in
     do rty <- type_of x ;
        add_type (tyname, LENGTH tyvars) ;
        aty <- mk_type(tyname,tyvars) ;

diff --git a/candle/prover/candle_kernel_permsScript.sml b/candle/prover/candle_kernel_permsScript.sml
@@ -133,10 +133,10 @@ Proof
   \\ rw[]
 QED
 
-Theorem perms_ok_sort_v[simp]:
-  perms_ok ps ListProg$sort_v
+Theorem perms_ok_mergesort_v[simp]:
+  perms_ok ps ListProg$mergesort_v
 Proof
-  rw[perms_ok_def, ListProgTheory.sort_v_def, astTheory.pat_bindings_def, perms_ok_env_def]
+  rw[perms_ok_def, ListProgTheory.mergesort_v_def, astTheory.pat_bindings_def, perms_ok_env_def]
   \\ pop_assum mp_tac \\ eval_nsLookup_tac
   \\ rw[]
 QED