From 31596491f0d2096daf5b253820adac3c690b4c4c Mon Sep 17 00:00:00 2001 From: imiel Date: Mon, 27 Apr 2026 12:51:47 +0000 Subject: [PATCH] extend source and target calculi with observable tick effects + add invariant checks for relation preservation and target arity/shape --- README.md | 5 +- bin/main.ml | 19 +++++-- src/audit.ml | 135 ++++++++++++++++++++++++++++++++++++++++++++- src/audit.mli | 27 ++++++++- src/corpus.ml | 19 ++++++- src/gen.ml | 4 ++ src/pipeline.ml | 54 ++++++++++++++++-- src/pipeline.mli | 4 +- src/relation.ml | 25 +++++++-- src/relation.mli | 3 +- src/reporting.ml | 22 +++++++- src/reporting.mli | 3 + src/source.ml | 44 ++++++++++++--- src/source.mli | 2 + src/target.ml | 55 +++++++++++++++--- src/target.mli | 2 + src/typecheck.ml | 2 +- test/invariants.ml | 14 ++++- 18 files changed, 395 insertions(+), 44 deletions(-) diff --git a/README.md b/README.md index 22f48c2..b5439e0 100644 --- a/README.md +++ b/README.md @@ -8,6 +8,10 @@ the target language makes representation explicit and forces each transition to the target calculus is intentionally lower level than the source and trades abstraction for control over layout and calling. it has decent tuple and sum representations and uses explicit box and unbox operations to mediate between them. equality on integers and booleans is primitive rather than encoded as well as recursive binding being built in rather than derived +the audit path now records pass-boundary observations for source, specialisation, inlining, effect rewriting, and representation lowering. each corpus case is checked against relation preservation, target arity/shape validation, termination class preservation, and effect trace preservation. unsafe profiles intentionally refute these invariants so optimiser bugs show up as small source/target deltas rather than vague failures. + +the source calculus also has an explicit `tick` effect. this is enough to expose unsound dce-style rewrites: eliminating a dead binding is only valid when the eliminated term is effect free. + ## example(s) a representation exposure witness starts from a polymorphic constant false term @@ -33,4 +37,3 @@ TArrow (TPair (TInt, TBool), TPair (TInt, TBool)) ``` the target worker receives `RInt` and `RBool` while the wrapper preserves the boxed source interface - diff --git a/bin/main.ml b/bin/main.ml index 71bfdaa..8e3edba 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -7,7 +7,7 @@ type profile = { } let safe_flags = - { Pipeline.default_flags with unsafe_repr_eq = false; unsafe_strict_unroll = false } + { Pipeline.default_flags with unsafe_repr_eq = false; unsafe_strict_unroll = false; unsafe_effect_drop = false } let profiles = [ @@ -17,17 +17,28 @@ let profiles = { name = "unsafe-inline"; flags = { safe_flags with unsafe_repr_eq = true }; relation = Relation.Boxed_unboxed }; { name = "unsafe-unbox"; flags = Pipeline.default_flags; relation = Relation.Boxed_unboxed }; { name = "unsafe-strictness"; flags = { safe_flags with inline = false; unsafe_strict_unroll = true }; relation = Relation.Boxed_unboxed }; + { name = "unsafe-effects"; flags = { safe_flags with unsafe_effect_drop = true }; relation = Relation.Boxed_unboxed }; ] let run_case (case : Corpus.case) = let audit = Audit.audit_case case in + let failed_invariants = + audit.Audit.invariants + |> List.filter (fun result -> not result.Audit.passed) + |> List.map (fun result -> Audit.invariant_kind_to_string result.Audit.kind) + in Printf.printf - "case %s\nclassification %s\nverdict %s\nsource %s\ntarget %s\n\n" + "case %s\nclassification %s\nverdict %s\nsource %s\ntarget %s\nfailed invariants %s\n\n" case.Corpus.name (Audit.failure_mode_to_string audit.Audit.failure_mode) (Reporting.verdict_to_string audit.Audit.comparison.Relation.verdict) - (Reporting.string_of_source_outcome audit.Audit.source_trace.Source.outcome) - (Reporting.string_of_target_outcome audit.Audit.target_trace.Target.outcome) + (Reporting.string_of_source_trace audit.Audit.source_trace) + (Reporting.string_of_target_trace audit.Audit.target_trace) + (if failed_invariants = [] then "none" else String.concat ", " failed_invariants); + if audit.Audit.failure_mode <> Audit.Preserved then begin + Printf.printf "%s\n\n" (Reporting.emit_pipeline_visualisation audit.Audit.compiled); + Printf.printf "%s\n\n" (Audit.emit_pass_boundaries audit) + end let run_profile profile = let result = Gen.run_campaign profile.flags profile.relation ~count:160 ~max_depth:4 () in diff --git a/src/audit.ml b/src/audit.ml index 1f2c885..06a277c 100644 --- a/src/audit.ml +++ b/src/audit.ml @@ -2,9 +2,30 @@ type failure_mode = | Preserved | Representation_exposure | Strictness_shift + | Effect_shift | Type_error of string | Other_failure of string +type invariant_kind = + | Relation_preservation + | Target_arity + | Termination_class + | Effect_trace + +type invariant_result = { + kind : invariant_kind; + passed : bool; + detail : string; +} + +type pass_boundary = { + pass : string; + source_outcome : Source.outcome option; + target_outcome : Target.outcome option; + effects : int; + verdict : string; +} + type obligation_status = | Discharged | Assumed @@ -27,15 +48,24 @@ type case_audit = { typecheck : (unit, string) result; failure_mode : failure_mode; obligations : obligation_result list; + invariants : invariant_result list; + pass_boundaries : pass_boundary list; } let failure_mode_to_string = function | Preserved -> "preserved" | Representation_exposure -> "representation_exposure" | Strictness_shift -> "strictness_shift" + | Effect_shift -> "effect_shift" | Type_error msg -> "type_error " ^ msg | Other_failure msg -> "other_failure " ^ msg +let invariant_kind_to_string = function + | Relation_preservation -> "relation_preservation" + | Target_arity -> "target_arity" + | Termination_class -> "termination_class" + | Effect_trace -> "effect_trace" + let obligation_status_to_string = function | Discharged -> "discharged" | Assumed -> "assumed" @@ -50,6 +80,8 @@ let classify validation compiled comparison = | Ok () -> begin match comparison.Relation.verdict with | Relation.Related -> Preserved + | Relation.Unrelated msg when String.equal msg "effect trace changed" -> Effect_shift + | Relation.Unrelated msg when String.equal msg "effect trace changed before divergence" -> Effect_shift | Relation.Unrelated msg when has_obligation Pipeline.Exposed_representation compiled.Pipeline.obligations -> Representation_exposure | Relation.Unrelated msg when String.equal msg "target diverged where source terminated" -> @@ -69,6 +101,8 @@ let status_for_obligation failure_mode (obligation : Pipeline.obligation) = { obligation; status = Refuted; note = "counterexample exposes a representation specific equality primitive" } | Strictness_shift, Pipeline.Strictness_risk -> { obligation; status = Refuted; note = "counterexample changes termination by forcing a recursive payload" } + | Effect_shift, Pipeline.Effect_observation -> + { obligation; status = Refuted; note = "counterexample changes the observable effect trace" } | Type_error msg, _ -> { obligation; status = Refuted; note = "program failed validation: " ^ msg } | Other_failure msg, _ -> @@ -81,6 +115,65 @@ let status_for_obligation failure_mode (obligation : Pipeline.obligation) = { obligation; status = Assumed; note = "unsafe inlining may expose representation observers" } | _, Pipeline.Strictness_risk -> { obligation; status = Assumed; note = "unsafe lowering may shift strictness" } + | _, Pipeline.Effect_observation -> + { obligation; status = Assumed; note = "effectful source terms require effect preservation" } + +let same_termination_class source target = + match source, target with + | Source.Value _, Target.Value _ -> true + | Source.Diverged _, Target.Diverged _ -> true + | Source.Stuck _, Target.Stuck _ -> true + | _ -> false + +let invariant_result kind passed detail = { kind; passed; detail } + +let check_invariants comparison source_trace target_trace target_program = + let target_validation = Target.validate target_program in + [ + invariant_result + Relation_preservation + (comparison.Relation.verdict = Relation.Related) + (Reporting.verdict_to_string comparison.Relation.verdict); + invariant_result + Target_arity + (match target_validation with Ok () -> true | Error _ -> false) + (match target_validation with Ok () -> "target IR validates" | Error errors -> String.concat "; " errors); + invariant_result + Termination_class + (same_termination_class source_trace.Source.outcome target_trace.Target.outcome) + (Reporting.string_of_source_outcome source_trace.Source.outcome ^ " / " ^ + Reporting.string_of_target_outcome target_trace.Target.outcome); + invariant_result + Effect_trace + (source_trace.Source.effects = target_trace.Target.effects) + ("source effects " ^ string_of_int source_trace.Source.effects ^ + ", target effects " ^ string_of_int target_trace.Target.effects); + ] + +let pass_boundaries compiled target_trace = + let source_boundary pass term = + let trace = Source.evaluate term in + { + pass; + source_outcome = Some trace.Source.outcome; + target_outcome = None; + effects = trace.Source.effects; + verdict = Reporting.string_of_source_trace trace; + } + in + [ + source_boundary "source" compiled.Pipeline.source_program; + source_boundary "specialise" compiled.Pipeline.specialised; + source_boundary "inline" compiled.Pipeline.inlined; + source_boundary "effect" compiled.Pipeline.effect_rewritten; + { + pass = "repr_lower"; + source_outcome = None; + target_outcome = Some target_trace.Target.outcome; + effects = target_trace.Target.effects; + verdict = Reporting.string_of_target_trace target_trace; + }; + ] let audit_case (case : Corpus.case) = let compiled = Pipeline.compile case.Corpus.flags case.Corpus.ty case.Corpus.source in @@ -95,6 +188,8 @@ let audit_case (case : Corpus.case) = { Relation.source_outcome = source_trace.Source.outcome; target_outcome = Target.Stuck ("invalid target IR: " ^ String.concat "; " errors); + source_effects = source_trace.Source.effects; + target_effects = 0; verdict = Relation.Unrelated "invalid target IR"; } in @@ -105,6 +200,7 @@ let audit_case (case : Corpus.case) = { Target.steps = [compiled.Pipeline.target_program]; outcome = Target.Stuck ("invalid target IR: " ^ String.concat "; " errors); + effects = 0; } in let typecheck = Typecheck.check case.Corpus.ty case.Corpus.source in @@ -116,7 +212,9 @@ let audit_case (case : Corpus.case) = in let failure_mode = classify validation compiled comparison in let obligations = List.map (status_for_obligation failure_mode) compiled.Pipeline.obligations in - { case; compiled; comparison; source_trace; specialised_trace; inlined_trace; target_trace; typecheck; failure_mode; obligations } + let invariants = check_invariants comparison source_trace target_trace compiled.Pipeline.target_program in + let pass_boundaries = pass_boundaries compiled target_trace in + { case; compiled; comparison; source_trace; specialised_trace; inlined_trace; target_trace; typecheck; failure_mode; obligations; invariants; pass_boundaries } let source_outcome trace = Reporting.string_of_source_outcome trace.Source.outcome let target_outcome trace = Reporting.string_of_target_outcome trace.Target.outcome @@ -126,6 +224,33 @@ let emit_obligation_result result = "| `" ^ o.Pipeline.pass ^ "` | `" ^ Reporting.obligation_kind_to_string o.Pipeline.kind ^ "` | `" ^ obligation_status_to_string result.status ^ "` | " ^ result.note ^ " |" +let emit_invariant_result result = + "| `" ^ invariant_kind_to_string result.kind ^ "` | `" ^ + (if result.passed then "ok" else "failed") ^ "` | " ^ result.detail ^ " |" + +let emit_boundary boundary = + "| `" ^ boundary.pass ^ "` | `" ^ boundary.verdict ^ "` |" + +let emit_invariants audit = + String.concat "\n" + ([ + "### invariants"; + ""; + "| invariant | status | detail |"; + "| --- | --- | --- |"; + ] + @ List.map emit_invariant_result audit.invariants) + +let emit_pass_boundaries audit = + String.concat "\n" + ([ + "### pass boundaries"; + ""; + "| pass | observation |"; + "| --- | --- |"; + ] + @ List.map emit_boundary audit.pass_boundaries) + let emit_case_audit audit = let typecheck = match audit.typecheck with @@ -144,6 +269,14 @@ let emit_case_audit audit = "| specialised | `" ^ source_outcome audit.specialised_trace ^ "` |"; "| inlined | `" ^ source_outcome audit.inlined_trace ^ "` |"; "| target | `" ^ target_outcome audit.target_trace ^ "` |"; + "| source effects | `" ^ string_of_int audit.source_trace.Source.effects ^ "` |"; + "| target effects | `" ^ string_of_int audit.target_trace.Target.effects ^ "` |"; + ""; + Reporting.emit_pipeline_visualisation audit.compiled; + ""; + emit_pass_boundaries audit; + ""; + emit_invariants audit; ""; "### obligation ledger"; ""; diff --git a/src/audit.mli b/src/audit.mli index 667f212..4868a85 100644 --- a/src/audit.mli +++ b/src/audit.mli @@ -2,9 +2,30 @@ type failure_mode = | Preserved | Representation_exposure | Strictness_shift + | Effect_shift | Type_error of string | Other_failure of string +type invariant_kind = + | Relation_preservation + | Target_arity + | Termination_class + | Effect_trace + +type invariant_result = { + kind : invariant_kind; + passed : bool; + detail : string; +} + +type pass_boundary = { + pass : string; + source_outcome : Source.outcome option; + target_outcome : Target.outcome option; + effects : int; + verdict : string; +} + type obligation_status = | Discharged | Assumed @@ -27,11 +48,15 @@ type case_audit = { typecheck : (unit, string) result; failure_mode : failure_mode; obligations : obligation_result list; + invariants : invariant_result list; + pass_boundaries : pass_boundary list; } val audit_case : Corpus.case -> case_audit val failure_mode_to_string : failure_mode -> string val obligation_status_to_string : obligation_status -> string +val invariant_kind_to_string : invariant_kind -> string +val emit_pass_boundaries : case_audit -> string +val emit_invariants : case_audit -> string val emit_case_audit : case_audit -> string val emit_matrix : case_audit list -> string - diff --git a/src/corpus.ml b/src/corpus.ml index 886566b..c79df31 100644 --- a/src/corpus.ml +++ b/src/corpus.ml @@ -13,10 +13,13 @@ type case = { let default = Pipeline.default_flags let safer = - { default with unsafe_repr_eq = false; unsafe_strict_unroll = false } + { default with unsafe_repr_eq = false; unsafe_strict_unroll = false; unsafe_effect_drop = false } let strictness_flags = - { default with inline = false; unsafe_repr_eq = false; unsafe_strict_unroll = true } + { default with inline = false; unsafe_repr_eq = false; unsafe_strict_unroll = true; unsafe_effect_drop = false } + +let effect_flags = + { safer with unsafe_effect_drop = true } let poly_const_false = Source.TyLam ("a", Source.Lam ("x", TVar "a", TArrow (TVar "a", TBool), Source.Lam ("y", TVar "a", TBool, Source.Bool false))) @@ -42,6 +45,9 @@ let pair_sum_roundtrip = ("p", Source.LetPair ("n", "b", Source.Var "p", Source.If (Source.Var "b", Source.Var "n", Source.Int 0))), ("k", Source.Var "k") ) +let effectful_dead_let = + Source.Let ("_", Source.Tick ("alloc", Source.Int 0), Source.Int 1) + let boxed_pair_projection = Source.App ( Source.Lam @@ -121,4 +127,13 @@ let all = flags = strictness_flags; relation = Relation.Boxed_unboxed; }; + { + name = "effect-elision-breaks-observation"; + summary = "drop an effectful dead binding during source simplification"; + claim = "DCE is only valid when the eliminated term is effect free"; + ty = TInt; + source = effectful_dead_let; + flags = effect_flags; + relation = Relation.Boxed_unboxed; + }; ] diff --git a/src/gen.ml b/src/gen.ml index a2c3e0f..94dc08f 100644 --- a/src/gen.ml +++ b/src/gen.ml @@ -85,6 +85,10 @@ let sample_terms ~count ~max_depth () = Source.Fix ("loop", TInt, Source.Var "loop") ), Source.Int 0 ); }; + { + ty = TInt; + term = Source.Let ("_", Source.Tick ("alloc", Source.Int 0), Source.Int 1); + }; ] in let rec fill acc i attempts = diff --git a/src/pipeline.ml b/src/pipeline.ml index cdb5d31..558946a 100644 --- a/src/pipeline.ml +++ b/src/pipeline.ml @@ -6,12 +6,14 @@ type optimisation_flags = { repr_lower : bool; unsafe_repr_eq : bool; unsafe_strict_unroll : bool; + unsafe_effect_drop : bool; } type obligation_kind = | Preserve_relation | Exposed_representation | Strictness_risk + | Effect_observation | Worker_wrapper_proof type obligation = { @@ -26,6 +28,7 @@ type compiled = { source_program : Source.term; specialised : Source.term; inlined : Source.term; + effect_rewritten : Source.term; target_program : Target.term; obligations : obligation list; } @@ -37,6 +40,7 @@ let default_flags = repr_lower = true; unsafe_repr_eq = true; unsafe_strict_unroll = true; + unsafe_effect_drop = true; } let obligation ?(kind = Preserve_relation) pass subject detail = @@ -52,10 +56,22 @@ let rec inline_cost = function | Source.Fix (_, _, body) -> 2 + inline_cost body | Source.Eq (_, a, b) -> 1 + inline_cost a + inline_cost b | Source.If (c, t, e) -> 1 + inline_cost c + inline_cost t + inline_cost e + | Source.Tick (_, t) -> 1 + inline_cost t | Source.Let (_, a, b) -> inline_cost a + inline_cost b | Source.LetPair (_, _, a, b) -> 1 + inline_cost a + inline_cost b | Source.Case (s, (_, l), (_, r)) -> 1 + inline_cost s + inline_cost l + inline_cost r +let rec contains_tick = function + | Source.Tick _ -> true + | Source.Pair (a, b) | Source.App (a, b) | Source.Eq (_, a, b) -> contains_tick a || contains_tick b + | Source.Inl (_, t) | Source.Inr (_, t) | Source.Roll (_, t) | Source.Unroll t -> contains_tick t + | Source.Lam (_, _, _, body) | Source.TyLam (_, body) | Source.Fix (_, _, body) -> contains_tick body + | Source.TyApp (t, _) -> contains_tick t + | Source.If (c, t, e) -> contains_tick c || contains_tick t || contains_tick e + | Source.Let (_, a, b) | Source.LetPair (_, _, a, b) -> contains_tick a || contains_tick b + | Source.Case (s, (_, l), (_, r)) -> contains_tick s || contains_tick l || contains_tick r + | Source.Var _ | Source.Int _ | Source.Bool _ -> false + let rec inline_term note unsafe_repr_eq term = match term with | Source.App (Source.Lam (x, _, _, body), arg) when inline_cost body <= 8 -> @@ -95,10 +111,11 @@ let rec inline_term note unsafe_repr_eq term = | Source.Eq (g, a, b) -> Source.Eq (g, inline_term note unsafe_repr_eq a, inline_term note unsafe_repr_eq b) | Source.If (c, t, e) -> Source.If (inline_term note unsafe_repr_eq c, inline_term note unsafe_repr_eq t, inline_term note unsafe_repr_eq e) + | Source.Tick (label, t) -> Source.Tick (label, inline_term note unsafe_repr_eq t) | Source.Let (x, a, b) -> let a' = inline_term note unsafe_repr_eq a in let b' = inline_term note unsafe_repr_eq b in - if inline_cost a' <= 4 then begin + if inline_cost a' <= 4 && not (contains_tick a') then begin note Preserve_relation "let inlining" ("inlined binding " ^ x); Source.substitute x a' b' end else Source.Let (x, a', b') @@ -107,6 +124,28 @@ let rec inline_term note unsafe_repr_eq term = Source.Case (inline_term note unsafe_repr_eq s, (x, inline_term note unsafe_repr_eq l), (y, inline_term note unsafe_repr_eq r)) | other -> other +let rec drop_effects note = function + | Source.Tick (label, t) -> + note Effect_observation "source effect" ("dropped observable tick " ^ label); + drop_effects note t + | Source.Pair (a, b) -> Source.Pair (drop_effects note a, drop_effects note b) + | Source.Inl (ty, t) -> Source.Inl (ty, drop_effects note t) + | Source.Inr (ty, t) -> Source.Inr (ty, drop_effects note t) + | Source.Lam (x, a, b, body) -> Source.Lam (x, a, b, drop_effects note body) + | Source.App (f, a) -> Source.App (drop_effects note f, drop_effects note a) + | Source.TyLam (x, body) -> Source.TyLam (x, drop_effects note body) + | Source.TyApp (t, ty) -> Source.TyApp (drop_effects note t, ty) + | Source.Roll (ty, t) -> Source.Roll (ty, drop_effects note t) + | Source.Unroll t -> Source.Unroll (drop_effects note t) + | Source.Fix (f, ty, body) -> Source.Fix (f, ty, drop_effects note body) + | Source.Eq (g, a, b) -> Source.Eq (g, drop_effects note a, drop_effects note b) + | Source.If (c, t, e) -> Source.If (drop_effects note c, drop_effects note t, drop_effects note e) + | Source.Let (x, a, b) -> Source.Let (x, drop_effects note a, drop_effects note b) + | Source.LetPair (x, y, a, b) -> Source.LetPair (x, y, drop_effects note a, drop_effects note b) + | Source.Case (s, (x, l), (y, r)) -> + Source.Case (drop_effects note s, (x, drop_effects note l), (y, drop_effects note r)) + | other -> other + let rec repr_of_typ = function | TInt -> Target.RInt | TBool -> Target.RBool @@ -142,6 +181,7 @@ let rec lower strict_unroll = function | Source.Eq (GBool, a, b) -> Target.EqBool (lower strict_unroll a, lower strict_unroll b) | Source.If (c, t, e) -> Target.If (lower strict_unroll c, lower strict_unroll t, lower strict_unroll e) + | Source.Tick (label, t) -> Target.Tick (label, lower strict_unroll t) | Source.Let (x, a, b) -> Target.Let (x, lower strict_unroll a, lower strict_unroll b) | Source.LetPair (x, y, a, b) -> Target.Let @@ -188,14 +228,18 @@ let compile flags source_type source_program = if flags.inline then inline_term (note "inline") flags.unsafe_repr_eq specialised else specialised in + let effect_rewritten = + if flags.unsafe_effect_drop then drop_effects (note "effect") inlined + else inlined + in let target_program = if flags.repr_lower then begin note "repr_lower" Worker_wrapper_proof "worker-wrapper" "wrapper must refine the boxed to unboxed relation on arguments and results"; if flags.unsafe_strict_unroll then note "repr_lower" Strictness_risk "roll/unroll" "strict unroll lowering may force recursive payloads earlier than the source"; match source_type with - | TArrow (TPair (TInt, TBool), TPair (TInt, TBool)) -> synthesize_worker_wrapper source_type inlined - | _ -> lower flags.unsafe_strict_unroll inlined - end else lower false inlined + | TArrow (TPair (TInt, TBool), TPair (TInt, TBool)) -> synthesize_worker_wrapper source_type effect_rewritten + | _ -> lower flags.unsafe_strict_unroll effect_rewritten + end else lower false effect_rewritten in - { source_type; source_program; specialised; inlined; target_program; obligations = List.rev !obligations } + { source_type; source_program; specialised; inlined; effect_rewritten; target_program; obligations = List.rev !obligations } diff --git a/src/pipeline.mli b/src/pipeline.mli index 92999e9..de14040 100644 --- a/src/pipeline.mli +++ b/src/pipeline.mli @@ -6,12 +6,14 @@ type optimisation_flags = { repr_lower : bool; unsafe_repr_eq : bool; unsafe_strict_unroll : bool; + unsafe_effect_drop : bool; } type obligation_kind = | Preserve_relation | Exposed_representation | Strictness_risk + | Effect_observation | Worker_wrapper_proof type obligation = { @@ -26,10 +28,10 @@ type compiled = { source_program : Source.term; specialised : Source.term; inlined : Source.term; + effect_rewritten : Source.term; target_program : Target.term; obligations : obligation list; } val default_flags : optimisation_flags val compile : optimisation_flags -> typ -> Source.term -> compiled - diff --git a/src/relation.ml b/src/relation.ml index 26375c7..77b4b6a 100644 --- a/src/relation.ml +++ b/src/relation.ml @@ -12,6 +12,8 @@ type verdict = type comparison = { source_outcome : Source.outcome; target_outcome : Target.outcome; + source_effects : int; + target_effects : int; verdict : verdict; } @@ -53,18 +55,29 @@ let rec cross_value_relation rel ty sv tv = | _ -> false let compare_programs ?(fuel = 256) rel ty src tgt = - let source_outcome = Source.observe ~fuel src in - let target_outcome = Target.observe ~fuel tgt in + let source_trace = Source.evaluate ~fuel src in + let target_trace = Target.evaluate ~fuel tgt in + let source_outcome = source_trace.Source.outcome in + let target_outcome = target_trace.Target.outcome in let verdict = match source_outcome, target_outcome with | Source.Value sv, Target.Value tv -> - if cross_value_relation rel ty sv tv then Related + if source_trace.Source.effects <> target_trace.Target.effects then + Unrelated "effect trace changed" + else if cross_value_relation rel ty sv tv then Related else Unrelated "value relation failed" - | Source.Diverged _, Target.Diverged _ -> Related + | Source.Diverged _, Target.Diverged _ -> + if source_trace.Source.effects = target_trace.Target.effects then Related + else Unrelated "effect trace changed before divergence" | Source.Diverged _, Target.Value _ -> Unrelated "target terminated where source diverged" | Source.Value _, Target.Diverged _ -> Unrelated "target diverged where source terminated" | Source.Stuck msg, _ -> Unrelated ("source stuck: " ^ msg) | _, Target.Stuck msg -> Unrelated ("target stuck: " ^ msg) in - { source_outcome; target_outcome; verdict } - + { + source_outcome; + target_outcome; + source_effects = source_trace.Source.effects; + target_effects = target_trace.Target.effects; + verdict; + } diff --git a/src/relation.mli b/src/relation.mli index e249d18..bf20830 100644 --- a/src/relation.mli +++ b/src/relation.mli @@ -12,10 +12,11 @@ type verdict = type comparison = { source_outcome : Source.outcome; target_outcome : Target.outcome; + source_effects : int; + target_effects : int; verdict : verdict; } val source_value_relation : relation -> typ -> Source.value -> Source.value -> bool val cross_value_relation : relation -> typ -> Source.value -> Target.value -> bool val compare_programs : ?fuel:int -> relation -> typ -> Source.term -> Target.term -> comparison - diff --git a/src/reporting.ml b/src/reporting.ml index f0d0f49..46fc80f 100644 --- a/src/reporting.ml +++ b/src/reporting.ml @@ -2,6 +2,7 @@ let obligation_kind_to_string = function | Pipeline.Preserve_relation -> "preserve_relation" | Pipeline.Exposed_representation -> "exposed_representation" | Pipeline.Strictness_risk -> "strictness_risk" + | Pipeline.Effect_observation -> "effect_observation" | Pipeline.Worker_wrapper_proof -> "worker_wrapper_proof" let string_of_source_outcome = function @@ -14,6 +15,12 @@ let string_of_target_outcome = function | Target.Stuck msg -> "stuck " ^ msg | Target.Diverged n -> "diverged after " ^ string_of_int n ^ " steps" +let string_of_source_trace trace = + string_of_source_outcome trace.Source.outcome ^ ", effects " ^ string_of_int trace.Source.effects + +let string_of_target_trace trace = + string_of_target_outcome trace.Target.outcome ^ ", effects " ^ string_of_int trace.Target.effects + let string_of_relation = function | Relation.Baseline -> "baseline" | Relation.Boxed_unboxed -> "boxed_unboxed" @@ -41,6 +48,17 @@ let emit_obligations (obligations : Pipeline.obligation list) = " / " ^ o.Pipeline.subject ^ ": " ^ o.Pipeline.detail) |> String.concat "\n" +let emit_pipeline_visualisation (compiled : Pipeline.compiled) = + String.concat "\n" + [ + "pipeline"; + "source: " ^ Source.string_of_term compiled.Pipeline.source_program; + "specialise: " ^ Source.string_of_term compiled.Pipeline.specialised; + "inline: " ^ Source.string_of_term compiled.Pipeline.inlined; + "effect: " ^ Source.string_of_term compiled.Pipeline.effect_rewritten; + "repr_lower: " ^ Target.string_of_term compiled.Pipeline.target_program; + ] + let emit_case_header (case : Corpus.case) (comparison : Relation.comparison) (compiled : Pipeline.compiled) = String.concat "\n" [ @@ -75,7 +93,7 @@ let emit_counterexample title (src_trace : Source.trace) (tgt_trace : Target.tra else "\n... " ^ string_of_int tgt_hidden ^ " more target steps omitted" in "source trace:\n" ^ emit_steps Source.string_of_term src_steps ^ - src_suffix ^ "\n\nsource outcome: " ^ string_of_source_outcome src_trace.Source.outcome ^ + src_suffix ^ "\n\nsource outcome: " ^ string_of_source_trace src_trace ^ "\n\ntarget trace:\n" ^ emit_steps Target.string_of_term tgt_steps ^ - tgt_suffix ^ "\n\ntarget outcome: " ^ string_of_target_outcome tgt_trace.Target.outcome ^ + tgt_suffix ^ "\n\ntarget outcome: " ^ string_of_target_trace tgt_trace ^ "\n\nobligations:\n" ^ emit_obligations obligations ^ "\n" diff --git a/src/reporting.mli b/src/reporting.mli index 7c5971e..3616472 100644 --- a/src/reporting.mli +++ b/src/reporting.mli @@ -1,9 +1,12 @@ val obligation_kind_to_string : Pipeline.obligation_kind -> string val string_of_source_outcome : Source.outcome -> string val string_of_target_outcome : Target.outcome -> string +val string_of_source_trace : Source.trace -> string +val string_of_target_trace : Target.trace -> string val string_of_relation : Relation.relation -> string val verdict_to_string : Relation.verdict -> string val take_steps : int -> 'a list -> 'a list * int val emit_obligations : Pipeline.obligation list -> string +val emit_pipeline_visualisation : Pipeline.compiled -> string val emit_case_header : Corpus.case -> Relation.comparison -> Pipeline.compiled -> string val emit_counterexample : string -> Source.trace -> Target.trace -> Pipeline.obligation list -> string diff --git a/src/source.ml b/src/source.ml index 4132a66..e29d7ff 100644 --- a/src/source.ml +++ b/src/source.ml @@ -18,6 +18,7 @@ type term = | Fix of var * typ * term | Eq of ground * term * term | If of term * term * term + | Tick of string * term | Let of var * term * term | LetPair of var * var * term * term | Case of term * (var * term) * (var * term) @@ -59,6 +60,7 @@ type outcome = type trace = { steps : term list; outcome : outcome; + effects : int; } let typ_of (Expr (ty, _)) = ty @@ -83,6 +85,7 @@ let rec string_of_term = function "(eq_" ^ string_of_ground g ^ " " ^ string_of_term a ^ " " ^ string_of_term b ^ ")" | If (c, t, e) -> "(if " ^ string_of_term c ^ " then " ^ string_of_term t ^ " else " ^ string_of_term e ^ ")" + | Tick (label, t) -> "(tick[" ^ label ^ "] " ^ string_of_term t ^ ")" | Let (x, a, b) -> "(let " ^ x ^ " = " ^ string_of_term a ^ " in " ^ string_of_term b ^ ")" | LetPair (x, y, a, b) -> @@ -127,6 +130,7 @@ let rec substitute x repl term = if String.equal x f then term else Fix (f, ty, go body) | Eq (g, a, b) -> Eq (g, go a, go b) | If (c, t, e) -> If (go c, go t, go e) + | Tick (label, t) -> Tick (label, go t) | Let (y, a, b) -> Let (y, go a, if String.equal x y then b else go b) | LetPair (y, z, a, b) -> @@ -151,6 +155,7 @@ let rec substitute_type x repl term = | Fix (f, ty, body) -> Fix (f, sub_ty ty, go body) | Eq (g, a, b) -> Eq (g, go a, go b) | If (c, t, e) -> If (go c, go t, go e) + | Tick (label, t) -> Tick (label, go t) | Let (y, a, b) -> Let (y, go a, go b) | LetPair (y, z, a, b) -> LetPair (y, z, go a, go b) | Case (scrut, (y, l), (z, r)) -> Case (go scrut, (y, go l), (z, go r)) @@ -211,6 +216,8 @@ let rec step term = | If (Bool false, _, e) -> Ok e | If (c, t, e) when not (is_value c) -> Result.map (fun c' -> If (c', t, e)) (stepv c) | If _ -> stuck "if scrutinee is not a bool" + | Tick (_, t) when is_value t -> Ok t + | Tick (label, t) -> Result.map (fun t' -> Tick (label, t')) (stepv t) | Let (x, a, b) when is_value a -> Ok (substitute x a b) | Let (x, a, b) -> Result.map (fun a' -> Let (x, a', b)) (stepv a) | LetPair (x, y, Pair (a, b), body) when is_value a && is_value b -> @@ -234,24 +241,43 @@ let rec step term = | Int _ | Bool _ | Lam _ | TyLam _ | Roll _ -> stuck "value" | Inl _ | Inr _ -> stuck "sum injection expects value subterm" +let rec active_tick = function + | Tick (_, payload) when is_value payload -> 1 + | Tick (_, payload) -> active_tick payload + | App (f, a) when not (is_value f) -> active_tick f + | App (f, a) when not (is_value a) -> active_tick a + | Pair (a, _) when not (is_value a) -> active_tick a + | Pair (_, b) when not (is_value b) -> active_tick b + | Inl (_, t) | Inr (_, t) when not (is_value t) -> active_tick t + | Eq (_, a, _) when not (is_value a) -> active_tick a + | Eq (_, _, b) when not (is_value b) -> active_tick b + | If (c, _, _) when not (is_value c) -> active_tick c + | Let (_, a, _) when not (is_value a) -> active_tick a + | LetPair (_, _, scrut, _) when not (is_value scrut) -> active_tick scrut + | Case (scrut, _, _) when not (is_value scrut) -> active_tick scrut + | TyApp (t, _) when not (is_value t) -> active_tick t + | Unroll t when not (is_value t) -> active_tick t + | _ -> 0 + let evaluate ?(fuel = 256) term = - let rec go n acc t = - if n = 0 then { steps = List.rev (t :: acc); outcome = Diverged fuel } + let rec go effects n acc t = + if n = 0 then { steps = List.rev (t :: acc); outcome = Diverged fuel; effects } else if is_value t then match value_of_term t with - | Some v -> { steps = List.rev (t :: acc); outcome = Value v } - | None -> { steps = List.rev (t :: acc); outcome = Stuck "internal value decoding failure" } + | Some v -> { steps = List.rev (t :: acc); outcome = Value v; effects } + | None -> { steps = List.rev (t :: acc); outcome = Stuck "internal value decoding failure"; effects } else + let ticked = active_tick t in match step t with - | Ok t' -> go (n - 1) (t :: acc) t' + | Ok t' -> go (effects + ticked) (n - 1) (t :: acc) t' | Error "value" -> begin match value_of_term t with - | Some v -> { steps = List.rev (t :: acc); outcome = Value v } - | None -> { steps = List.rev (t :: acc); outcome = Stuck "internal value decoding failure" } + | Some v -> { steps = List.rev (t :: acc); outcome = Value v; effects } + | None -> { steps = List.rev (t :: acc); outcome = Stuck "internal value decoding failure"; effects } end - | Error msg -> { steps = List.rev (t :: acc); outcome = Stuck msg } + | Error msg -> { steps = List.rev (t :: acc); outcome = Stuck msg; effects } in - go fuel [] term + go 0 fuel [] term let observe ?fuel term = (evaluate ?fuel term).outcome diff --git a/src/source.mli b/src/source.mli index c01012c..7c4ecca 100644 --- a/src/source.mli +++ b/src/source.mli @@ -18,6 +18,7 @@ type term = | Fix of var * typ * term | Eq of ground * term * term | If of term * term * term + | Tick of string * term | Let of var * term * term | LetPair of var * var * term * term | Case of term * (var * term) * (var * term) @@ -59,6 +60,7 @@ type outcome = type trace = { steps : term list; outcome : outcome; + effects : int; } val typ_of : 'a expr -> typ diff --git a/src/target.ml b/src/target.ml index 5b5e579..0931d2c 100644 --- a/src/target.ml +++ b/src/target.ml @@ -30,6 +30,7 @@ type term = | EqInt of term * term | EqBool of term * term | If of term * term * term + | Tick of string * term | Box of typ * term | Unbox of term | Roll of typ * term @@ -66,6 +67,7 @@ type outcome = type trace = { steps : term list; outcome : outcome; + effects : int; } let rec string_of_repr = function @@ -99,6 +101,7 @@ let rec string_of_term = function | EqBool (a, b) -> "(eq_bool# " ^ string_of_term a ^ " " ^ string_of_term b ^ ")" | If (c, t, e) -> "(if# " ^ string_of_term c ^ " then " ^ string_of_term t ^ " else " ^ string_of_term e ^ ")" + | Tick (label, t) -> "(tick#[" ^ label ^ "] " ^ string_of_term t ^ ")" | Box (_, t) -> "(box " ^ string_of_term t ^ ")" | Unbox t -> "(unbox " ^ string_of_term t ^ ")" | Roll (_, t) -> "(roll# " ^ string_of_term t ^ ")" @@ -270,6 +273,7 @@ let validate term = let tr, errors = infer ctx env t errors in let er, errors = infer ctx env e errors in (tr, expect_repr ctx tr er (expect_repr ctx RBool cr errors)) + | Tick (_, t) -> infer ctx env t errors | Box (ty, t) -> let _r, errors = infer ctx env t errors in (RBox ty, errors) @@ -356,6 +360,7 @@ let rec substitute x repl term = | EqInt (a, b) -> EqInt (go a, go b) | EqBool (a, b) -> EqBool (go a, go b) | If (c, t, e) -> If (go c, go t, go e) + | Tick (label, t) -> Tick (label, go t) | Box (ty, t) -> Box (ty, go t) | Unbox t -> Unbox (go t) | Roll (ty, t) -> Roll (ty, go t) @@ -421,6 +426,8 @@ let rec step term = | If (Bool false, _, e) -> Ok e | If (c, t, e) when not (is_value c) -> Result.map (fun c' -> If (c', t, e)) (step c) | If _ -> Error "if# on non-bool value" + | Tick (_, t) when is_value t -> Ok t + | Tick (label, t) -> Result.map (fun t' -> Tick (label, t')) (step t) | Box (ty, t) when not (is_value t) -> Result.map (fun t' -> Box (ty, t')) (step t) | Unbox (Box (_, v)) when is_value v -> Ok v | Unbox t when not (is_value t) -> Result.map (fun t' -> Unbox t') (step t) @@ -443,24 +450,54 @@ let rec step term = | Int _ | Bool _ | Lam _ | Box _ | Roll _ -> Error "value" | Inl _ | Inr _ -> Error "sum injection expects value subterm" +let rec first_active_tick = function + | Tick (_, payload) when is_value payload -> 1 + | Tick (_, payload) -> first_active_tick payload + | App (f, _) when not (is_value f) -> first_active_tick f + | App (_, args) -> + args + |> List.find_opt (fun arg -> not (is_value arg)) + |> Option.map first_active_tick + |> Option.value ~default:0 + | Tuple xs -> + xs + |> List.find_opt (fun arg -> not (is_value arg)) + |> Option.map first_active_tick + |> Option.value ~default:0 + | Proj (_, t) when not (is_value t) -> first_active_tick t + | Inl (_, _, t) | Inr (_, _, t) when not (is_value t) -> first_active_tick t + | Case (s, _, _) when not (is_value s) -> first_active_tick s + | Let (_, a, _) when not (is_value a) -> first_active_tick a + | EqInt (a, _) when not (is_value a) -> first_active_tick a + | EqInt (_, b) when not (is_value b) -> first_active_tick b + | EqBool (a, _) when not (is_value a) -> first_active_tick a + | EqBool (_, b) when not (is_value b) -> first_active_tick b + | If (c, _, _) when not (is_value c) -> first_active_tick c + | Box (_, t) when not (is_value t) -> first_active_tick t + | Unbox t when not (is_value t) -> first_active_tick t + | Unroll t when not (is_value t) -> first_active_tick t + | Halt t when not (is_value t) -> first_active_tick t + | _ -> 0 + let evaluate ?(fuel = 256) term = - let rec go n acc t = - if n = 0 then { steps = List.rev (t :: acc); outcome = Diverged fuel } + let rec go effects n acc t = + if n = 0 then { steps = List.rev (t :: acc); outcome = Diverged fuel; effects } else if is_value t then match value_of_term t with - | Some v -> { steps = List.rev (t :: acc); outcome = Value v } - | None -> { steps = List.rev (t :: acc); outcome = Stuck "internal target value decoding failure" } + | Some v -> { steps = List.rev (t :: acc); outcome = Value v; effects } + | None -> { steps = List.rev (t :: acc); outcome = Stuck "internal target value decoding failure"; effects } else + let ticked = first_active_tick t in match step t with - | Ok t' -> go (n - 1) (t :: acc) t' + | Ok t' -> go (effects + ticked) (n - 1) (t :: acc) t' | Error "value" -> begin match value_of_term t with - | Some v -> { steps = List.rev (t :: acc); outcome = Value v } - | None -> { steps = List.rev (t :: acc); outcome = Stuck "internal target value decoding failure" } + | Some v -> { steps = List.rev (t :: acc); outcome = Value v; effects } + | None -> { steps = List.rev (t :: acc); outcome = Stuck "internal target value decoding failure"; effects } end - | Error msg -> { steps = List.rev (t :: acc); outcome = Stuck msg } + | Error msg -> { steps = List.rev (t :: acc); outcome = Stuck msg; effects } in - go fuel [] term + go 0 fuel [] term let observe ?fuel term = (evaluate ?fuel term).outcome diff --git a/src/target.mli b/src/target.mli index ab99b6b..4a88f0f 100644 --- a/src/target.mli +++ b/src/target.mli @@ -30,6 +30,7 @@ type term = | EqInt of term * term | EqBool of term * term | If of term * term * term + | Tick of string * term | Box of typ * term | Unbox of term | Roll of typ * term @@ -66,6 +67,7 @@ type outcome = type trace = { steps : term list; outcome : outcome; + effects : int; } val string_of_repr : repr -> string diff --git a/src/typecheck.ml b/src/typecheck.ml index 351e81b..07b766c 100644 --- a/src/typecheck.ml +++ b/src/typecheck.ml @@ -95,6 +95,7 @@ let rec type_of_env env term = let* te = type_of_env env e in let* () = expect tt te in Ok tt + | Source.Tick (_, t) -> type_of_env env t | Source.Let (x, a, b) -> let* ta = type_of_env env a in type_of_env ((x, ta) :: env) b @@ -125,4 +126,3 @@ let is_well_typed expected term = match check expected term with | Ok () -> true | Error _ -> false - diff --git a/test/invariants.ml b/test/invariants.ml index 5c643b8..0211ada 100644 --- a/test/invariants.ml +++ b/test/invariants.ml @@ -57,6 +57,18 @@ let () = assert_true "expected strictness shift witness" (strict.failure_mode = Audit.Strictness_shift); + let effect_audit = Audit.audit_case (find_case "effect-elision-breaks-observation") in + assert_true + "expected effect shift witness" + (effect_audit.failure_mode = Audit.Effect_shift); + assert_true + "expected unsafe effect rewrite to emit effect observation obligation" + (has_obligation Pipeline.Effect_observation effect_audit.compiled.obligations); + assert_true + "expected effect trace invariant failure" + (List.exists + (fun result -> result.Audit.kind = Audit.Effect_trace && not result.Audit.passed) + effect_audit.Audit.invariants); let generated = Gen.sample_terms ~count:80 ~max_depth:4 () in List.iter (fun specimen -> @@ -84,7 +96,7 @@ let () = "expected unsupported worker-wrapper source shape to be rejected" (fun () -> Pipeline.compile - { Pipeline.default_flags with unsafe_repr_eq = false; unsafe_strict_unroll = false } + { Pipeline.default_flags with unsafe_repr_eq = false; unsafe_strict_unroll = false; unsafe_effect_drop = false } (Types.TArrow (Types.TPair (Types.TInt, Types.TBool), Types.TPair (Types.TInt, Types.TBool))) (Source.Lam ( "p",