cli: the precomputed-tree cache's posture follows the host target (W3 block)

LFM_PRECOMPUTED_TREE_CACHE_CAP, when the environment leaves it unset, is
set by the CLI's posture from the host target (block_whir's spill target):
64 entries (about 6.2 GiB once full) from a 64 GiB target up, 16 below it,
as #1013's CLI does (49c4bb5). A miss only rebuilds a tree whose root is
the key, so nothing moves in a proof. The BLOCK POSTURE line compares the
knob against the same rule, and a note says when the posture set 16.

Author: MauroToscano

bin/cli/src/main.rs

@@ -490,23 +490,43 @@ fn main() -> ExitCode {
 }
 
 /// What the posture does in an environment: the knobs it sets (each posture
-/// knob the environment leaves unset) and the ones the environment already
-/// sets.
+/// knob the environment leaves unset), the ones the environment already sets,
+/// and notes on the knobs it set to something other than the table's value.
 struct PosturePlan {
     set: Vec<(&'static str, &'static str)>,
     env: Vec<String>,
+    notes: Vec<String>,
 }
 
-fn posture_plan(env: impl Fn(&str) -> Option<String>) -> PosturePlan {
+/// The posture against the environment `env` and the host `target` (bytes):
+/// the precomputed-tree cache's cap follows the target
+/// ([`prover::lfm::whir_block_tree::posture_tree_cache_cap`]).
+fn posture_plan(env: impl Fn(&str) -> Option<String>, target: impl Fn() -> u64) -> PosturePlan {
+    use prover::lfm::whir_block_tree::{POSTURE, POSTURE_TREE_CACHE_KNOB, posture_tree_cache_cap};
     let mut plan = PosturePlan {
         set: Vec::new(),
         env: Vec::new(),
+        notes: Vec::new(),
     };
-    for &(name, value) in prover::lfm::whir_block_tree::POSTURE {
-        match env(name) {
-            Some(v) => plan.env.push(format!("{name}={v}")),
-            None => plan.set.push((name, value)),
+    for &(name, value) in POSTURE {
+        if let Some(v) = env(name) {
+            plan.env.push(format!("{name}={v}"));
+            continue;
+        }
+        if name == POSTURE_TREE_CACHE_KNOB {
+            let target = target();
+            let cap = posture_tree_cache_cap(target);
+            if cap != value {
+                plan.notes.push(format!(
+                    "BLOCK POSTURE: {name}={cap}, not {value}: the host target is {:.1} GiB \
+                     (LAMBDA_VM_BLOCK_SPILL_TARGET_GIB, else the cgroup or MemTotal less 10 GiB)",
+                    target as f64 / (1u64 << 30) as f64
+                ));
+            }
+            plan.set.push((name, cap));
+            continue;
         }
+        plan.set.push((name, value));
     }
     plan
 }
@@ -520,7 +540,10 @@ fn posture_plan(env: impl Fn(&str) -> Option<String>) -> PosturePlan {
 ///
 /// Sets environment variables: no other thread may exist.
 unsafe fn apply_posture() -> Vec<String> {
-    let plan = posture_plan(|name| std::env::var(name).ok());
+    let plan = posture_plan(
+        |name| std::env::var(name).ok(),
+        prover::block_whir::spill_target_bytes,
+    );
     for (name, value) in &plan.set {
         // SAFETY: the caller's: no other thread exists.
         unsafe { std::env::set_var(name, value) };
@@ -537,11 +560,13 @@ unsafe fn apply_posture() -> Vec<String> {
             w.join(" ")
         }
     };
-    vec![format!(
+    let mut lines = vec![format!(
         "BLOCK POSTURE SET: {} · from the environment: {} · jemalloc: {decay}",
         words(plan.set.iter().map(|(n, v)| format!("{n}={v}")).collect()),
         words(plan.env),
-    )]
+    )];
+    lines.extend(plan.notes);
+    lines
 }
 
 fn hex(bytes: &[u8]) -> String {
@@ -1677,14 +1702,37 @@ mod tests {
     #[test]
     fn the_posture_sets_only_unset_knobs() {
         use prover::lfm::whir_block_tree::POSTURE;
-        let all = posture_plan(|_| None);
+        let roomy = || 110u64 << 30;
+        let all = posture_plan(|_| None, roomy);
         assert_eq!(all.set, POSTURE.to_vec());
-        assert!(all.env.is_empty());
-        let mine = posture_plan(|n| (n == "TABLE_PARALLELISM").then(|| "8".to_string()));
+        assert!(all.env.is_empty() && all.notes.is_empty());
+        let mine = posture_plan(
+            |n| (n == "TABLE_PARALLELISM").then(|| "8".to_string()),
+            roomy,
+        );
         assert!(mine.set.iter().all(|(n, _)| *n != "TABLE_PARALLELISM"));
         assert_eq!(mine.env, vec!["TABLE_PARALLELISM=8".to_string()]);
     }
 
+    /// The precomputed-tree cache's posture follows the host target: 64
+    /// entries from a 64 GiB target up, 16 below it (with a note), and a value
+    /// the environment sets is left alone.
+    #[test]
+    fn the_tree_cache_posture_follows_the_host_target() {
+        use prover::lfm::whir_block_tree::POSTURE_TREE_CACHE_KNOB as CAP;
+        let none = |_: &str| None;
+        let cap = |plan: &PosturePlan| plan.set.iter().find(|(n, _)| *n == CAP).map(|(_, v)| *v);
+        let big = posture_plan(none, || 64u64 << 30);
+        assert_eq!(cap(&big), Some("64"));
+        assert!(big.notes.is_empty());
+        let small = posture_plan(none, || 38u64 << 30);
+        assert_eq!(cap(&small), Some("16"));
+        assert_eq!(small.notes.len(), 1, "the note says why");
+        let set = posture_plan(|n| (n == CAP).then(|| "32".to_string()), || 38u64 << 30);
+        assert_eq!(cap(&set), None, "the environment's value stays");
+        assert_eq!(set.env, vec![format!("{CAP}=32")]);
+    }
+
     /// The binary runs the allocator posture it compiles in: jemalloc never
     /// purges (`opt.dirty_decay_ms` and `opt.muzzy_decay_ms` are -1), unless
     /// `_RJEM_MALLOC_CONF` says otherwise. Deleting the `malloc_conf` export

prover/src/block_whir.rs

@@ -438,7 +438,7 @@ fn parse_spill_policy(value: Option<&str>) -> BlockSpillPolicy {
 /// smaller of the cgroup's memory limit (v2 or v1, [`cgroup_memory`]) and
 /// `MemTotal`, less 10 GiB ([`spill_target_from`]) (#1013's
 /// `spill_target_bytes` @ 035aef5d6).
-pub(crate) fn spill_target_bytes() -> u64 {
+pub fn spill_target_bytes() -> u64 {
     if let Some(gib) = std::env::var("LAMBDA_VM_BLOCK_SPILL_TARGET_GIB")
         .ok()
         .and_then(|v| v.trim().parse::<f64>().ok())

prover/src/lfm/whir_block_tree.rs

@@ -77,6 +77,9 @@ impl WhirTreeSink for StderrSink {
 /// too, and a verifier configured otherwise refuses (completeness, never
 /// soundness). The measurement-only `LAMBDA_VM_BASE_SPLIT` is not posture, and
 /// the allocator's never-purge posture is compiled into the binary.
+/// `LFM_PRECOMPUTED_TREE_CACHE_CAP`'s posture follows the host target
+/// ([`posture_tree_cache_cap`]): the table's 64 from a 64 GiB target up, 16
+/// below it.
 pub const POSTURE: &[(&str, &str)] = &[
     ("TABLE_PARALLELISM", "4"),
     ("LAMBDA_VM_MAX_ROWS_LOG2", "21"),
@@ -88,11 +91,42 @@ pub const POSTURE: &[(&str, &str)] = &[
     ("LAMBDA_VM_GRIND_GRID", "1024"),
 ];
 
+/// The precomputed-tree cache's knob, whose posture follows the host target.
+pub const POSTURE_TREE_CACHE_KNOB: &str = "LFM_PRECOMPUTED_TREE_CACHE_CAP";
+
+/// The host target (GiB, [`block_whir::spill_target_bytes`]) from which the
+/// posture keeps [`POSTURE`]'s 64 precomputed-tree cache entries.
+pub const POSTURE_TREE_CACHE_FULL_TARGET_GIB: u64 = 64;
+
+/// `LFM_PRECOMPUTED_TREE_CACHE_CAP`'s posture for a host `target` in bytes:
+/// 64 entries (≈ 100 MiB each, ≈ 6.2 GiB once full) from a
+/// [`POSTURE_TREE_CACHE_FULL_TARGET_GIB`] target up, 16 below it, where the
+/// ≈ 4.7 GiB they free count for more than the hits they lose. A miss only
+/// rebuilds the tree: the cache's key is the root, so nothing a proof commits
+/// to moves (#1013's rule, 49c4bb512).
+pub fn posture_tree_cache_cap(target: u64) -> &'static str {
+    if target >= POSTURE_TREE_CACHE_FULL_TARGET_GIB << 30 {
+        "64"
+    } else {
+        "16"
+    }
+}
+
 /// The `BLOCK POSTURE:` line: each posture knob as the process has it — equal
 /// to the posture, unset, or another value.
 pub fn posture_line() -> String {
     let words: Vec<String> = POSTURE
         .iter()
+        .map(|&(name, want)| {
+            if name == POSTURE_TREE_CACHE_KNOB {
+                (
+                    name,
+                    posture_tree_cache_cap(block_whir::spill_target_bytes()),
+                )
+            } else {
+                (name, want)
+            }
+        })
         .map(|(name, want)| match std::env::var(name) {
             Ok(v) if v == *want => format!("{name}={v}"),
             Ok(v) => format!("{name}={v} (≠ posture {want})"),