250 lines
10 KiB
Rust
250 lines
10 KiB
Rust
use dever_core::diagnostic::Diagnostic;
|
|
use dever_core::source::SourceMap;
|
|
|
|
fn checked(declarations: &str) -> Result<dever_core::hir::Program, Vec<Diagnostic>> {
|
|
let mut sources = SourceMap::default();
|
|
sources.add("main.dever", declarations);
|
|
dever_core::check(&sources)
|
|
}
|
|
|
|
fn accepts(declarations: &str) {
|
|
checked(declarations).unwrap_or_else(|errors| panic!("unexpected errors: {errors:#?}"));
|
|
}
|
|
|
|
fn rejects(declarations: &str) {
|
|
let errors = checked(declarations).expect_err("constraint proof must fail");
|
|
assert!(
|
|
errors.iter().any(|error| error.code == "C011"),
|
|
"{errors:#?}"
|
|
);
|
|
}
|
|
|
|
#[test]
|
|
fn constrained_construction_requires_a_proof_even_in_unused_functions() {
|
|
rejects(
|
|
"type Port { value: Int >= 1 and <= 65535 }\nbad() (port: Port) { port = Port { value = 0 } }",
|
|
);
|
|
rejects(
|
|
"type Port { value: Int >= 1 and <= 65535 }\nbad(value: Int) (port: Port) { port = Port { value = value } }",
|
|
);
|
|
accepts(
|
|
"type Port { value: Int >= 1 and <= 65535 }\nmake() (port: Port) { port = Port { value = 8080 } }",
|
|
);
|
|
}
|
|
|
|
#[test]
|
|
fn clause_domains_establish_safe_construction_and_arithmetic() {
|
|
accepts(
|
|
"type Port { value: Int >= 1 and <= 65535 }\nmake(value: Int >= 1 and <= 65534) (port: Port) { port = Port { value = value + 1 } }\nmake(value: other) (port: Port) { port = Port { value = 8080 } }",
|
|
);
|
|
rejects(
|
|
"type Port { value: Int >= 1 and <= 65535 }\nmake(value: Int >= 1 and <= 65535) (port: Port) { port = Port { value = value + 1 } }\nmake(value: other) (port: Port) { port = Port { value = 8080 } }",
|
|
);
|
|
}
|
|
|
|
#[test]
|
|
fn constrained_outputs_and_input_transfer_survive_function_boundaries() {
|
|
accepts(
|
|
"type Port { value: Int >= 1 and <= 65535 }\nidentity(value: Int) (result: Int) { result = value }\nnumber(port: Port) (value: Int >= 1 and <= 65535) { value = identity(port.value) }\nmake(port: Port) (result: Port) { result = Port { value = number(port) } }",
|
|
);
|
|
rejects("bad(value: Int) (result: Int >= 1) { result = value }");
|
|
accepts("valid() (result: Int >= 1) { result = 1 }");
|
|
}
|
|
|
|
#[test]
|
|
fn choice_payload_constraints_apply_at_construction_and_binding() {
|
|
rejects(
|
|
"type Result { Ready(value: Int >= 1) }\nbad() (result: Result) { result = Result.Ready(0) }",
|
|
);
|
|
accepts(
|
|
"type Result { Ready(value: Int >= 1) }\nread(result: Result.Ready(value)) (number: Int >= 1) { number = value }",
|
|
);
|
|
}
|
|
|
|
#[test]
|
|
fn nested_mutation_rechecks_constraints_and_aliases_keep_independent_facts() {
|
|
rejects(
|
|
"type Port { value: Int >= 1 }\ntype Config { port: Port }\nbad(config: Config) (result: Config) { config.port.value = 0\nresult = config }",
|
|
);
|
|
accepts(
|
|
"type Box { value: Int }\nmake() (result: Int >= 1) { original = Box { value = 1 }\nalias = original\noriginal.value = 0\nresult = alias.value }",
|
|
);
|
|
rejects(
|
|
"type Box { value: Int }\nmake() (result: Int >= 1) { original = Box { value = 1 }\noriginal.value = 0\nresult = original.value }",
|
|
);
|
|
}
|
|
|
|
#[test]
|
|
fn reassignment_removes_previous_range_guarantees() {
|
|
rejects(
|
|
"type Port { value: Int >= 1 }\nmake(input: Int) (port: Port) { value = 1\nvalue = input\nport = Port { value = value } }",
|
|
);
|
|
rejects(
|
|
"type Box { value: Int }\nmake(box: Box) (result: Int >= 1) { box.value = 0\nresult = box.value }",
|
|
);
|
|
}
|
|
|
|
#[test]
|
|
fn decimal_bounds_reuse_checked_numeric_semantics() {
|
|
accepts(
|
|
"type Amount { value: Decimal >= 0.0 and <= 10.0 }\nmake(value: Decimal >= 0.0 and <= 9.0) (result: Amount) { result = Amount { value = value + 1.0 } }\nmake(value: other) (result: Amount) { result = Amount { value = 0.0 } }",
|
|
);
|
|
rejects(
|
|
"type Amount { value: Decimal >= 0.0 }\nmake(value: Decimal) (result: Amount) { result = Amount { value = value } }",
|
|
);
|
|
}
|
|
|
|
#[test]
|
|
fn handler_inputs_use_declared_bounds_including_sequence_adapters() {
|
|
accepts(
|
|
"call(step: handler(value: Int >= 1) (result: Int >= 1)) (result: Int >= 1) { result = step(1) }",
|
|
);
|
|
rejects(
|
|
"call(step: handler(value: Int >= 1) (result: Int)) (result: Int) { result = step(0) }",
|
|
);
|
|
rejects("call(step: handler(value: Int >= 1) ()) () { each(step, [0]) }");
|
|
}
|
|
|
|
#[test]
|
|
fn proven_comparisons_and_call_domains_have_evidence_without_rejecting_callees() {
|
|
let program = checked("type Port { value: Int >= 1 }\npositive(value: Int >= 1) (result: Bool) { result = true }\npositive(value: other) (result: Bool) { result = false }\ncheck(port: Port) (result: Bool) { compared = port.value < 0\nresult = positive(port.value) and compared }").unwrap();
|
|
let warnings: Vec<_> = program
|
|
.warnings()
|
|
.iter()
|
|
.filter(|warning| warning.code == "W002")
|
|
.collect();
|
|
assert!(
|
|
warnings
|
|
.iter()
|
|
.any(|warning| warning.message.contains("comparison"))
|
|
);
|
|
assert!(
|
|
warnings
|
|
.iter()
|
|
.any(|warning| warning.message.contains("cannot run"))
|
|
);
|
|
assert!(warnings.iter().all(|warning| !warning.related.is_empty()));
|
|
accepts(
|
|
"positive(value: Int >= 1) (result: Bool) { result = true }\npositive(value: other) (result: Bool) { result = false }",
|
|
);
|
|
}
|
|
|
|
#[test]
|
|
fn constant_calls_and_unknown_comparisons_do_not_create_redundancy_noise() {
|
|
let mut sources = SourceMap::default();
|
|
let id = sources.add("main.dever", "positive(value: Int >= 1) (result: Bool) { result = true }\npositive(value: other) (result: Bool) { result = false }\nmain(value: Int) (result: Bool) { known = positive(1)\nresult = value < 0 and known }");
|
|
let program = dever_core::check(&sources).unwrap();
|
|
assert!(
|
|
!program
|
|
.warnings()
|
|
.iter()
|
|
.any(|warning| warning.code == "W002" && warning.primary.source == id)
|
|
);
|
|
}
|
|
|
|
#[test]
|
|
fn bool_null_and_choice_facts_reach_call_sites() {
|
|
let mut sources = SourceMap::default();
|
|
let id = sources.add("main.dever", "type Choice { Yes\nNo }\ntype State { enabled: Bool\nchoice: Choice\noptional: Int? }\nflag(value: true) () {}\nflag(value: false) () {}\noption(value: Int) () {}\noption(value: null) () {}\nchoose(value: Choice.Yes) () {}\nchoose(value: Choice.No) () {}\nmain() () { state = State { enabled = true\nchoice = Choice.Yes\noptional = null }\nflag(state.enabled)\noption(state.optional)\nchoose(state.choice) }");
|
|
let program = dever_core::check(&sources).unwrap();
|
|
let warnings: Vec<_> = program
|
|
.warnings()
|
|
.iter()
|
|
.filter(|warning| warning.code == "W002" && warning.primary.source == id)
|
|
.collect();
|
|
assert_eq!(warnings.len(), 3);
|
|
}
|
|
|
|
#[test]
|
|
fn arithmetic_does_not_assume_wrapping_or_unproved_division_bounds() {
|
|
rejects(
|
|
"type Positive { value: Int >= 1 }\nmake(input: Int) (result: Positive) { result = Positive { value = input + 1 } }",
|
|
);
|
|
rejects(
|
|
"type Positive { value: Int >= 1 }\nmake(input: Int) (result: Positive) { result = Positive { value = input // 2 } }",
|
|
);
|
|
}
|
|
|
|
#[test]
|
|
fn concrete_handler_outputs_are_proved_from_bodies_without_wrapper_annotations() {
|
|
accepts(
|
|
"apply(step: handler(value: Int >= 1) (result: Int >= 1)) (result: Int >= 1) { result = step(1) }\nidentity(value: Int) (result: Int) { result = value }\nmain() (result: Int >= 1) { result = apply(identity) }",
|
|
);
|
|
accepts(
|
|
"apply(step: handler(value: Int >= 1) (result: Int >= 1)) (result: Int >= 1) { result = step(1) }\ngood(value: Int) (result: Int) { result = 2 }\nmain() (result: Int >= 1) { result = apply(good) }",
|
|
);
|
|
rejects(
|
|
"apply(step: handler(value: Int >= 1) (result: Int >= 1)) (result: Int >= 1) { result = step(1) }\nbad(value: Int) (result: Int) { result = 0 }\nmain() (result: Int >= 1) { result = apply(bad) }",
|
|
);
|
|
}
|
|
|
|
#[test]
|
|
fn forwarded_handler_inputs_are_contravariant_and_outputs_covariant() {
|
|
accepts(
|
|
"apply(step: handler(value: Int >= 1) (result: Int >= 1)) (result: Int >= 1) { result = step(1) }\nforward(step: handler(value: Int >= 0) (result: Int >= 2)) (result: Int >= 1) { result = apply(step) }",
|
|
);
|
|
for signature in [
|
|
"handler(value: Int >= 2) (result: Int >= 1)",
|
|
"handler(value: Int >= 0) (result: Int >= 0)",
|
|
] {
|
|
let source = format!(
|
|
"apply(step: handler(value: Int >= 1) (result: Int >= 1)) (result: Int >= 1) {{ result = step(1) }}\nforward(step: {signature}) (result: Int >= 1) {{ result = apply(step) }}"
|
|
);
|
|
let errors = checked(&source).expect_err("unsafe handler variance");
|
|
assert!(
|
|
errors.iter().any(|error| error.code == "C005"),
|
|
"{errors:#?}"
|
|
);
|
|
}
|
|
}
|
|
|
|
#[test]
|
|
fn shared_value_graphs_keep_linear_facts_and_independent_mutation_snapshots() {
|
|
const DEPTH: usize = 24;
|
|
let mut declarations = String::from("type Layer0 { value: Int >= 1 }\n");
|
|
for level in 1..=DEPTH {
|
|
declarations.push_str(&format!(
|
|
"type Layer{level} {{ left: Layer{}\nright: Layer{} }}\n",
|
|
level - 1,
|
|
level - 1
|
|
));
|
|
}
|
|
for (flag, initial) in [("true", 1), ("false", 2)] {
|
|
declarations.push_str(&format!(
|
|
"build(flag: {flag}) (result: Layer{DEPTH}) {{\nv0 = Layer0 {{ value = {initial} }}\n"
|
|
));
|
|
for level in 1..=DEPTH {
|
|
declarations.push_str(&format!(
|
|
"v{level} = Layer{level} {{ left = v{}\nright = v{} }}\n",
|
|
level - 1,
|
|
level - 1
|
|
));
|
|
}
|
|
declarations.push_str(&format!("result = v{DEPTH}\n}}\n"));
|
|
}
|
|
let path = format!("{}value", "left.".repeat(DEPTH));
|
|
declarations.push_str(&format!("main() (result: Int >= 1 and <= 2) {{ value = build(true)\nalias = value\nvalue.{path} = 3\nresult = alias.{path}\n}}"));
|
|
accepts(&declarations);
|
|
let mutated = declarations.replace(
|
|
&format!("result = alias.{path}"),
|
|
&format!("result = value.{path}"),
|
|
);
|
|
rejects(&mutated);
|
|
}
|
|
|
|
#[test]
|
|
fn excessive_fact_work_is_an_explicit_diagnostic() {
|
|
// A broad but shallow source exercises the budget without allocating an
|
|
// exponentially nested value or risking the host process's memory.
|
|
let mut declarations = String::from("main(input: Int) (result: Int) {\n");
|
|
for _ in 0..5500 {
|
|
declarations.push_str("result = input + 1\n");
|
|
}
|
|
declarations.push('}');
|
|
let errors = checked(&declarations).expect_err("proof budget must be enforced");
|
|
assert!(
|
|
errors.iter().any(|error| error.code == "C015"),
|
|
"{errors:#?}"
|
|
);
|
|
}
|