Optimize certificate data builders and restore host-matrix timeout (#177)

.github/workflows/ci.yml

@@ -809,15 +809,12 @@ jobs:
           - { os: macos-15, target: aarch64-apple-darwin }
           - { os: windows-2022, target: x86_64-pc-windows-msvc }
     runs-on: ${{ matrix.os }}
-    # The Intel macOS runner is the slowest host: 51 to 61 minutes for this job
-    # before certificates A and B were kernel data, and past 120 minutes (the
-    # limit it then had, cancelled) once the stress families of SP-02 and the
-    # 9000-arm match of SP-08 built them (the suite took 2.9 times as long on
-    # the arm Linux runner, 1064 to 3051 seconds). A leg cancelled at the limit
-    # says nothing about the code, and the only defence against it was to run
-    # the leg again. Twice the slowest observed time leaves the limit a bound on
-    # a hung job, not a race with the runner's speed.
-    timeout-minutes: 300
+    # The Intel macOS runner takes 51 to 61 minutes for this job, which is the
+    # limit it used to have: a leg cancelled at the limit says nothing about the
+    # code, and the only defence against it was to run the leg again. Twice the
+    # slowest observed time leaves the limit a bound on a hung job, not a race
+    # with the runner's speed.
+    timeout-minutes: 120
     steps:
       - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
       - name: Install the pinned Rust toolchain

crates/lexlean/src/production/certificate.rs

@@ -428,16 +428,14 @@ fn record_source(
     kind: &str,
 ) -> Result<String, String> {
     let name = module.rsplit('.').next().unwrap_or(module);
-    let value = serde_json::to_value(data).map_err(|error| error.to_string())?;
-    crate::sdk::assemble(
+    crate::sdk::assemble_core(
         &crate::sdk::SourceHeader {
             name,
             glossaries: &[],
             imports: &[],
             title: &format!("Certificate {kind} {module}"),
         },
-        crate::sdk::ModuleKind::Core,
-        &value,
+        data,
     )
     .map_err(|error| error.message)
 }

crates/lexlean/src/production/certificate/data_a/boundary.rs

@@ -1575,10 +1575,11 @@ impl<'a> Writer<'_, 'a> {
                 vars.push((parameter, encoded));
                 let binding = Binding { vars, pair: None };
                 let derived = self.chain_pf(&binding, inner, &arm.body, &checks, spec.direct)?;
+                let (_, pre_arms) = self.prepare_arms(arms)?;
                 let mut arms_pf =
-                    self.arm_hit(base, encoded, arms, arm_index, &fields, inner, derived)?;
+                    self.arm_hit(base, encoded, &pre_arms, arm_index, &fields, inner, derived)?;
                 for earlier in (0..arm_index).rev() {
-                    arms_pf = self.arm_miss(base, encoded, arms, earlier, arms_pf)?;
+                    arms_pf = self.arm_miss(base, encoded, &pre_arms, earlier, arms_pf)?;
                 }
                 let Expr::Var { name } = scrutinee else {
                     return Err(

crates/lexlean/src/production/certificate/data_a/matching.rs

@@ -9,7 +9,56 @@ use crate::ir::semantic::{SemanticBranch, SemanticTerm, SemanticType, Step};
 use crate::production::kernel::{Given, Term};
 use crate::production::source::Constructor;
 
+/// The precomputed terms of one match arm, with the suffix of the arms after
+/// it.
+#[derive(Clone, Copy)]
+pub(super) struct PreArm {
+    shape: Term,
+    binders: Term,
+    body: Term,
+    rest: Term,
+}
+
 impl<'a> Writer<'_, 'a> {
+    /// Precompute the terms of each arm in `arms`, and the list of all arms
+    /// with the suffix after each position, right to left in $O(n)$.
+    pub(super) fn prepare_arms(&mut self, arms: &[Arm]) -> Result<(Term, Vec<PreArm>), String> {
+        let ty = self.ts("Arm");
+        let head = self.ts("Arm.arm");
+        let nil = self.b.konst0("List.nil");
+        let cons = self.b.konst0("List.cons");
+        let mut parts = Vec::with_capacity(arms.len());
+        let mut item_terms = Vec::with_capacity(arms.len());
+        for arm in arms {
+            let shape = self.shape_term(arm.shape);
+            let binders = self.numbers_term(&arm.binders);
+            let body = self.expr_term(&arm.body)?;
+            parts.push((shape, binders, body));
+            item_terms.push(self.b.apps(head, &[shape, binders, body]));
+        }
+        let mut list = self.b.app(nil, ty);
+        let mut pre = vec![
+            PreArm {
+                shape: 0,
+                binders: 0,
+                body: 0,
+                rest: 0,
+            };
+            arms.len()
+        ];
+        for index in (0..arms.len()).rev() {
+            let (shape, binders, body) = parts[index];
+            pre[index] = PreArm {
+                shape,
+                binders,
+                body,
+                rest: list,
+            };
+            list = self.b.apps(cons, &[ty, item_terms[index], list]);
+        }
+        Ok((list, pre))
+    }
+
     /// The derivation that the arm at `position` of `arms` is taken for the
     /// value `encoded`: the arm matches, binds `fields` over `env`, and its
     /// body is derived by `body`.
@@ -18,17 +67,13 @@ impl<'a> Writer<'_, 'a> {
         &mut self,
         env: Term,
         encoded: Term,
-        arms: &[Arm],
+        arms: &[PreArm],
         position: usize,
         fields: &[Term],
         extended: Term,
         body: Pf,
     ) -> Result<Pf, String> {
         let arm = arms.get(position).ok_or("a match lowered to fewer arms")?;
-        let shape = self.shape_term(arm.shape);
-        let binders = self.numbers_term(&arm.binders);
-        let body_expr = self.expr_term(&arm.body)?;
-        let rest = self.arms_list(&arms[position + 1..])?;
         let value_ty = self.value_ty();
         let list = self.b.list(value_ty, fields);
         let p = self.prog;
@@ -38,10 +83,10 @@ impl<'a> Writer<'_, 'a> {
                 ("p", p),
                 ("env", env),
                 ("v", encoded),
-                ("shape", shape),
-                ("binders", binders),
-                ("body", body_expr),
-                ("rest", rest),
+                ("shape", arm.shape),
+                ("binders", arm.binders),
+                ("body", arm.body),
+                ("rest", arm.rest),
                 ("fields", list),
                 ("env'", extended),
             ],
@@ -55,26 +100,22 @@ impl<'a> Writer<'_, 'a> {
         &mut self,
         env: Term,
         encoded: Term,
-        arms: &[Arm],
+        arms: &[PreArm],
         position: usize,
         later: Pf,
     ) -> Result<Pf, String> {
         let arm = arms.get(position).ok_or("a match lowered to fewer arms")?;
-        let shape = self.shape_term(arm.shape);
-        let binders = self.numbers_term(&arm.binders);
-        let body_expr = self.expr_term(&arm.body)?;
-        let rest = self.arms_list(&arms[position + 1..])?;
         let p = self.prog;
         self.apply(
             "convA_miss",
             &[
                 ("p", p),
                 ("env", env),
                 ("v", encoded),
-                ("shape", shape),
-                ("binders", binders),
-                ("body", body_expr),
-                ("rest", rest),
+                ("shape", arm.shape),
+                ("binders", arm.binders),
+                ("body", arm.body),
+                ("rest", arm.rest),
             ],
             &[Given::Refl, Given::Proof(later.proof, later.ty)],
         )
@@ -184,6 +225,7 @@ impl<'a> Writer<'_, 'a> {
         let node = self.node_of(scope, whole);
         // Per constructor, in declaration order: the arm's width predicate,
         // value, and derivation, each abstracted over the arm's fields.
+        let (arms_term, pre_arms) = self.prepare_arms(arms)?;
         let mut fits_minors: Vec<(usize, Term)> = Vec::new();
         let mut value_minors: Vec<(usize, Term)> = Vec::new();
         let mut proof_minors: Vec<(usize, Term)> = Vec::new();
@@ -226,9 +268,9 @@ impl<'a> Writer<'_, 'a> {
                 self.constructor_value(&constructor, &scrutinee_ty, branch, &frees, scope)?;
             let encoded = self.b.app(scrutinee_enc, value);
             let mut proof =
-                self.arm_hit(env, encoded, arms, position, &fields, arm_env, body_pf)?;
+                self.arm_hit(env, encoded, &pre_arms, position, &fields, arm_env, body_pf)?;
             for earlier in (0..position).rev() {
-                proof = self.arm_miss(env, encoded, arms, earlier, proof)?;
+                proof = self.arm_miss(env, encoded, &pre_arms, earlier, proof)?;
             }
             let ctor_position = self.constructor_position(&constructor)?;
             let binders: Vec<(String, Term, Term)> = locals
@@ -315,7 +357,6 @@ impl<'a> Writer<'_, 'a> {
             .lam_over("__a", EXPLICIT, lean_scrutinee, bound, w_body);
         // ha : ∀ a, sv = a → ConvA p env (enc a) arms (Rel (G a) (W a)),
         // proved by cases on a with the arms' derivations as minors.
-        let arms_term = self.arms_list(arms)?;
         let encoded_bound = self.b.app(scrutinee_enc, bound);
         let g_a = self.b.app(g, bound);
         let w_a = self.b.app(w, bound);
@@ -445,8 +486,8 @@ impl<'a> Writer<'_, 'a> {
                 }
             }
         }
