diff options
Diffstat (limited to '')
| -rw-r--r-- | docs/core-design-and-pipeline.org | 17 | ||||
| -rw-r--r-- | docs/virtual-machine-specification.org | 7 | ||||
| -rw-r--r-- | docs/vm.org | 16 | ||||
| -rw-r--r-- | lib/vm.ml | 239 | ||||
| -rw-r--r-- | test/test_embedding.ml | 5 | ||||
| -rw-r--r-- | test/test_vm.ml | 54 |
6 files changed, 313 insertions, 25 deletions
diff --git a/docs/core-design-and-pipeline.org b/docs/core-design-and-pipeline.org index 823a24e..c81b58a 100644 --- a/docs/core-design-and-pipeline.org +++ b/docs/core-design-and-pipeline.org @@ -111,13 +111,18 @@ two of the ladder in decision 10: with every measure position demanded ground at unfolding; self recursion and mutual recursion are the same check; - bounded enumeration through =Between=; -- decidable negation and universals only over decidable quantifiers; +- decidable negation and universals over decidable quantifiers; - residuation: open membership returns as residual constraints - instead of failing the plan. - -Not yet present: symbolic discharge (algebraic proof of universals -over infinite domains), Rocq certificates as admission evidence, and -active constraint propagation over residue. Each arrives as a + instead of failing the plan; +- interval propagation over residue: contradictions fail, finite + integer ranges enumerate; +- symbolic discharge, first fragment: universals over infinite + domains decided by kind inclusion and interval entailment, with + refutations backed by counterexamples. + +Not yet present: symbolic discharge beyond the interval fragment +(algebraic identities of relations, arithmetic decrease measures) +and Rocq certificates as admission evidence. Each arrives as a strengthening of admission or planning; none changes the semantics of what is already admitted. diff --git a/docs/virtual-machine-specification.org b/docs/virtual-machine-specification.org index 828bc3c..f84bc84 100644 --- a/docs/virtual-machine-specification.org +++ b/docs/virtual-machine-specification.org @@ -135,9 +135,10 @@ without changing admitted semantics: one-sided comparisons; difference constraints between variables, arithmetic relations, and propagation through record structure are the next strengths; -- symbolic discharge: algebraic evidence for universals over - infinite domains, and arithmetic decrease measures for recursion - that structural containment cannot see; +- symbolic discharge beyond the interval fragment: algebraic + identities of relations (universals mentioning =Plus= and kin), + and arithmetic decrease measures for recursion that structural + containment cannot see; - Rocq certificates as admission evidence, and extraction of the lexicographic search itself (the containment core is already extracted); diff --git a/docs/vm.org b/docs/vm.org index 446cee2..a51b85a 100644 --- a/docs/vm.org +++ b/docs/vm.org @@ -96,10 +96,18 @@ open goals cannot happen. =Exists= lowers to a conjunction at loading, since query variables are existential already; its =variable:= is renamed apart so the scope cannot be forged. =ForAll= runs when its quantifier is -decidable: every solution of the quantifier must satisfy the body. A -universal over an infinite domain is a non total plan, rejected, as -decision 10 requires. Variables that live only under a universal are -not answer variables. +decidable: every solution of the quantifier must satisfy the body. +Variables that live only under a universal are not answer variables. + +A universal over an infinite domain is never enumerated. It gets one +chance at symbolic discharge: when quantifier and body both read as +kind and interval constraints over the quantified variable, the +engine decides entailment algebraically. Every natural is at least +zero: proven. Not every integer is: refuted, and the refutation is +backed by a concrete counterexample. Every integer is a rational: +proven, which is decision 12's subtype inclusion decided +symbolically. A universal outside that fragment is a non total plan, +rejected, as decision 10 requires. * Membership criteria as domains @@ -236,6 +236,217 @@ module Make (W : World.WORLD) = struct | None -> Unknown end + (* Symbolic discharge (decision 10, rung three, first fragment): + universals whose quantifier is an infinite domain are decided + algebraically when quantifier and body both read as kind and + interval constraints over the one quantified variable. Holds + means every member is covered; Fails is always backed by a + concrete counterexample; anything outside the fragment stays + deferred. Subtype inclusions (a Natural is an Integer is a + Rational) are decided here, literally, per decision 12. *) + module Symbolic = struct + type side = { + is_int : bool; (** members are integers *) + is_str : bool; + has_domain : bool; (** some domain goal declared the kind *) + lower : Propagate.bound option; + upper : Propagate.bound option; + } + + let free = { is_int = false; is_str = false; has_domain = false; lower = None; upper = None } + + (* One goal read as a constraint on [var]; None = outside the + fragment. Goals without variables evaluate outright. *) + let read subst var side (name, bindings) = + let value = Label.Map.find_opt Propagate.value_l bindings + and left = Label.Map.find_opt Propagate.left_l bindings + and right = Label.Map.find_opt Propagate.right_l bindings in + let ground_goal () = + match Builtin.run subst name bindings with + | Some (Builtin.Solved []) -> Some `Contradiction + | Some (Builtin.Solved _) -> Some `Trivial + | _ -> None + in + let is_var = function + | Pattern.Var v -> String.equal v var + | _ -> false + in + match (name, value, left, right) with + | ("Integer" | "Natural"), Some v, _, _ when is_var v -> + let side = { side with is_int = true; has_domain = true } in + if String.equal name "Natural" then + Some + (`Side + { + side with + lower = + Some + (match side.lower with + | None -> { Propagate.value = Q.zero; strict = false } + | Some b -> + Propagate.stronger_lower b + { Propagate.value = Q.zero; strict = false }); + }) + else Some (`Side side) + | "Rational", Some v, _, _ when is_var v -> + Some (`Side { side with has_domain = true }) + | "String", Some v, _, _ when is_var v -> + Some (`Side { side with is_str = true; has_domain = true }) + | ( ("LessThan" | "LessThanEqual" | "GreaterThan" | "GreaterEqual"), + _, + Some l, + Some r ) -> ( + let strict = + String.equal name "LessThan" || String.equal name "GreaterThan" + in + let less = + String.equal name "LessThan" || String.equal name "LessThanEqual" + in + let with_bound upper bound = + if upper then + `Side + { + side with + upper = + Some + (match side.upper with + | None -> bound + | Some b -> Propagate.stronger_upper b bound); + } + else + `Side + { + side with + lower = + Some + (match side.lower with + | None -> bound + | Some b -> Propagate.stronger_lower b bound); + } + in + match (l, r) with + | v, g when is_var v && Option.is_some (Propagate.numeric_value g) -> + Some + (with_bound less + { Propagate.value = Option.get (Propagate.numeric_value g); strict }) + | g, v when is_var v && Option.is_some (Propagate.numeric_value g) -> + Some + (with_bound (not less) + { Propagate.value = Option.get (Propagate.numeric_value g); strict }) + | _ -> None) + | _, _, _, _ -> + if + Label.Map.for_all + (fun _ p -> Pattern.vars p = []) + bindings + then ground_goal () + else None + + let read_side subst var goals = + List.fold_left + (fun acc goal -> + match acc with + | None | Some `Contradiction -> acc + | Some (`Side side) -> ( + match read subst var side goal with + | Some (`Side _ as s) -> Some s + | Some `Trivial -> Some (`Side side) + | Some `Contradiction -> Some `Contradiction + | None -> None)) + (Some (`Side free)) goals + + (* Does the quantifier's lower bound guarantee the body's? For + integer kinds compare tightened endpoints; missing body bound + is no demand, missing quantifier bound cannot guarantee one. *) + let lower_entails ~int q b = + match b with + | None -> true + | Some b -> ( + match q with + | None -> false + | Some q -> + if int then Z.geq (Propagate.lower_int q) (Propagate.lower_int b) + else + Q.gt q.Propagate.value b.Propagate.value + || (Q.equal q.Propagate.value b.Propagate.value + && ((not b.strict) || q.strict))) + + let upper_entails ~int q b = + match b with + | None -> true + | Some b -> ( + match q with + | None -> false + | Some q -> + if int then Z.leq (Propagate.upper_int q) (Propagate.upper_int b) + else + Q.lt q.Propagate.value b.Propagate.value + || (Q.equal q.Propagate.value b.Propagate.value + && ((not b.strict) || q.strict))) + + (* A rational interval that is one integer point. *) + let single_integer_point q = + match (q.lower, q.upper) with + | Some lo, Some hi -> + (not lo.Propagate.strict) + && (not hi.Propagate.strict) + && Q.equal lo.value hi.value + && Z.equal (Q.den lo.value) Z.one + | _ -> false + + let entails q b = + if q.is_str then + if b.is_int || b.lower <> None || b.upper <> None then `Fails + else `Holds + else if b.is_str then `Fails + else if b.is_int && (not q.is_int) && not (single_integer_point q) then + `Fails + else if + lower_entails ~int:q.is_int q.lower b.lower + && upper_entails ~int:q.is_int q.upper b.upper + then `Holds + else `Fails + + let discharge subst quantifier_goals body_goals = + let apply_only goals = + List.fold_left + (fun acc goal -> + Option.bind acc (fun goals -> + match goal with + | World.Apply (name, bindings) -> + Some + ((name, Label.Map.map (Pattern.Subst.resolve subst) bindings) + :: goals) + | _ -> None)) + (Some []) goals + in + match (apply_only quantifier_goals, apply_only body_goals) with + | Some quantifier, Some body -> ( + let vars = + List.concat_map + (fun (_, bindings) -> + Label.Map.fold (fun _ p acc -> acc @ Pattern.vars p) bindings []) + quantifier + |> List.sort_uniq String.compare + in + match vars with + | [ var ] -> ( + match (read_side subst var quantifier, read_side subst var body) with + | Some (`Side q), Some (`Side b) -> + if q.has_domain then entails q b else `Unknown + | Some (`Side q), Some `Contradiction -> + (* The body is falsified outright; any member of a + nonempty quantifier is a counterexample. *) + if q.has_domain then `Fails else `Unknown + | Some `Contradiction, _ -> + (* An empty quantifier satisfies any universal. *) + `Holds + | _ -> `Unknown) + | _ -> `Unknown) + | _ -> `Unknown + end + + let rec try_goal world subst goal = match goal with | Negated denial -> @@ -252,15 +463,31 @@ module Make (W : World.WORLD) = struct Run [ (subst, flatten a); (subst, flatten b) ] | Positive ((World.And _ | World.Not _) as expr) -> Run [ (subst, flatten expr) ] | Positive (World.Forall (quantifier, body)) -> ( - (* Universal over the quantifier's solutions. Runs only when - the quantifier is decidable and closed; an undetermined - quantifier or body defers the universal, and an infinite - one therefore never runs. *) + (* Universal over the quantifier's solutions. Runs when the + quantifier is decidable and closed; otherwise symbolic + discharge gets a chance before the universal defers, so + truths over infinite domains are proven, never + enumerated. *) + let rec conjuncts = function + | World.And (a, b) -> conjuncts a @ conjuncts b + | expr -> [ expr ] + in + let symbolically () = + match + Symbolic.discharge subst (conjuncts quantifier) (conjuncts body) + with + | `Holds -> Run [ (subst, []) ] + | `Fails -> Run [] + | `Unknown -> Wait { residuatable = false } + in match search world subst (flatten quantifier) with - | exception Stuck _ -> Wait { residuatable = false } + | exception Stuck _ -> symbolically () | quantified -> if List.exists (fun (_, residue) -> residue <> []) quantified then - Wait { residuatable = false } + (* The quantifier residuated: an infinite or + underdetermined domain. Enumeration is off the + table; proof is not. *) + symbolically () else let body_status (s, _) = match search world s (flatten body) with diff --git a/test/test_embedding.ml b/test/test_embedding.ml index ea55e4f..a2eab95 100644 --- a/test/test_embedding.ml +++ b/test/test_embedding.ml @@ -66,9 +66,12 @@ let test_kernel_scan () = | Error error -> Alcotest.failf "solve error: %a" Sol.Vm.pp_error error let test_kernel_totality () = + (* A universal over an infinite domain whose body the symbolic + fragment cannot read: neither enumerable nor provable, so it + must be rejected, embedding or not. *) match solve - {| [ForAll variable: X quantifier: [Integer value: X] body: [True]] |} + {| [ForAll variable: X quantifier: [Integer value: X] body: [Sensor id: X]] |} with | Error (Sol.Vm.Non_total_plan _) -> () | Ok _ -> Alcotest.fail "the embedded engine must keep the totality guard" diff --git a/test/test_vm.ml b/test/test_vm.ml index f3d8484..16ca63c 100644 --- a/test/test_vm.ml +++ b/test/test_vm.ml @@ -263,13 +263,47 @@ let test_forall_fails () = | [ _ :: _ ] -> Alcotest.fail "the universal must fail: Ana is 12" | _ -> Alcotest.fail "expected one query" -let test_forall_over_infinite_rejected () = - match load {| Query expression: [ForAll variable: X quantifier: [Integer value: X] body: [True]] |} with +let holds source = count_solutions source = 1 + +(* Symbolic discharge: the specification's own two examples, decided + without enumerating anything. *) + +let test_symbolic_naturals_nonnegative () = + Alcotest.(check bool) "every natural is at least zero" true + (holds + {| Query expression: [ForAll variable: X quantifier: [Natural value: X] body: [GreaterEqual left: X right: 0]] |}) + +let test_symbolic_integers_not_nonnegative () = + Alcotest.(check bool) "not every integer is at least zero" false + (holds + {| Query expression: [ForAll variable: X quantifier: [Integer value: X] body: [GreaterEqual left: X right: 0]] |}) + +let test_symbolic_inclusion () = + (* Decision 12: subtype inclusion, decided symbolically. *) + Alcotest.(check bool) "every integer is a rational" true + (holds + {| Query expression: [ForAll variable: X quantifier: [Integer value: X] body: [Rational value: X]] |}); + Alcotest.(check bool) "not every rational is an integer" false + (holds + {| Query expression: [ForAll variable: X quantifier: [Rational value: X] body: [Integer value: X]] |}) + +let test_symbolic_interval_entailment () = + Alcotest.(check bool) "naturals from ten upward exceed five" true + (holds + {| Query expression: [ForAll variable: X quantifier: ([Natural value: X] :and [GreaterEqual left: X right: 10]) body: [GreaterThan left: X right: 5]] |}) + +let test_forall_outside_fragment_still_rejected () = + match + load + {| Query expression: [ForAll variable: X quantifier: [Integer value: X] body: [Equal left: X right: 5]] |} + with | Error error -> Alcotest.failf "load error: %a" Sol.Program.pp_error error | Ok (world, [ query ]) -> ( match Sol.Vm.Standalone.solve world query with | Error (Sol.Vm.Non_total_plan _) -> () - | Ok _ -> Alcotest.fail "a universal over an infinite domain must be rejected") + | Ok _ -> + Alcotest.fail + "a universal the symbolic fragment cannot read must still be rejected") | Ok _ -> Alcotest.fail "expected one query" let test_exists () = @@ -444,10 +478,20 @@ let () = [ Alcotest.test_case "forall holds" `Quick test_forall_holds; Alcotest.test_case "forall fails" `Quick test_forall_fails; - Alcotest.test_case "forall over infinite rejected" `Quick - test_forall_over_infinite_rejected; Alcotest.test_case "exists" `Quick test_exists; ] ); + ( "symbolic", + [ + Alcotest.test_case "naturals nonnegative" `Quick + test_symbolic_naturals_nonnegative; + Alcotest.test_case "integers not nonnegative" `Quick + test_symbolic_integers_not_nonnegative; + Alcotest.test_case "inclusion" `Quick test_symbolic_inclusion; + Alcotest.test_case "interval entailment" `Quick + test_symbolic_interval_entailment; + Alcotest.test_case "outside fragment still rejected" `Quick + test_forall_outside_fragment_still_rejected; + ] ); ( "criteria", [ Alcotest.test_case "criterion admits" `Quick test_criterion_admits; |