src/compiler/explanations.panack
Green: covered; red: known zero; amber: unavailable. Blank lines are outside the executable-start-line denominator.
1 import "source_maps.panack" 2 3 // Presentation consumes retained checker decisions and the exact loaded text. 4 // It does not rerun proofs, parse diagnostics, or execute user code. 5 pure explanation_location(origin: Option[SourceSpan], sources: Map[Str,Str], root: Str, stdlib_root: Str): Str { 6 match origin { 7 None() => "source: unavailable", 8 Some(span) => { 9 if !sources.has(span.start.file) { "source: unavailable" } 10 else { 11 source: Str = sources.get(span.start.file) 12 if span.end.offset < span.start.offset || span.end.offset > len(source) { "source: unavailable" } 13 else { 14 file: Str = source_map_escape(source_identifier(span.start.file, root, stdlib_root)) 15 line: Nat = span.start.line 16 column: Nat = span.start.column 17 end_line: Nat = span.end.line 18 end_column: Nat = span.end.column 19 expression: Str = source_map_escape(slice(source, span.start.offset, span.end.offset)) 20 "source: ${file}:${line}:${column}-${end_line}:${end_column}\nexpression: ${expression}" 21 } 22 } 23 } 24 } 25 } 26 27 pure render_subtraction_evidence(entry: SubtractionEvidence, sources: Map[Str,Str], root: Str, stdlib_root: Str): Str { 28 decision: SubtractionDecision = entry.decision 29 unavailable: Bool = decision.rule == "unsupported" || decision.rule == "invalid-operands" 30 status: Str = if unavailable { "unavailable" } else { if decision.proven { "proved" } else { "unproved" } } 31 left_type: Str = source_map_escape(entry.left.name) 32 right_type: Str = source_map_escape(entry.right.name) 33 mut output: Str = "subtraction: ${status}\n" + explanation_location(entry.span, sources, root, stdlib_root) + 34 "\noperand types: ${left_type}, ${right_type}" 35 if unavailable { 36 output = output + if decision.rule == "unsupported" { 37 "\nreason: this query only explains Nat subtraction obligations" 38 } else { "\nreason: operand checking failed; no trustworthy subtraction explanation" } 39 } else { 40 output = output + "\nobligation: left >= right" 41 if entry.left.has_nat { 42 value: Nat = entry.left.nat_value 43 output = output + "\nleft constant: ${value}" 44 } 45 if entry.right.has_nat { 46 value: Nat = entry.right.nat_value 47 output = output + "\nright constant: ${value}" 48 } else { output = output + "\nright constant: unknown" } 49 if decision.has_lower { 50 bound: Nat = decision.lower 51 output = output + "\nleft lower bound: ${bound}" 52 match decision.guard { 53 None() => { output = output + "\nguard origin: unavailable"; }, 54 Some(guard) => { 55 truth: Str = if guard.truth { "true" } else { "false" } 56 output = output + "\nguard branch: ${truth}\n" + explanation_location(guard.span, sources, root, stdlib_root) 57 } 58 } 59 } 60 output = output + if decision.rule == "constants" { 61 "\nreason: retained constant values satisfy the obligation" 62 } else { if decision.rule == "lower-bound" { 63 "\nreason: retained lower bound is at least the right constant" 64 } else { 65 "\nreason: retained facts do not prove the obligation; this does not establish a runtime failure" 66 } } 67 } 68 output 69 } 70 71 pure render_subtraction_explanations(project: LoadedProject, name: Str, root: Str, stdlib_root: Str): Str { 72 state: Str = if len(project.diagnostics) == 0 { "accepted" } else { "rejected" } 73 function_name: Str = source_map_escape(name) 74 mut output: Str = "program: ${state}\nfunction: ${function_name}\nscope: Nat subtraction; generic definitions, not call-site specialisations" 75 mut count: Nat = 0 76 for entry in project.evidence { 77 if entry.function_name == name { 78 output = output + "\n\n" + render_subtraction_evidence(entry, project.sources, root, stdlib_root) 79 count = count + 1 80 } 81 } 82 if count == 0 { output = output + "\n\nsubtraction: unavailable\nreason: no subtraction evidence was retained for this function"; } 83 output 84 } 85 86 // Each status concerns one local rule boundary, never the execution of a path 87 // or the validity of the complete expression/program. 88 pure effect_display_target(name: Str): Str { 89 if name == "$unit" { "()" } else { 90 if starts_with(name, "$method_") { slice(name, 8, len(name)) } else { 91 if starts_with(name, "$core_") { slice(name, 6, len(name)) } else { name } 92 } 93 } 94 } 95 96 pure render_effect_evidence(entry: EffectEvidence, sources: Map[Str,Str], root: Str, stdlib_root: Str): Str { 97 status: Str = if len(entry.violations) == 0 { "allowed" } else { "rejected" } 98 mut output: Str = "effect boundary: ${status}\n" + explanation_location(entry.span, sources, root, stdlib_root) + 99 "\nboundary: " + entry.kind + "\ncontext: " + entry.mode 100 if entry.kind == "call" { 101 output = output + "\ncallee: " + source_map_escape(effect_display_target(entry.target)) + "\nclassification basis: " + entry.basis + 102 "\ncallee effect: " + entry.target_effect + if entry.awaited { "\nawaited: yes" } else { "\nawaited: no" } 103 } 104 if len(entry.violations) > 0 { 105 for reason in entry.violations { output = output + "\nreason: " + source_map_escape(reason); } 106 } else { 107 output = output + if entry.kind == "await" { 108 "\nreason: enclosing function is async; operand boundaries are checked separately" 109 } else { if entry.target_effect == "async" { 110 "\nreason: async call is awaited inside an async function" 111 } else { if entry.target_effect == "pure" { 112 "\nreason: pure call is permitted in this context" 113 } else { 114 "\nreason: ordinary function permits this effectful call" 115 } } } 116 } 117 output 118 } 119 120 pure render_function_explanations(project: LoadedProject, name: Str, root: Str, stdlib_root: Str): Str { 121 mut output: Str = render_subtraction_explanations(project, name, root, stdlib_root) 122 output = output + "\n\neffect scope: local call and await boundaries; declarations and callable types, not transitive/runtime effects" 123 if !project.effects_checked { 124 output = output + "\neffects: unavailable\nreason: loading, resolution or global declaration checking prevented the effect pass" 125 } else { if project.function_types.has(name) && !project.function_types.get(name) { 126 output = output + "\neffects: unavailable\nreason: function body type checking prevented the effect pass for this function" 127 } else { 128 mut count: Nat = 0 129 for entry in project.effects { 130 if entry.function_name == name { 131 output = output + "\n\n" + render_effect_evidence(entry, project.sources, root, stdlib_root) 132 count = count + 1 133 } 134 } 135 if count == 0 { output = output + "\neffects: unavailable\nreason: no call or await boundary was retained for this function"; } 136 } } 137 output 138 } 139
Functions
[
{
"id": "declaration/1",
"name": "explanation_location",
"line": 5,
"state": "zero",
"entries": "0"
},
{
"id": "declaration/2",
"name": "render_subtraction_evidence",
"line": 27,
"state": "zero",
"entries": "0"
},
{
"id": "declaration/3",
"name": "render_subtraction_explanations",
"line": 71,
"state": "zero",
"entries": "0"
},
{
"id": "declaration/4",
"name": "effect_display_target",
"line": 88,
"state": "zero",
"entries": "0"
},
{
"id": "declaration/5",
"name": "render_effect_evidence",
"line": 96,
"state": "zero",
"entries": "0"
},
{
"id": "declaration/6",
"name": "render_function_explanations",
"line": 120,
"state": "zero",
"entries": "0"
}
]Source branch outcomes
[
{
"id": "declaration/1/tail/arm/0",
"outcome": "None",
"line": 7,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/1/tail/arm/1",
"outcome": "Some",
"line": 8,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/1/tail/arm/1/body/block/tail/decision/true",
"outcome": "true",
"line": 9,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/1/tail/arm/1/body/block/tail/decision/false",
"outcome": "false",
"line": 9,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/1/tail/arm/1/body/block/tail/false/tail/decision/true",
"outcome": "true",
"line": 12,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/1/tail/arm/1/body/block/tail/false/tail/decision/false",
"outcome": "false",
"line": 12,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/1/tail/arm/1/body/block/tail/false/tail/condition/decision/evaluate-right",
"outcome": "evaluate-right",
"line": 12,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/1/tail/arm/1/body/block/tail/false/tail/condition/decision/skip-right",
"outcome": "skip-right",
"line": 12,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/1/value/decision/evaluate-right",
"outcome": "evaluate-right",
"line": 29,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/1/value/decision/skip-right",
"outcome": "skip-right",
"line": 29,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/2/value/decision/true",
"outcome": "true",
"line": 30,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/2/value/decision/false",
"outcome": "false",
"line": 30,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/2/value/false/tail/decision/true",
"outcome": "true",
"line": 30,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/2/value/false/tail/decision/false",
"outcome": "false",
"line": 30,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/6/value/decision/true",
"outcome": "true",
"line": 35,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/6/value/decision/false",
"outcome": "false",
"line": 35,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/6/value/true/statement/0/value/right/decision/true",
"outcome": "true",
"line": 36,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/6/value/true/statement/0/value/right/decision/false",
"outcome": "false",
"line": 36,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/6/value/false/statement/1/value/decision/true",
"outcome": "true",
"line": 41,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/6/value/false/statement/1/value/decision/false",
"outcome": "false",
"line": 41,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/6/value/false/statement/2/value/decision/true",
"outcome": "true",
"line": 45,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/6/value/false/statement/2/value/decision/false",
"outcome": "false",
"line": 45,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/6/value/false/statement/3/value/decision/true",
"outcome": "true",
"line": 49,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/6/value/false/statement/3/value/decision/false",
"outcome": "false",
"line": 49,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/6/value/false/statement/3/value/true/tail/arm/0",
"outcome": "None",
"line": 53,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/6/value/false/statement/3/value/true/tail/arm/1",
"outcome": "Some",
"line": 54,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/6/value/false/statement/3/value/true/tail/arm/1/body/block/statement/0/value/decision/true",
"outcome": "true",
"line": 55,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/6/value/false/statement/3/value/true/tail/arm/1/body/block/statement/0/value/decision/false",
"outcome": "false",
"line": 55,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/6/value/false/statement/4/value/right/decision/true",
"outcome": "true",
"line": 60,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/6/value/false/statement/4/value/right/decision/false",
"outcome": "false",
"line": 60,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/6/value/false/statement/4/value/right/false/tail/decision/true",
"outcome": "true",
"line": 62,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/2/statement/6/value/false/statement/4/value/right/false/tail/decision/false",
"outcome": "false",
"line": 62,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/3/statement/0/value/decision/true",
"outcome": "true",
"line": 72,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/3/statement/0/value/decision/false",
"outcome": "false",
"line": 72,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/3/statement/4/decision/body",
"outcome": "body",
"line": 76,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/3/statement/4/decision/exit",
"outcome": "exit",
"line": 76,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/3/statement/4/body/tail/decision/true",
"outcome": "true",
"line": 77,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/3/statement/4/body/tail/decision/false",
"outcome": "false",
"line": 77,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/3/statement/5/value/decision/true",
"outcome": "true",
"line": 82,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/3/statement/5/value/decision/false",
"outcome": "false",
"line": 82,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/4/tail/decision/true",
"outcome": "true",
"line": 89,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/4/tail/decision/false",
"outcome": "false",
"line": 89,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/4/tail/false/tail/decision/true",
"outcome": "true",
"line": 90,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/4/tail/false/tail/decision/false",
"outcome": "false",
"line": 90,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/4/tail/false/tail/false/tail/decision/true",
"outcome": "true",
"line": 91,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/4/tail/false/tail/false/tail/decision/false",
"outcome": "false",
"line": 91,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/5/statement/0/value/decision/true",
"outcome": "true",
"line": 97,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/5/statement/0/value/decision/false",
"outcome": "false",
"line": 97,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/5/statement/2/value/decision/true",
"outcome": "true",
"line": 100,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/5/statement/2/value/decision/false",
"outcome": "false",
"line": 100,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/5/statement/2/value/true/statement/0/value/right/decision/true",
"outcome": "true",
"line": 102,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/5/statement/2/value/true/statement/0/value/right/decision/false",
"outcome": "false",
"line": 102,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/5/statement/3/value/decision/true",
"outcome": "true",
"line": 104,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/5/statement/3/value/decision/false",
"outcome": "false",
"line": 104,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/5/statement/3/value/true/statement/0/decision/body",
"outcome": "body",
"line": 105,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/5/statement/3/value/true/statement/0/decision/exit",
"outcome": "exit",
"line": 105,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/5/statement/3/value/false/statement/0/value/right/decision/true",
"outcome": "true",
"line": 107,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/5/statement/3/value/false/statement/0/value/right/decision/false",
"outcome": "false",
"line": 107,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/5/statement/3/value/false/statement/0/value/right/false/tail/decision/true",
"outcome": "true",
"line": 109,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/5/statement/3/value/false/statement/0/value/right/false/tail/decision/false",
"outcome": "false",
"line": 109,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/5/statement/3/value/false/statement/0/value/right/false/tail/false/tail/decision/true",
"outcome": "true",
"line": 111,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/5/statement/3/value/false/statement/0/value/right/false/tail/false/tail/decision/false",
"outcome": "false",
"line": 111,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/6/statement/2/value/decision/true",
"outcome": "true",
"line": 123,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/6/statement/2/value/decision/false",
"outcome": "false",
"line": 123,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/6/statement/2/value/false/tail/decision/true",
"outcome": "true",
"line": 125,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/6/statement/2/value/false/tail/decision/false",
"outcome": "false",
"line": 125,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/6/statement/2/value/false/tail/condition/decision/evaluate-right",
"outcome": "evaluate-right",
"line": 125,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/6/statement/2/value/false/tail/condition/decision/skip-right",
"outcome": "skip-right",
"line": 125,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/6/statement/2/value/false/tail/false/statement/1/decision/body",
"outcome": "body",
"line": 129,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/6/statement/2/value/false/tail/false/statement/1/decision/exit",
"outcome": "exit",
"line": 129,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/6/statement/2/value/false/tail/false/statement/1/body/tail/decision/true",
"outcome": "true",
"line": 130,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/6/statement/2/value/false/tail/false/statement/1/body/tail/decision/false",
"outcome": "false",
"line": 130,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/6/statement/2/value/false/tail/false/tail/decision/true",
"outcome": "true",
"line": 135,
"state": "zero",
"hits": "0"
},
{
"id": "declaration/6/statement/2/value/false/tail/false/tail/decision/false",
"outcome": "false",
"line": 135,
"state": "zero",
"hits": "0"
}
]Reviewed declaration exclusions
[
{
"id": "declaration/0",
"reason": "import",
"line": 1
}
]