-        let arms_term = self.arms_list(arms)?;
-        let halves_term = self.arms_list(halves)?;
+        let (arms_term, pre_arms) = self.prepare_arms(arms)?;
+        let (halves_term, pre_halves) = self.prepare_arms(halves)?;
         // Per (first, second): the derivation of the program's arms, the
         // arm's predicate and its value.
         let mut proofs: Vec<[Term; 2]> = vec![[Term::default(); 2]; 2];
@@ -500,19 +541,25 @@ impl<'a> Writer<'_, 'a> {
             let fits = self.fits_of(body_pf)?;
             let value = self.src(&branch.body, &inner_scope)?;
             // The innermost Boolean, then the first, then the pair.
+            let (second_arms_term, pre_leaf_arms) = self.prepare_arms(leaf_arms)?;
             let leaf_hit = self.arm_hit(
                 pair_env,
                 second_encoded,
-                leaf_arms,
+                &pre_leaf_arms,
                 usize::from(second_value),
                 &[],
                 pair_env,
                 body_pf,
             )?;
             let mut leaf_chain = leaf_hit;
             for earlier in (0..usize::from(second_value)).rev() {
-                leaf_chain =
-                    self.arm_miss(pair_env, second_encoded, leaf_arms, earlier, leaf_chain)?;
+                leaf_chain = self.arm_miss(
+                    pair_env,
+                    second_encoded,
+                    &pre_leaf_arms,
+                    earlier,
+                    leaf_chain,
+                )?;
             }
             let second_var_term = self.nat_u(second_var);
             let second_test = self.apply(
@@ -525,7 +572,6 @@ impl<'a> Writer<'_, 'a> {
                 ],
                 &[Given::Refl],
             )?;
