diff --git a/changelog.d/codegen-facts-local-ranges.md b/changelog.d/codegen-facts-local-ranges.md new file mode 100644 index 0000000000..9261809518 --- /dev/null +++ b/changelog.d/codegen-facts-local-ranges.md @@ -0,0 +1 @@ +Performance: the whole-program interval of an int32 local reaches codegen's range proofs. wpfacts already proved such intervals (a `let` read from an int Array is in the Array's element interval; a typed body's I32 parameter is in its signature's interval) but exported only "this local is an int32", so an element key built from such locals (`table[(old + 6) * 128 + square]`) was computed in doubles and normalized by a runtime call, and an at-rest element site keyed by a signed int32 local converted the key to a double and back. Now the key is an i32 chain bounded by one unsigned compare. `PERRY_FACTS_LOCAL_RANGES=0` restores the old lowering. Check mode witnesses the interval at every store into such a `let` (signature parameters are witnessed at their call sites). diff --git a/crates/perry-codegen/src/codegen/facts_int32_locals.rs b/crates/perry-codegen/src/codegen/facts_int32_locals.rs index 63eb95c03d..25815cf8e9 100644 --- a/crates/perry-codegen/src/codegen/facts_int32_locals.rs +++ b/crates/perry-codegen/src/codegen/facts_int32_locals.rs @@ -8,8 +8,14 @@ //! (`repsel_benefit`). A double entering that slot is an exact int32, so it //! converts with `fptosi` instead of ToInt32 (`store_from_double`). //! +//! The proof's interval is a range proof of the local at every read +//! (`expr::range_facts::facts_local_range`, `PERRY_FACTS_LOCAL_RANGES=0` +//! turns that off): an index or an integer chain built from it needs no +//! dominating guard. +//! //! Check mode (`PERRY_VERIFY_FACTS=1`) witnesses every store: the stored value -//! must pass the exact-i32 test (`emit_typed_i32_plain_guard_and_raw`). Stores the +//! must pass the exact-i32 test (`emit_typed_i32_plain_guard_and_raw`) and lie +//! in the interval the range proofs read. Stores the //! ordinary lowering would compute natively in i32 take the double path //! there, so no store escapes the witness (`checked`). //! @@ -96,6 +102,24 @@ pub(crate) fn witness_exact(ctx: &mut crate::expr::FnCtx<'_>, value: &str, id: u let nz = ctx.block().icmp_eq(I64, &bits, "-9223372036854775808"); exact = ctx.block().or(I1, &exact, &nz); } + // The interval the body's range proofs read for this local + // (`range_facts::facts_local_range`): the stored value lies in it. A + // tolerated `-0` compares as 0. + if let Some(range) = crate::expr::facts_local_range(ctx, id) { + let blk = ctx.block(); + let ge = blk.fcmp( + "oge", + value, + &crate::nanbox::double_literal(range.min as f64), + ); + let le = blk.fcmp( + "ole", + value, + &crate::nanbox::double_literal(range.max as f64), + ); + let inside = blk.and(I1, &ge, &le); + exact = blk.and(I1, &exact, &inside); + } crate::verify_facts::tick(ctx); let miss = ctx.new_block("int32.input.verify_miss"); let next = ctx.new_block("int32.input.admitted"); @@ -141,3 +165,7 @@ pub(crate) fn store_from_double( #[cfg(test)] #[path = "facts_int32_locals_tests.rs"] mod tests; + +#[cfg(test)] +#[path = "facts_local_ranges_tests.rs"] +mod range_tests; diff --git a/crates/perry-codegen/src/codegen/facts_local_ranges_tests.rs b/crates/perry-codegen/src/codegen/facts_local_ranges_tests.rs new file mode 100644 index 0000000000..0cf12af323 --- /dev/null +++ b/crates/perry-codegen/src/codegen/facts_local_ranges_tests.rs @@ -0,0 +1,112 @@ +//! The whole-program interval of a proven int32 `let` is a range proof +//! (`expr::range_facts::facts_local_range`): a key built from the local is +//! an int32 by the interval, so it is computed in i32 and handed to the +//! element read as it is. Without the interval the key is a double chain +//! and goes through the index normalizer. + +use std::sync::Arc; + +use crate::codegen::{ElisionFacts, FactsRep, ProgramFactsView}; +use crate::{compile_module, CompileOptions}; +use perry_hir::Module; + +/// `k` has no local range proof (an element of an ordinary Array): only +/// the facts' interval bounds it. +const SRC: &str = "export function f(t: number[], u: number[], i: number): number {\n\ + const k = u[i];\n\ + return t[k * 2 + 1] ?? -1;\n\ + }\n"; + +fn lower(src: &str) -> Module { + let src = src.to_string(); + std::thread::Builder::new() + .stack_size(32 * 1024 * 1024) + .spawn(move || { + let mut cache = perry_diagnostics::SourceCache::new(); + let parsed = perry_parser::parse_typescript_with_cache(&src, "lr.ts", &mut cache) + .expect("parses"); + perry_hir::lower_module(&parsed.module, "lr", "lr.ts").expect("lowers") + }) + .expect("spawn") + .join() + .expect("lowering thread") +} + +/// The HIR id of the `let` named `name`. +fn let_id(m: &Module, name: &str) -> u32 { + let text = format!("{m:?}"); + let mut rest = text.as_str(); + while let Some(i) = rest.find("Let { id: ") { + rest = &rest[i + 10..]; + let num: String = rest.chars().take_while(|c| c.is_ascii_digit()).collect(); + let j = rest.find("name: \"").expect("named let"); + if rest[j + 7..].starts_with(&format!("{name}\"")) { + return num.parse().expect("id"); + } + } + panic!("no let {name}"); +} + +/// The IR of `f` with `k` proven int32, and its interval `range` when given. +fn ir_of_f(range: Option<(i64, i64)>) -> String { + let m = lower(SRC); + let mut elision = ElisionFacts::default(); + let k = let_id(&m, "k"); + elision.int32_inputs.insert(k); + elision.local_reps.insert(k, FactsRep::I32); + if let Some(range) = range { + elision.int32_ranges.insert(k, range); + } + let opts = CompileOptions { + emit_ir_only: true, + program_facts: ProgramFactsView { + elision: Arc::new(elision), + ..Default::default() + }, + ..Default::default() + }; + let ir = String::from_utf8(compile_module(&m, opts).expect("compiles")).expect("UTF-8"); + let start = ir + .lines() + .position(|l| l.starts_with("define") && l.contains("perry_fn_lr__f")) + .expect("f defined"); + ir.lines() + .skip(start) + .take_while(|l| *l != "}") + .collect::>() + .join("\n") +} + +fn normalizer_calls(ir: &str) -> usize { + ir.lines() + .filter(|l| l.contains("call") && l.contains("perry_array_index_normalize_i32")) + .count() +} + +/// The normalizer calls of `f` when `k` has no interval: one for `t[k * 2 + +/// 1]` (and one for `u[i]`, whose key is a double parameter in every arm). +fn baseline() -> usize { + let n = normalizer_calls(&ir_of_f(None)); + assert!( + n >= 1, + "the key of `t[k * 2 + 1]` is normalized without an interval" + ); + n +} + +#[test] +fn a_key_built_from_a_ranged_int32_let_is_an_i32_key() { + // `k` in [-3, 12]: `k * 2 + 1` is in [-5, 25], an int32 of either sign: + // its normalizer call is gone, and the key is an i32 chain. + let f = ir_of_f(Some((-3, 12))); + assert_eq!(normalizer_calls(&f) + 1, baseline(), "{f}"); + assert!(f.contains("mul i32") || f.contains("shl i32"), "{f}"); +} + +#[test] +fn an_interval_whose_chain_leaves_int32_is_no_i32_key() { + // `k` up to 2^31 - 1: `k * 2 + 1` may pass int32, so the key keeps its + // double (a wrapped i32 would name another element). + let f = ir_of_f(Some((0, i64::from(i32::MAX)))); + assert_eq!(normalizer_calls(&f), baseline(), "{f}"); +} diff --git a/crates/perry-codegen/src/codegen/function.rs b/crates/perry-codegen/src/codegen/function.rs index 1889493332..0713a0c9ab 100644 --- a/crates/perry-codegen/src/codegen/function.rs +++ b/crates/perry-codegen/src/codegen/function.rs @@ -1712,6 +1712,8 @@ pub(super) fn compile_function( ctx.sig_return = sig_return; ctx.nonnegative_integer_locals .extend(super::signature_entry::nonnegative_params(f, plan)); + ctx.int_range_facts + .extend(super::signature_entry::param_range_facts(f, plan)); } let wrapper_name = format!("__perry_wrap_{}", public_llvm_name); super::arguments::materialize_arguments_object( diff --git a/crates/perry-codegen/src/codegen/method.rs b/crates/perry-codegen/src/codegen/method.rs index aef8786324..839e88aca3 100644 --- a/crates/perry-codegen/src/codegen/method.rs +++ b/crates/perry-codegen/src/codegen/method.rs @@ -999,7 +999,10 @@ pub(super) fn compile_method( buffer_hazard_reasons: HashMap::new(), native_i32_aliases: HashMap::new(), int_range_aliases: HashMap::new(), - int_range_facts: Vec::new(), + int_range_facts: match sig { + Some(tm) => super::signature_entry::param_range_facts(method, &tm.plan), + None => Vec::new(), + }, next_loop_proof_scope_id: 0, nonnegative_integer_locals: nonnegative_param_ids, elided_arguments: HashMap::new(), diff --git a/crates/perry-codegen/src/codegen/program_facts_view.rs b/crates/perry-codegen/src/codegen/program_facts_view.rs index fd4b5ef8eb..2112555279 100644 --- a/crates/perry-codegen/src/codegen/program_facts_view.rs +++ b/crates/perry-codegen/src/codegen/program_facts_view.rs @@ -335,6 +335,11 @@ pub struct ElisionFacts { pub local_reps: std::collections::BTreeMap, /// The `int32_inputs` whose interval is non-negative. pub nonneg_int32_inputs: std::collections::BTreeSet, + /// Each of the `int32_inputs` with its interval (wpfacts + /// `BindingFacts::int_range`): every value the binding ever holds lies + /// in it. Codegen's range proofs read it for a proven int32 `let` + /// (`expr::range_facts::facts_local_range`). + pub int32_ranges: std::collections::BTreeMap, /// Local id → it holds only strings and ordinary Arrays: `x.length` is a /// Number. pub length_number_inputs: std::collections::BTreeSet, diff --git a/crates/perry-codegen/src/codegen/signature_entry.rs b/crates/perry-codegen/src/codegen/signature_entry.rs index a8032ee6dd..4481a79a83 100644 --- a/crates/perry-codegen/src/codegen/signature_entry.rs +++ b/crates/perry-codegen/src/codegen/signature_entry.rs @@ -1050,6 +1050,35 @@ pub(crate) fn slot_i32_params(f: &Function, plan: &SpecFnPlan) -> HashSet { .collect() } +/// `F$sig`'s parameters with the interval the signature proves (T1): an I32 +/// parameter in its i32 slot (never written: plan selection demoted written +/// parameters) holds an integer of its interval for the whole body, so the +/// body's range proofs start from it (`FnCtx::int_range_facts`, under a +/// scope no loop ends). The interval is witnessed at every typed site and at +/// the boxed entry (`witness_value`). Empty with +/// `PERRY_FACTS_LOCAL_RANGES=0`. +pub(crate) fn param_range_facts(f: &Function, plan: &SpecFnPlan) -> Vec { + let Some(sig) = plan.signature.as_ref() else { + return Vec::new(); + }; + if !crate::expr::facts_local_ranges() { + return Vec::new(); + } + f.params + .iter() + .zip(plan.reps.iter()) + .zip(sig.ranges.iter()) + .filter_map(|((p, rep), range)| { + let (min, max) = (*range)?; + matches!(rep, SpecParamRep::I32).then_some(crate::expr::IntRangeFact { + local_id: p.id, + scope_id: u32::MAX, + range: crate::expr::IntRange { min, max }, + }) + }) + .collect() +} + /// `F$sig`'s parameters that seed `nonnegative_integer_locals` (T1): an I32 /// parameter in its i32 slot whose interval has `lo >= 0` (the slot is /// never written: plan selection demoted written parameters). diff --git a/crates/perry-codegen/src/expr/index_get.rs b/crates/perry-codegen/src/expr/index_get.rs index 756f6d0081..68fecf31e6 100644 --- a/crates/perry-codegen/src/expr/index_get.rs +++ b/crates/perry-codegen/src/expr/index_get.rs @@ -1475,6 +1475,32 @@ pub(crate) fn lower(ctx: &mut FnCtx<'_>, expr: &Expr) -> Result { let repair_slot = receiver_repair_slot(ctx, object); let confined = confined_receiver(ctx, object); let proven = proven_array::fact(ctx, object, *element_offset); + // A key the range proofs bound to int32 (of either sign) + // is lowered as that i32: the split takes it as a native + // key, with no normalizer call (`int32_key`). + if super::int32_key::proven(ctx, index) { + return rooting::with_operands_rooted_across( + ctx, + &[object], + &[index], + |ctx| super::int32_key::lower(ctx, index), + |ctx, vals, key| { + with_confined_read(ctx, confined, |ctx| { + lower_array_index_get_via_canonical_i32_split( + ctx, + &vals[0], + &key, + index, + false, + false, + false, + repair_slot.as_deref(), + proven, + ) + }) + }, + ); + } return rooting::with_operands_rooted(ctx, &[object, index], |ctx, vals| { with_confined_read(ctx, confined, |ctx| { lower_array_index_get_via_canonical_i32_split( diff --git a/crates/perry-codegen/src/expr/index_set.rs b/crates/perry-codegen/src/expr/index_set.rs index 6ef441554c..0159f10d9a 100644 --- a/crates/perry-codegen/src/expr/index_set.rs +++ b/crates/perry-codegen/src/expr/index_set.rs @@ -320,7 +320,13 @@ fn lower_array_index_set_via_runtime_key( &[object], &[index, value], |ctx| { - let idx_double = lower_expr(ctx, index)?; + // A key the range proofs bound to int32 is lowered as that i32 + // (`int32_key`): the guarded store takes it as a native key. + let idx_double = if super::int32_key::proven(ctx, index) { + super::int32_key::lower(ctx, index)? + } else { + lower_expr(ctx, index)? + }; let value_needs_barrier = array_store_needs_write_barrier(ctx, value); let (val_double, val_bits) = lower_value_for_dynamic_index_set( ctx, diff --git a/crates/perry-codegen/src/expr/int32_key.rs b/crates/perry-codegen/src/expr/int32_key.rs new file mode 100644 index 0000000000..37a694b4d3 --- /dev/null +++ b/crates/perry-codegen/src/expr/int32_key.rs @@ -0,0 +1,38 @@ +//! An element key the body's range proofs bound to the int32 range, of +//! either sign. +//! +//! The canonical key split (`index_get`'s runtime-key arm, `index_set`'s +//! runtime-key store) admits a key that is only statically numeric through +//! the shared normalizer (`index_key`, a call) unless the key's lowered +//! double has a native i32 source. A key whose range is proven inside int32 +//! ([`proven`]: `i32_fast_path::is_known_i32_range`, so a loop fact, a typed +//! body's parameter interval, or the whole-program interval of an int32 +//! `let`, `range_facts::facts_local_range`) is an exact int32 at every +//! evaluation, so it is lowered as one ([`lower`]: its i32 chain, else one +//! conversion of its double) and handed to the split as that source. The +//! split's unsigned bound (N10) then declines a negative key onto the arm +//! that reads the original value, as it does for any native key. +//! +//! `PERRY_FACTS_LOCAL_RANGES=0` keeps the double key and the normalizer. + +use anyhow::Result; +use perry_hir::Expr; + +use super::FnCtx; +use crate::types::{DOUBLE, I32}; + +/// `index` is an int32 at every evaluation by the body's range proofs, and +/// the unsigned bound is on (the split then needs no sign test for it). +pub(crate) fn proven(ctx: &FnCtx<'_>, index: &Expr) -> bool { + super::facts_local_ranges() + && super::index_key::unsigned_bound() + && !ctx.wpfacts_off + && super::i32_fast_path::is_known_i32_range(ctx, index) +} + +/// The key `index` ([`proven`]) as the double whose source is its i32 +/// (`sitofp`): `index_key::normalize_unsigned` hands that i32 over as it is. +pub(crate) fn lower(ctx: &mut FnCtx<'_>, index: &Expr) -> Result { + let idx = super::lower_expr_as_i32(ctx, index)?; + Ok(ctx.block().sitofp(I32, &idx, DOUBLE)) +} diff --git a/crates/perry-codegen/src/expr/mod.rs b/crates/perry-codegen/src/expr/mod.rs index 8e1d2e3031..7971bb6542 100644 --- a/crates/perry-codegen/src/expr/mod.rs +++ b/crates/perry-codegen/src/expr/mod.rs @@ -222,6 +222,7 @@ pub(crate) use range_facts::{ record_int_facts_for_update, record_local_value_alias_for_write, while_condition_range_fact, IntRange, IntRangeFact, }; +pub(crate) use range_facts::{facts_local_range, facts_local_ranges}; pub(crate) use strings::emit_string_literal_global; pub(crate) use typed_feedback::{ emit_typed_feedback_record_call, emit_typed_feedback_register_site, native_region_slug, @@ -3365,6 +3366,7 @@ pub(crate) use index_get::guarded_array::emit_spread_stack_admission; #[cfg(test)] mod index_get_claim_tests; pub(crate) mod index_key; +pub(crate) mod int32_key; #[cfg(test)] mod kind_entry_selection_tests; #[cfg(test)] diff --git a/crates/perry-codegen/src/expr/range_facts.rs b/crates/perry-codegen/src/expr/range_facts.rs index 6496f40d13..f5e17de6e5 100644 --- a/crates/perry-codegen/src/expr/range_facts.rs +++ b/crates/perry-codegen/src/expr/range_facts.rs @@ -323,10 +323,45 @@ fn int_range_for_local( // parameter. Without it one unbounded parameter leaf poisons the whole // index expression and demotes EVERY array access in the function. let result = result.or_else(|| ctx.param_int_ranges.get(&id).copied()); + // The whole-program interval of a proven int32 `let`: the weakest proof, + // read only when nothing local bounds the local. + let result = result.or_else(|| facts_local_range(ctx, id)); seen.remove(&id); result } +/// `PERRY_FACTS_LOCAL_RANGES=0` (`off`, `false`): codegen's range proofs do +/// not read the whole-program interval of a proven int32 `let` or of a typed +/// body's I32 parameter (main before this rule). +pub(crate) fn facts_local_ranges() -> bool { + static ON: std::sync::OnceLock = std::sync::OnceLock::new(); + *ON.get_or_init(|| { + !matches!( + std::env::var("PERRY_FACTS_LOCAL_RANGES").as_deref(), + Ok("0") | Ok("off") | Ok("false") + ) + }) +} + +/// The whole-program interval (wpfacts `BindingFacts::int_range`) of local +/// `id` when this body holds it as a proven int32 `let` +/// (`FnCtx::facts_int32_locals`): every value the local ever holds is an +/// integer in it, at every read, so it is a range proof that needs no +/// dominating guard. Check mode witnesses the interval at every store into +/// such a local (`codegen::facts_int32_locals::witness_exact`). The negative +/// control `PERRY_FACTS_SABOTAGE=localrange` claims the interval's lower +/// bound alone. +pub(crate) fn facts_local_range(ctx: &FnCtx<'_>, id: u32) -> Option { + if !facts_local_ranges() || ctx.wpfacts_off || !ctx.facts_int32_locals.contains(&id) { + return None; + } + let &(min, max) = ctx.wpfacts.int32_ranges.get(&id)?; + if std::env::var("PERRY_FACTS_SABOTAGE").as_deref() == Ok("localrange") { + return Some(IntRange { min, max: min }); + } + Some(IntRange { min, max }) +} + fn int_range_expr_inner( ctx: &FnCtx<'_>, expr: &Expr, diff --git a/crates/perry/src/commands/compile/compile_env.rs b/crates/perry/src/commands/compile/compile_env.rs index 1afaac2795..fba08a9888 100644 --- a/crates/perry/src/commands/compile/compile_env.rs +++ b/crates/perry/src/commands/compile/compile_env.rs @@ -67,6 +67,7 @@ pub(super) const COMPILE_ENV_VARS: &[&str] = &[ "PERRY_FACTS_INT_RANGES", "PERRY_FACTS_INT_DEMAND", "PERRY_FACTS_COMPARE_DEMAND", + "PERRY_FACTS_LOCAL_RANGES", "PERRY_FACTS_AT_REST", "PERRY_REST_ELEMS", "PERRY_REST_FIELDS", diff --git a/crates/perry/src/commands/compile/compile_env/tests.rs b/crates/perry/src/commands/compile/compile_env/tests.rs index dbd5756bd1..d1d4cc44cc 100644 --- a/crates/perry/src/commands/compile/compile_env/tests.rs +++ b/crates/perry/src/commands/compile/compile_env/tests.rs @@ -385,6 +385,17 @@ fn signed_index_switch_is_a_cache_input() { ); } +/// The local-range switch decides whether codegen's range proofs read the +/// facts' interval of an int32 local, so `=0` must never reuse an `=1` +/// object. +#[test] +fn local_ranges_switch_is_a_cache_input() { + assert!( + COMPILE_ENV_VARS.contains(&"PERRY_FACTS_LOCAL_RANGES"), + "PERRY_FACTS_LOCAL_RANGES must key the compile caches" + ); +} + /// N4: the cold-path switch changes helper declarations, call-site /// attributes and branch weights, so `=0` must never reuse an `=1` object. #[test] diff --git a/crates/perry/src/commands/compile/program_facts.rs b/crates/perry/src/commands/compile/program_facts.rs index 2fb428e1a5..b2fba4bdae 100644 --- a/crates/perry/src/commands/compile/program_facts.rs +++ b/crates/perry/src/commands/compile/program_facts.rs @@ -662,6 +662,9 @@ fn elision_for(pf: &perry_wpfacts::ProgramFacts, path: &str) -> perry_codegen::E .is_some_and(|(lo, hi)| lo >= i64::from(i32::MIN) && hi <= i64::from(i32::MAX)) { out.int32_inputs.insert(*id); + if let Some(range) = b.int_range { + out.int32_ranges.insert(*id, range); + } if b.zero_tol { out.zero_tolerant_locals.insert(*id); } diff --git a/scripts/check_file_size.sh b/scripts/check_file_size.sh index cd4d1f2ed2..fdfcb6a249 100755 --- a/scripts/check_file_size.sh +++ b/scripts/check_file_size.sh @@ -28,7 +28,7 @@ crates/perry-codegen/src/codegen/mod.rs 3662 # Representation-aware HIR fact collection; further decomposition is tracked in #1435. crates/perry-codegen/src/collectors/hir_facts.rs 2760 # Representation-aware expression dispatch; further decomposition is tracked in #1435. -crates/perry-codegen/src/expr/mod.rs 2838 +crates/perry-codegen/src/expr/mod.rs 2844 # Loop versioning and representation evidence share lowering state; decomposition is tracked in #1435. crates/perry-codegen/src/stmt/loops.rs 8354 # Representation-aware map core; further decomposition is tracked in #1435. diff --git a/scripts/test-verify-facts-s0.py b/scripts/test-verify-facts-s0.py index 9273ed54d7..8981380682 100644 --- a/scripts/test-verify-facts-s0.py +++ b/scripts/test-verify-facts-s0.py @@ -135,6 +135,7 @@ def oracle(source, *argv): ("signature-escape-negative", "signature-escape", "signature"), ("signature-range-negative", "signature-range", "signature"), ("signed-index-negative", "signature-range", "signature"), + ("local-range-negative", "localrange", "int32 input"), ("rest-field-negative", "restfield", "field rep"), ("rest-field-zero-negative", "restfield", "field rep"), ("rest-elem-negative", "restelem", "array rep"), diff --git a/scripts/verify_facts_s0/local-range-negative.ts b/scripts/verify_facts_s0/local-range-negative.ts new file mode 100644 index 0000000000..f640ff2f01 --- /dev/null +++ b/scripts/verify_facts_s0/local-range-negative.ts @@ -0,0 +1,16 @@ +// The facts' interval of a proven int32 `let` is a range proof in codegen +// (`range_facts::facts_local_range`): `k` is in [3, 18], so `k * 2 + 1` is an +// int32 element key with no guard. Under PERRY_FACTS_SABOTAGE=localrange the +// interval claimed is its lower bound alone ([3, 3]): the store witness of +// the local must report the first other value. +// A loop bound the compiler cannot fold keeps the loop as written. +const RUN = Math.random() < 2 ? 1 : 0; +const table: number[] = []; +for (let i = 0; i < 64; i++) table.push(i * 7); +function pick(i: number): number { + const k = (i & 15) + 3; + return table[k * 2 + 1] ?? -1; +} +let s = 0; +for (let i = 0; i < 40 * RUN; i++) s += pick(i); +console.log(s); diff --git a/tests/parity/language/number/test_facts_local_ranges.ts b/tests/parity/language/number/test_facts_local_ranges.ts new file mode 100644 index 0000000000..831a9da254 --- /dev/null +++ b/tests/parity/language/number/test_facts_local_ranges.ts @@ -0,0 +1,138 @@ +// The whole-program interval of a proven int32 local is a range proof in +// codegen (PERRY_FACTS_LOCAL_RANGES): a key or an integer chain built from +// such `let`s and from a typed body's I32 parameters is computed in i32. +// Exact against node with the rule on, off and in check mode. +// A loop bound the compiler cannot fold keeps each loop as written. +const RUN = Math.random() < 2 ? 1 : 0; + +const table: number[] = []; +for (let i = 0; i < 4096; i++) table.push((i * 2654435761) | 0); + +// 1. A `let` read from an int Array and a parameter, both of either sign, +// feed a key: `(old + 6) * 64 + square`. +class Grid { + cells: number[] = new Array(64).fill(0); + h = 0; + put(square: number, piece: number): void { + const old = this.cells[square] ?? 0; + if (old !== 0) this.h ^= table[(old + 6) * 64 + square] ?? 0; + this.cells[square] = piece; + if (piece !== 0) this.h ^= table[(piece + 6) * 64 + square] ?? 0; + } +} +const g = new Grid(); +for (let i = 0; i < 64 * RUN; i++) g.put(i, (i % 13) - 6); +for (let i = 0; i < 64 * RUN; i += 3) g.put(i, 0); +for (let i = 0; i < 64 * RUN; i += 7) g.put(i, i & 1 ? -6 : 6); +console.log("grid", g.h, g.cells.join(",")); + +// 2. A key that can be negative: it names a property, and the chain's +// negative value must not wrap into an element. +const sparse: number[] = [10, 20, 30, 40]; +function probe(i: number): number { + const k = (i & 7) - 4; + return sparse[k * 2 + 1] ?? -1; +} +let s2 = 0; +for (let i = 0; i < 16 * RUN; i++) s2 += probe(i); +(sparse as any)[-3] = 7; +for (let i = 0; i < 16 * RUN; i++) s2 += probe(i); +console.log("negative key", s2); + +// 3. A product past int32: the interval is no int32, so the key stays a +// double and names the property "4294967296" (never element 0). +const wide: number[] = [1, 2, 3]; +function far(i: number): number { + const a = (i & 1) * 65536; + const b = a * 65536; + (wide as any)[b] = i + 100; + return ((wide as any)[b] as number) + wide[0]; +} +let s3 = 0; +for (let i = 0; i < 4 * RUN; i++) s3 += far(i); +console.log("past int32", s3, wide.length, wide[0], (wide as any)[4294967296]); + +// 4. Lets that are no int32: a fraction, -0, NaN, undefined. No interval. +function loose(i: number): string { + const half = i / 2; + const negz = i === 0 ? -0 : i; + const nan = i === 1 ? NaN : i; + const und = i === 2 ? undefined : i; + const o: any = { 0: "zero", 1: "one", 2: "two", 0.5: "half", NaN: "nan", undefined: "undef" }; + return [o[half], o[negz], o[nan], o[und as any], Object.is(negz, -0)].join("/"); +} +const out4: string[] = []; +for (let i = 0; i < 4 * RUN; i++) out4.push(loose(i)); +console.log("loose", out4.join(" ")); + +// 5. A let a closure captures and writes (boxed), and a let written past +// its first interval: the proof covers every value or it is not used. +function boxed(n: number): number { + let k = n & 3; + const bump = () => { + k = k + 100; + }; + let r = table[k + 1] ?? -1; + bump(); + r = (r + (table[k + 1] ?? -1)) | 0; + return r; +} +function widened(n: number): number { + let k = n & 3; + let r = table[k] ?? -1; + if (n > 5) k = k - 9; + r = (r + (table[k] ?? -5)) | 0; + return r; +} +let s5 = 0; +for (let i = 0; i < 12 * RUN; i++) s5 = (s5 + boxed(i) + widened(i)) | 0; +console.log("boxed and widened", s5); + +// 6. Typed parameters with signed intervals in a chain: every call is +// direct, so both are I32 (`i` in [-1, 7], `j` in [-2, 8]). +class Lookup { + t: number[] = []; + constructor() { + for (let i = 0; i < 64; i++) this.t.push(i * i); + } + get(i: number, j: number): number { + return this.t[i * 8 + j] ?? -1; + } +} +const lk = new Lookup(); +let s6 = 0; +for (let i = 0; i < 9 * RUN; i++) for (let j = -2; j < 9 * RUN; j++) s6 += lk.get(i - 1, j); +(lk.t as any)[-3] = 1000; +for (let j = -2; j < 3 * RUN; j++) s6 += lk.get(-1, j + 3); +console.log("typed chain", s6); + +// 6b. The same helper also called indirectly with a key past every direct +// site's range, a fraction and a negative chain: its parameters are no I32. +class LookupLoose { + t: number[] = []; + constructor() { + for (let i = 0; i < 64; i++) this.t.push(i * i); + } + get(i: number, j: number): number { + return this.t[i * 8 + j] ?? -1; + } +} +const ll = new LookupLoose(); +let s6b = 0; +for (let i = 0; i < 9 * RUN; i++) for (let j = -2; j < 9 * RUN; j++) s6b += ll.get(i - 1, j); +const viaCall = ll.get; +console.log("loose chain", s6b, viaCall.call(ll, 1000, 5), viaCall.call(ll, 0.5, 1), viaCall.call(ll, -1, 9)); + +// 7. Loop counters keep their own (narrower) facts beside a facts interval. +function sweep(): number { + let acc = 0; + for (let r = 0; r < 8 * RUN; r++) { + const base = r * 8; + for (let f = 0; f < 8; f++) { + const sq = base + f; + acc = (acc + (table[sq * 3 + 1] ?? 0)) | 0; + } + } + return acc; +} +console.log("sweep", sweep());