File size: 6,783 Bytes
119e586 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 | <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE execution_node [
<!-- Execution node DTD — ISO 8879:1986 -->
<!ELEMENT execution_node - - (configuration, input_spec, synthesis_tree, proof_receipt)>
<!ATTLIST execution_node
id ID #REQUIRED
status (SUCCESS|FAILURE|IN_PROGRESS) #REQUIRED>
<!ELEMENT configuration - - (flag*, target_algorithm?)>
<!ELEMENT flag - O EMPTY>
<!ATTLIST flag
key CDATA #REQUIRED
value CDATA #REQUIRED>
<!ELEMENT target_algorithm - O EMPTY>
<!ATTLIST target_algorithm
name CDATA #REQUIRED>
<!ELEMENT input_spec - - (partial_ast, relational_constraint)>
<!ELEMENT partial_ast - - (#PCDATA)>
<!ELEMENT relational_constraint - - (#PCDATA)>
<!ELEMENT synthesis_tree - - (iteration+)>
<!ELEMENT iteration - - (minikanren_trace, z3_refinement_check, mutation_event?, proof_generation?)>
<!ATTLIST iteration
pass NUMBER #REQUIRED
status (VERIFIED|REJECTED_BY_SMT|PENDING) #REQUIRED>
<!ELEMENT minikanren_trace - - (unification_step+, derived_ast)>
<!ATTLIST minikanren_trace
engine CDATA #REQUIRED>
<!ELEMENT unification_step - - (goal, binding+)>
<!ATTLIST unification_step
id ID #REQUIRED>
<!ELEMENT goal - - (#PCDATA)>
<!ELEMENT binding - O EMPTY>
<!ATTLIST binding
var CDATA #REQUIRED
val CDATA #REQUIRED>
<!ELEMENT derived_ast - - (#PCDATA)>
<!ELEMENT z3_refinement_check - - (smt_lib2_script, solver_output, violation_reason?)>
<!ATTLIST z3_refinement_check
solver CDATA #REQUIRED
result (sat|unsat) #REQUIRED>
<!ELEMENT smt_lib2_script - - (#PCDATA)>
<!ELEMENT solver_output - - (#PCDATA)>
<!ELEMENT violation_reason - O (#PCDATA)>
<!ELEMENT mutation_event - O EMPTY>
<!ATTLIST mutation_event
action CDATA #REQUIRED>
<!ELEMENT reason - - (#PCDATA)>
<!ELEMENT proof_generation - O (lean4_certificate)>
<!ELEMENT lean4_certificate - - (#PCDATA)>
<!ELEMENT proof_receipt - - (summary, final_synthesized_ast)>
<!ATTLIST proof_receipt
mode (VERBOSE|COMPACT) #REQUIRED>
<!ELEMENT summary - - (total_iterations, smt_status, lean_status)>
<!ELEMENT total_iterations - - (#PCDATA)>
<!ELEMENT smt_status - - (#PCDATA)>
<!ELEMENT lean_status - - (#PCDATA)>
<!ELEMENT final_synthesized_ast - - (#PCDATA)>
]>
<execution_node id="exec-tree-invert-001" status="SUCCESS">
<configuration>
<flag key="verbose" value="true"/>
<flag key="max_refinement_depth" value="5"/>
<target_algorithm name="tree-invert"/>
</configuration>
<input_spec>
<partial_ast>
(define tree-invert
(lambda (t)
(if (null? t)
'()
(list (car t) _ (tree-invert (cadr t))))))
</partial_ast>
<relational_constraint>
(evalo '(tree-invert '(1 (2 () ()) (3 () ()))) '() '(1 (3 () ()) (2 () ())))
</relational_constraint>
</input_spec>
<synthesis_tree>
<!-- PASS 1: FAILS REFINEMENT CHECK -->
<iteration pass="1" status="REJECTED_BY_SMT">
<minikanren_trace engine="JS_MINIKANREN">
<unification_step id="u1">
<goal>evalo (cadr t) env val_left</goal>
<binding var="_" val="(tree-invert (cadr t))"/>
</unification_step>
<derived_ast>
(list (car t) (tree-invert (cadr t)) (tree-invert (cadr t)))
</derived_ast>
</minikanren_trace>
<z3_refinement_check solver="Z3_WASM" result="unsat">
<smt_lib2_script>
(set-logic QF_LIA)
(declare-fun left_subtree_val () Int)
(declare-fun right_subtree_val () Int)
; Refinement invariant: inversion must SWAP subtrees, not duplicate
; left_val must equal right_input (3), not left_input (2)
(assert (= left_subtree_val 2))
(assert (= right_subtree_val 3))
(assert (= left_subtree_val right_subtree_val))
; ^ VIOLATION: duplicated left branch, swap invariant breached
(check-sat)
</smt_lib2_script>
<solver_output>unsat</solver_output>
<violation_reason>
Subtree symmetry invariant breached: duplicated left branch instead of
swapping right branch. Hole _ was bound to (tree-invert (cadr t)) but
must be bound to (tree-invert (caddr t)) to satisfy the swap constraint.
</violation_reason>
</z3_refinement_check>
<mutation_event action="AST_MUTATE"/>
</iteration>
<!-- PASS 2: SUCCESS AND VERIFIED -->
<iteration pass="2" status="VERIFIED">
<minikanren_trace engine="JS_MINIKANREN">
<unification_step id="u2">
<goal>evalo (caddr t) env val_right</goal>
<binding var="_" val="(tree-invert (caddr t))"/>
</unification_step>
<derived_ast>
(define tree-invert
(lambda (t)
(if (null? t)
'()
(list (car t) (tree-invert (caddr t)) (tree-invert (cadr t))))))
</derived_ast>
</minikanren_trace>
<z3_refinement_check solver="Z3_WASM" result="sat">
<smt_lib2_script>
(set-logic QF_LIA)
(declare-fun left_in () Int)
(declare-fun right_in () Int)
(declare-fun left_out () Int)
(declare-fun right_out () Int)
; Input tree: (1 (2 () ()) (3 () ()))
(assert (= left_in 2))
(assert (= right_in 3))
; Inversion swap invariant: left_out == right_in, right_out == left_in
(assert (= left_out right_in))
(assert (= right_out left_in))
(check-sat)
(get-model)
</smt_lib2_script>
<solver_output>
sat
(model
(define-fun left_in () Int 2)
(define-fun right_in () Int 3)
(define-fun left_out () Int 3)
(define-fun right_out () Int 2)
)
</solver_output>
</z3_refinement_check>
<proof_generation>
<lean4_certificate>
-- Lean 4 proof: tree_invert_correct
-- depth preserved AND structure is mirror image
theorem tree_invert_correct (t : Tree) :
Tree.depth (tree_invert t) = Tree.depth t
&& Tree.mirror (tree_invert t) = t := by
induction t with
| leaf => rfl
| node val l r ihl ihr =>
simp [tree_invert]
exact <| by omega, by rw [ihl, ihr] |>
</lean4_certificate>
</proof_generation>
</iteration>
</synthesis_tree>
<proof_receipt mode="VERBOSE">
<summary>
<total_iterations>2</total_iterations>
<smt_status>SAT</smt_status>
<lean_status>PROVEN</lean_status>
</summary>
<final_synthesized_ast>
(define tree-invert
(lambda (t)
(if (null? t)
'()
(list (car t) (tree-invert (caddr t)) (tree-invert (cadr t))))))
</final_synthesized_ast>
</proof_receipt>
</execution_node>
|