fix(analysis): bound type-checker continuations and admission work
This commit is contained in:
@@ -325,6 +325,32 @@ fn add_calculation(project: &mut Project, n: u128, result: AnalysisType, body: E
|
||||
id
|
||||
}
|
||||
|
||||
fn add_identity_calculation(
|
||||
project: &mut Project,
|
||||
n: u128,
|
||||
value_type: AnalysisType,
|
||||
) -> (Id, ParameterId) {
|
||||
let id = Id::from_u128(n);
|
||||
let parameter = ParameterId(Id::from_u128(n + 10_000));
|
||||
project.definitions.insert(
|
||||
id,
|
||||
definition(
|
||||
id,
|
||||
&format!("identity_{n}"),
|
||||
DefinitionBody::Calculation(CalculationDefinition {
|
||||
parameters: vec![Parameter {
|
||||
id: parameter,
|
||||
name: "value".into(),
|
||||
value_type: value_type.clone(),
|
||||
}],
|
||||
result: value_type,
|
||||
body: expression(Expr::Parameter(parameter)),
|
||||
}),
|
||||
),
|
||||
);
|
||||
(id, parameter)
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn complete_real_model_roundtrips_and_exposes_explicit_effective_bindings() {
|
||||
let f = fixture();
|
||||
@@ -611,6 +637,34 @@ fn calculations_are_pure_parameters_are_scoped_and_calls_bind_exactly() {
|
||||
calculation.parameters[0].name = "first_duration".into();
|
||||
renamed = execute_batch(&renamed, &[Command::EditDefinition(f.combine, revised)]).unwrap();
|
||||
admit(&renamed, AdmissionLimits::REFERENCE).unwrap();
|
||||
|
||||
// Distinct errors make argument order observable. Parameter a sorts before
|
||||
// b by UUID; reversing declaration order must reverse the first error.
|
||||
let mut ordered = f.project.clone();
|
||||
*base_mut(&mut ordered, f.total) = expression(Expr::Call {
|
||||
definition: reference(f.combine),
|
||||
arguments: BTreeMap::from([
|
||||
(f.a, Expr::Parameter(f.a)),
|
||||
(f.b, Expr::Property(f.respond)),
|
||||
]),
|
||||
});
|
||||
assert_eq!(reject(&ordered).code, "analysis_parameter");
|
||||
calculation_mut(&mut ordered, f.combine)
|
||||
.parameters
|
||||
.swap(0, 1);
|
||||
assert_eq!(reject(&ordered).code, "analysis_property");
|
||||
*base_mut(&mut ordered, f.total) = expression(binary(
|
||||
BinaryOp::Add,
|
||||
Expr::Property(f.respond),
|
||||
Expr::Parameter(f.a),
|
||||
));
|
||||
assert_eq!(reject(&ordered).code, "analysis_property");
|
||||
*base_mut(&mut ordered, f.total) = expression(binary(
|
||||
BinaryOp::Add,
|
||||
Expr::Parameter(f.a),
|
||||
Expr::Property(f.respond),
|
||||
));
|
||||
assert_eq!(reject(&ordered).code, "analysis_parameter");
|
||||
}
|
||||
|
||||
#[test]
|
||||
@@ -851,6 +905,7 @@ fn logical_depth_and_call_depth_have_exact_boundaries() {
|
||||
};
|
||||
}
|
||||
let deep = add_calculation(&mut f.project, 7000, scalar_number(), nested);
|
||||
eprintln!("analysis depth gate: admitting 128 unary nodes");
|
||||
admit(&f.project, AdmissionLimits::REFERENCE).unwrap();
|
||||
let old = std::mem::replace(
|
||||
&mut calculation_mut(&mut f.project, deep).body,
|
||||
@@ -863,9 +918,74 @@ fn logical_depth_and_call_depth_have_exact_boundaries() {
|
||||
op: UnaryOp::Negate,
|
||||
operand: Box::new(old),
|
||||
});
|
||||
eprintln!("analysis depth gate: rejecting 129 unary nodes");
|
||||
assert_eq!(reject(&f.project).code, "analysis_depth");
|
||||
// Only 129 nodes here: no hostile unbounded recursive teardown probe.
|
||||
f.project.definitions.remove(&deep);
|
||||
|
||||
let (identity, parameter) = add_identity_calculation(&mut f.project, 7001, scalar_number());
|
||||
let mut mixed = number(1);
|
||||
for level in 1..128 {
|
||||
mixed = match level % 5 {
|
||||
0 => Expr::Unary {
|
||||
op: UnaryOp::Absolute,
|
||||
operand: Box::new(mixed),
|
||||
},
|
||||
1 => binary(BinaryOp::Add, mixed, number(0)),
|
||||
2 => Expr::If {
|
||||
condition: Box::new(Expr::Boolean(true)),
|
||||
when_true: Box::new(mixed),
|
||||
when_false: Box::new(number(0)),
|
||||
},
|
||||
3 => Expr::Call {
|
||||
definition: reference(identity),
|
||||
arguments: BTreeMap::from([(parameter, mixed)]),
|
||||
},
|
||||
_ => Expr::Power {
|
||||
base: Box::new(mixed),
|
||||
exponent: 1,
|
||||
},
|
||||
};
|
||||
}
|
||||
let mixed_id = add_calculation(&mut f.project, 7002, scalar_number(), mixed);
|
||||
eprintln!("analysis depth gate: admitting mixed Binary/If/Call/Power/Unary depth 128");
|
||||
admit(&f.project, AdmissionLimits::REFERENCE).unwrap();
|
||||
let Binding::Expression(mixed) = std::mem::replace(
|
||||
&mut calculation_mut(&mut f.project, mixed_id).body,
|
||||
Binding::Unbound,
|
||||
) else {
|
||||
panic!()
|
||||
};
|
||||
calculation_mut(&mut f.project, mixed_id).body = expression(Expr::Unary {
|
||||
op: UnaryOp::Negate,
|
||||
operand: Box::new(mixed),
|
||||
});
|
||||
eprintln!("analysis depth gate: rejecting mixed depth 129");
|
||||
assert_eq!(reject(&f.project).code, "analysis_depth");
|
||||
f.project.definitions.remove(&mixed_id);
|
||||
|
||||
let list_type = AnalysisType::List(ScalarType::Number);
|
||||
let (list_identity, list_parameter) =
|
||||
add_identity_calculation(&mut f.project, 7003, list_type.clone());
|
||||
let mut list = Expr::List(vec![]);
|
||||
for level in 1..128 {
|
||||
list = if level % 2 == 0 {
|
||||
Expr::If {
|
||||
condition: Box::new(Expr::Boolean(false)),
|
||||
when_true: Box::new(list),
|
||||
when_false: Box::new(Expr::List(vec![])),
|
||||
}
|
||||
} else {
|
||||
Expr::Call {
|
||||
definition: reference(list_identity),
|
||||
arguments: BTreeMap::from([(list_parameter, list)]),
|
||||
}
|
||||
};
|
||||
}
|
||||
add_calculation(&mut f.project, 7004, list_type, list);
|
||||
eprintln!("analysis depth gate: admitting contextual empty lists through If/Call depth 128");
|
||||
admit(&f.project, AdmissionLimits::REFERENCE).unwrap();
|
||||
|
||||
let mut previous = add_calculation(&mut f.project, 7100, scalar_number(), number(1));
|
||||
for n in 7101..7132 {
|
||||
previous = add_calculation(
|
||||
@@ -878,6 +998,7 @@ fn logical_depth_and_call_depth_have_exact_boundaries() {
|
||||
},
|
||||
);
|
||||
}
|
||||
eprintln!("analysis depth gate: admitting 32-definition call graph");
|
||||
admit(&f.project, AdmissionLimits::REFERENCE).unwrap();
|
||||
add_calculation(
|
||||
&mut f.project,
|
||||
@@ -888,6 +1009,7 @@ fn logical_depth_and_call_depth_have_exact_boundaries() {
|
||||
arguments: BTreeMap::new(),
|
||||
},
|
||||
);
|
||||
eprintln!("analysis depth gate: rejecting 33-definition call graph");
|
||||
assert_eq!(reject(&f.project).code, "analysis_call_depth");
|
||||
}
|
||||
|
||||
@@ -992,6 +1114,36 @@ fn static_work_is_lowerable_deterministic_and_aggregated_across_cases() {
|
||||
.admission_usage();
|
||||
assert_eq!(first, second);
|
||||
assert!(first.static_events > used);
|
||||
let mut described = f.project.clone();
|
||||
described
|
||||
.definitions
|
||||
.get_mut(&f.duration)
|
||||
.unwrap()
|
||||
.description = "x".repeat(1024);
|
||||
assert_eq!(
|
||||
admit(&described, AdmissionLimits::REFERENCE)
|
||||
.unwrap()
|
||||
.admission_usage()
|
||||
.static_events,
|
||||
used + 1024,
|
||||
);
|
||||
// Duration is the first definition in UUID order. The forbidden final byte
|
||||
// must not be inspected before its complete text span has been charged.
|
||||
described
|
||||
.definitions
|
||||
.get_mut(&f.duration)
|
||||
.unwrap()
|
||||
.description = format!("{}\0", "x".repeat(1023));
|
||||
let text_limit = AdmissionLimits {
|
||||
max_static_events: 2 + described.definitions[&f.duration].name.len() as u64 + 1023,
|
||||
};
|
||||
let failure = match admit(&described, text_limit) {
|
||||
Ok(_) => panic!("Text inspection must be precharged"),
|
||||
Err(error) => error,
|
||||
};
|
||||
assert_eq!(failure.code, "analysis_limit");
|
||||
assert_eq!(failure.object, f.duration);
|
||||
assert_eq!(failure.field, "description");
|
||||
}
|
||||
|
||||
#[test]
|
||||
|
||||
Reference in New Issue
Block a user