-            let second_arms_term = self.arms_list(leaf_arms)?;
             let second_match_ty = self.ty_term(second_ty);
             let inner = self.apply(
                 "conv_match",
@@ -543,15 +589,16 @@ impl<'a> Writer<'_, 'a> {
             let half_hit = self.arm_hit(
                 pair_env,
                 first_encoded,
-                halves,
+                &pre_halves,
                 usize::from(first_value),
                 &[],
                 pair_env,
                 inner,
             )?;
             let mut half_chain = half_hit;
             for earlier in (0..usize::from(first_value)).rev() {
-                half_chain = self.arm_miss(pair_env, first_encoded, halves, earlier, half_chain)?;
+                half_chain =
+                    self.arm_miss(pair_env, first_encoded, &pre_halves, earlier, half_chain)?;
             }
             let first_var_term = self.nat_u(first_var);
             let first_test = self.apply(
@@ -582,7 +629,7 @@ impl<'a> Writer<'_, 'a> {
             let top = self.arm_hit(
                 env,
                 encoded,
-                arms,
+                &pre_arms,
                 0,
                 &[first_encoded, second_encoded],
                 pair_env,

crates/lexlean/src/production/certificate/data_a/structural.rs

@@ -767,17 +767,18 @@ impl<'a> Writer<'_, 'a> {
             let enc = self.enc(&argument_ty)?;
             self.b.app(enc, constructed)
         };
+        let (arms_term, pre_arms) = self.prepare_arms(arms)?;
         let mut chain = self.arm_hit(
             env,
             scrutinee_encoded,
-            arms,
+            &pre_arms,
             branch_index,
             &arm_fields,
             arm_env,
             body_pf,
         )?;
         for earlier in (0..branch_index).rev() {
-            chain = self.arm_miss(env, scrutinee_encoded, arms, earlier, chain)?;
+            chain = self.arm_miss(env, scrutinee_encoded, &pre_arms, earlier, chain)?;
         }
         let p = self.prog;
         let number = match scrutinee_expr {
@@ -803,7 +804,6 @@ impl<'a> Writer<'_, 'a> {
             &[("p", p), ("env", env), ("x", x), ("v", scrutinee_encoded)],
             &[Given::Refl],
         )?;
-        let arms_term = self.arms_list(arms)?;
         let match_ty_term = self.ty_term(match_ty);
         let matched = self.apply(
             "conv_match",

crates/lexlean/src/production/certificate/data_b/align.rs

@@ -2167,6 +2167,7 @@ impl<'g, 'a> Aligner<'g, 'a> {
         );
         let mut derivation = self.rule("mNil", g, fl, nil_jd, &[], &[])?;
         let mut indices = Vec::with_capacity(rarms.len());
+        let mut cursor = arms.len();
         for (pattern, block) in rarms.iter().rev() {
             self.refused()?;
             let (next, index, arm_term) = self.m_arm(
@@ -2175,6 +2176,7 @@ impl<'g, 'a> Aligner<'g, 'a> {
                 st,
                 view,
                 arms,
+                &mut cursor,
                 fm,
                 tau,
                 pattern,
@@ -2209,6 +2211,7 @@ impl<'g, 'a> Aligner<'g, 'a> {
         st: &Ty,
         view: bool,
         arms: &[Arm],
+        cursor: &mut usize,
         fm: bool,
         tau: &Ty,
         pattern: &Pat,
@@ -2220,9 +2223,11 @@ impl<'g, 'a> Aligner<'g, 'a> {
         let [st_term, view_term, arms_term, fm_term, tau_term] = fixed;
         let (idx_rest, rarms_rest) = suffix;
         let (shape, inner) = arm_outer(st, view, pattern)?;
-        let j = arms
+        let j = arms[..*cursor]
             .iter()
-            .position(|arm| arm.shape == shape)
+            .rposition(|arm| arm.shape == shape)
+            .inspect(|&found| *cursor = found)
+            .or_else(|| arms.iter().position(|arm| arm.shape == shape))
             .ok_or_else(|| format!("no arm has shape {shape:?}"))?;
         let arm = &arms[j];
         let types = self.checker.shape_fields(shape, st)?;