1/**
2 * Proof verification logic.
3 */
5import { Block } from './block.js';
6import { Expression } from './expression.js';
7import { Context } from './context.js';
8import { VerificationError } from './errors.js';
9import { simplify } from './simplifier.js';
10import { verifyCalculate } from './calculateVerifier.js';
12/**
13 * Verify all axioms and theorems in a file.
14 */
15export function verifyFile(blocks: Block[], verbose: boolean = false): void {
16 // First pass: collect all axioms and theorems
17 const axiomsAndTheorems = new Map<string, Block>();
19 for (const block of blocks) {
20 if (block.blockType === 'axiom' || block.blockType === 'theorem') {
21 if (block.args.length !== 1) {
22 throw new VerificationError(
23 `Line ${block.lineNum}: ${block.blockType} must have exactly one argument (the name)`
24 );
25 }
27 const name = block.args[0].name;
28 if (block.args[0].children.length > 0) {
29 throw new VerificationError(
30 `Line ${block.lineNum}: ${block.blockType} name must be a simple identifier`
31 );
32 }
34 axiomsAndTheorems.set(name, block);
36 if (verbose) {
37 console.log(`Found ${block.blockType}: ${name}`);
38 }
39 } else {
40 throw new VerificationError(
41 `Line ${block.lineNum}: Top-level blocks must be 'axiom' or 'theorem', got '${block.blockType}'`
42 );
43 }
44 }
46 // Second pass: verify theorems
47 for (const block of blocks) {
48 if (block.blockType === 'theorem') {
49 const name = block.args[0].name;
50 if (verbose) {
51 console.log(`\nVerifying theorem: ${name}`);
52 }
53 verifyTheorem(block, axiomsAndTheorems, verbose);
54 if (verbose) {
55 console.log(`✓ Theorem ${name} verified`);
56 }
57 }
58 }
59}
61/**
62 * Verify a single theorem.
63 */
64function verifyTheorem(theoremBlock: Block, axiomsAndTheorems: Map<string, Block>, verbose: boolean): void {
65 // Create initial context from suppose blocks
66 const context = new Context();
68 const supposeBlocks: Block[] = [];
69 let concludeBlock: Block | null = null;
70 let proofBlock: Block | null = null;
72 // Parse structure: suppose* conclude proof
73 for (const child of theoremBlock.children) {
74 if (child.blockType === 'suppose') {
75 supposeBlocks.push(child);
76 } else if (child.blockType === 'conclude') {
77 if (concludeBlock !== null) {
78 throw new VerificationError(`Line ${child.lineNum}: Multiple 'conclude' blocks in theorem`);
79 }
80 concludeBlock = child;
81 } else if (child.blockType === 'proof') {
82 if (proofBlock !== null) {
83 throw new VerificationError(`Line ${child.lineNum}: Multiple 'proof' blocks in theorem`);
84 }
85 proofBlock = child;
86 } else {
87 throw new VerificationError(
88 `Line ${child.lineNum}: Invalid block type '${child.blockType}' in theorem`
89 );
90 }
91 }
93 if (concludeBlock === null) {
94 throw new VerificationError(`Line ${theoremBlock.lineNum}: Theorem missing 'conclude' block`);
95 }
97 if (proofBlock === null) {
98 throw new VerificationError(`Line ${theoremBlock.lineNum}: Theorem missing 'proof' block`);
99 }
101 // Process suppose blocks
102 for (const suppose of supposeBlocks) {
103 processSuppose(suppose, context);
104 }
106 // Process conclude block
107 processConclude(concludeBlock, context);
109 // Verify the proof
110 const goalResolved = verifyProof(proofBlock, context, axiomsAndTheorems, verbose);
112 if (!goalResolved) {
113 throw new VerificationError(`Line ${proofBlock.lineNum}: Proof does not resolve the goal`);
114 }
115}
117/**
118 * Process a suppose block: suppose name : type
119 */
120function processSuppose(supposeBlock: Block, context: Context): void {
121 if (supposeBlock.args.length !== 1) {
122 throw new VerificationError(`Line ${supposeBlock.lineNum}: 'suppose' must have exactly one argument`);
123 }
125 const arg = supposeBlock.args[0];
126 if (arg.name !== 'var' || arg.children.length !== 2) {
127 throw new VerificationError(
128 `Line ${supposeBlock.lineNum}: 'suppose' argument must be of form 'name : type'`
129 );
130 }
132 const varName = arg.children[0].name;
133 const varType = arg.children[1];
135 if (arg.children[0].children.length > 0) {
136 throw new VerificationError(`Line ${supposeBlock.lineNum}: Variable name must be a simple identifier`);
137 }
139 context.addVariable(varName, varType);
140}
142/**
143 * Process a conclude block: conclude type
144 */
145function processConclude(concludeBlock: Block, context: Context): void {
146 if (concludeBlock.args.length !== 1) {
147 throw new VerificationError(`Line ${concludeBlock.lineNum}: 'conclude' must have exactly one argument`);
148 }
150 context.goal = concludeBlock.args[0];
151}
153/**
154 * Verify a proof block and return whether the goal was resolved.
155 */
156function verifyProof(proofBlock: Block, context: Context, axiomsAndTheorems: Map<string, Block>, verbose: boolean): boolean {
157 let goalResolved = false;
159 for (const child of proofBlock.children) {
160 const result = verifyProofStep(child, context, axiomsAndTheorems, verbose);
161 if (result) {
162 goalResolved = true;
163 }
164 }
166 return goalResolved;
167}
169/**
170 * Verify a single proof step. Returns true if the goal was resolved.
171 */
172function verifyProofStep(step: Block, context: Context, axiomsAndTheorems: Map<string, Block>, verbose: boolean): boolean {
173 switch (step.blockType) {
174 case 'unpack-and':
175 return verifyUnpackAnd(step, context, axiomsAndTheorems, verbose);
176 case 'cases':
177 return verifyCases(step, context, axiomsAndTheorems, verbose);
178 case 'witness':
179 return verifyWitness(step, context);
180 case 'assert-goal':
181 return verifyAssertGoal(step, context);
182 case 'exact':
183 return verifyExact(step, context);
184 case 'calculate':
185 return verifyCalculate(step, context, axiomsAndTheorems);
186 case 'assert':
187 return verifyAssert(step, context);
188 case 'define':
189 return verifyDefine(step, context);
190 case 'consider':
191 return verifyConsider(step, context);
192 case 'forall-apply':
193 return verifyForallApply(step, context);
194 case 'deconstruct-exists':
195 return verifyDeconstructExists(step, context);
196 case 'we-have':
197 return verifyWeHave(step, context, axiomsAndTheorems, verbose);
198 case 'focus-or':
199 return verifyFocusOr(step, context);
200 default:
201 throw new VerificationError(`Line ${step.lineNum}: Unknown proof step type '${step.blockType}'`);
202 }
203}
205/**
206 * Verify unpack-and: goal must be and(a, b), requires two goal children.
207 */
208function verifyUnpackAnd(step: Block, context: Context, axiomsAndTheorems: Map<string, Block>, verbose: boolean): boolean {
209 if (step.args.length !== 0) {
210 throw new VerificationError(`Line ${step.lineNum}: 'unpack-and' takes no arguments`);
211 }
213 if (context.goal === null) {
214 throw new VerificationError(`Line ${step.lineNum}: No goal to unpack`);
215 }
217 if (context.goal.name !== 'and' || context.goal.children.length !== 2) {
218 throw new VerificationError(`Line ${step.lineNum}: Goal must be and(a, b), got ${context.goal}`);
219 }
221 if (step.children.length !== 2) {
222 throw new VerificationError(`Line ${step.lineNum}: 'unpack-and' requires exactly 2 children`);
223 }
225 // Verify both children are goal blocks
226 for (let i = 0; i < step.children.length; i++) {
227 const child = step.children[i];
228 if (child.blockType !== 'goal') {
229 throw new VerificationError(`Line ${child.lineNum}: 'unpack-and' children must be 'goal' blocks`);
230 }
232 if (child.args.length !== 1) {
233 throw new VerificationError(`Line ${child.lineNum}: 'goal' must have exactly one argument`);
234 }
236 const expectedGoal = context.goal.children[i];
237 if (!child.args[0].equals(expectedGoal)) {
238 throw new VerificationError(
239 `Line ${child.lineNum}: Expected goal ${expectedGoal}, got ${child.args[0]}`
240 );
241 }
243 // Each goal must have one proof child
244 if (child.children.length !== 1 || child.children[0].blockType !== 'proof') {
245 throw new VerificationError(`Line ${child.lineNum}: 'goal' must have exactly one 'proof' child`);
246 }
248 // Verify the proof with the subgoal
249 const subContext = context.copy();
250 subContext.goal = expectedGoal;
251 const resolved = verifyProof(child.children[0], subContext, axiomsAndTheorems, verbose);
253 if (!resolved) {
254 throw new VerificationError(`Line ${child.lineNum}: Proof does not resolve goal ${expectedGoal}`);
255 }
256 }
258 return true; // Goal resolved
259}
261/**
262 * Verify cases: variable must have type or(a, b), requires two case children.
263 */
264function verifyCases(step: Block, context: Context, axiomsAndTheorems: Map<string, Block>, verbose: boolean): boolean {
265 if (step.args.length !== 1) {
266 throw new VerificationError(`Line ${step.lineNum}: 'cases' takes exactly one argument (variable name)`);
267 }
269 const varName = step.args[0].name;
270 if (step.args[0].children.length > 0) {
271 throw new VerificationError(`Line ${step.lineNum}: 'cases' argument must be a simple variable name`);
272 }
274 if (!context.hasVariable(varName)) {
275 throw new VerificationError(`Line ${step.lineNum}: Variable '${varName}' not in context`);
276 }
278 const varType = context.getVariableType(varName)!;
279 if (varType.name !== 'or' || varType.children.length !== 2) {
280 throw new VerificationError(
281 `Line ${step.lineNum}: Variable '${varName}' must have type or(a, b), got ${varType}`
282 );
283 }
285 if (step.children.length !== 2) {
286 throw new VerificationError(`Line ${step.lineNum}: 'cases' requires exactly 2 'case' children`);
287 }
289 // Verify both case children
290 for (let i = 0; i < step.children.length; i++) {
291 const child = step.children[i];
292 if (child.blockType !== 'case') {
293 throw new VerificationError(`Line ${child.lineNum}: 'cases' children must be 'case' blocks`);
294 }
296 if (child.args.length !== 1) {
297 throw new VerificationError(`Line ${child.lineNum}: 'case' must have exactly one argument`);
298 }
300 const arg = child.args[0];
301 if (arg.name !== 'var' || arg.children.length !== 2) {
302 throw new VerificationError(`Line ${child.lineNum}: 'case' argument must be of form 'name : type'`);
303 }
305 const caseVarName = arg.children[0].name;
306 const caseType = arg.children[1];
308 const expectedType = varType.children[i];
309 if (!caseType.equals(expectedType)) {
310 throw new VerificationError(
311 `Line ${child.lineNum}: Expected case type ${expectedType}, got ${caseType}`
312 );
313 }
315 // Verify proof with added case variable
316 const caseContext = context.copy();
317 caseContext.addVariable(caseVarName, caseType);
319 // Each case needs a proof
320 if (child.children.length !== 1 || child.children[0].blockType !== 'proof') {
321 throw new VerificationError(`Line ${child.lineNum}: 'case' must have exactly one 'proof' child`);
322 }
324 const resolved = verifyProof(child.children[0], caseContext, axiomsAndTheorems, verbose);
325 if (!resolved) {
326 throw new VerificationError(`Line ${child.lineNum}: Proof in case does not resolve goal`);
327 }
328 }
330 return true; // Goal resolved
331}
333/**
334 * Verify witness: goal must be exists(var(name, type), body), modifies goal.
335 */
336function verifyWitness(step: Block, context: Context): boolean {
337 if (step.args.length !== 1) {
338 throw new VerificationError(`Line ${step.lineNum}: 'witness' takes exactly one argument`);
339 }
341 const witnessName = step.args[0].name;
342 if (step.args[0].children.length > 0) {
343 throw new VerificationError(`Line ${step.lineNum}: 'witness' argument must be a simple identifier`);
344 }
346 if (context.goal === null) {
347 throw new VerificationError(`Line ${step.lineNum}: No goal for witness`);
348 }
350 if (context.goal.name !== 'exists' || context.goal.children.length !== 2) {
351 throw new VerificationError(
352 `Line ${step.lineNum}: Goal must be exists(var(name, type), body), got ${context.goal}`
353 );
354 }
356 const varExpr = context.goal.children[0];
357 if (varExpr.name !== 'var' || varExpr.children.length !== 2) {
358 throw new VerificationError(
359 `Line ${step.lineNum}: exists must have var(name, type) as first argument`
360 );
361 }
363 const boundVarName = varExpr.children[0].name;
364 const body = context.goal.children[1];
366 // Substitute witness into body
367 context.goal = body.substitute(boundVarName, new Expression(witnessName));
369 return false; // Does not resolve goal
370}
372/**
373 * Verify assert-goal: expression must match current goal.
374 */
375function verifyAssertGoal(step: Block, context: Context): boolean {
376 if (step.args.length !== 1) {
377 throw new VerificationError(`Line ${step.lineNum}: 'assert-goal' takes exactly one argument`);
378 }
380 const expectedGoal = step.args[0];
382 if (context.goal === null) {
383 throw new VerificationError(`Line ${step.lineNum}: No current goal`);
384 }
386 if (!context.goal.equals(expectedGoal)) {
387 throw new VerificationError(
388 `Line ${step.lineNum}: Expected goal ${expectedGoal}, but current goal is ${context.goal}`
389 );
390 }
392 return false; // Does not resolve goal
393}
395/**
396 * Verify exact: two variants - variable name or expression after simplification.
397 */
398function verifyExact(step: Block, context: Context): boolean {
399 if (step.args.length !== 1) {
400 throw new VerificationError(`Line ${step.lineNum}: 'exact' takes exactly one argument`);
401 }
403 const arg = step.args[0];
405 if (context.goal === null) {
406 throw new VerificationError(`Line ${step.lineNum}: No goal to resolve`);
407 }
409 // Variant 1: Simple variable name
410 if (arg.children.length === 0 && context.hasVariable(arg.name)) {
411 const varType = context.getVariableType(arg.name)!;
412 if (!varType.equals(context.goal)) {
413 throw new VerificationError(
414 `Line ${step.lineNum}: Variable '${arg.name}' has type ${varType}, but goal is ${context.goal}`
415 );
416 }
417 return true; // Goal resolved
418 }
420 // Variant 2: Expression after simplification
421 const simplified = simplify(arg, context);
422 if (!simplified.equals(context.goal)) {
423 throw new VerificationError(
424 `Line ${step.lineNum}: Expression ${arg} simplifies to ${simplified}, but goal is ${context.goal}`
425 );
426 }
428 return true; // Goal resolved
429}
431/**
432 * Verify assert: assert name : type.
433 */
434function verifyAssert(step: Block, context: Context): boolean {
435 if (step.args.length !== 1) {
436 throw new VerificationError(`Line ${step.lineNum}: 'assert' must have exactly one argument`);
437 }
439 const arg = step.args[0];
440 if (arg.name !== 'var' || arg.children.length !== 2) {
441 throw new VerificationError(`Line ${step.lineNum}: 'assert' argument must be of form 'name : type'`);
442 }
444 const varName = arg.children[0].name;
445 const expectedType = arg.children[1];
447 if (!context.hasVariable(varName)) {
448 throw new VerificationError(`Line ${step.lineNum}: Variable '${varName}' not in context`);
449 }
451 const actualType = context.getVariableType(varName)!;
452 if (!actualType.equals(expectedType)) {
453 throw new VerificationError(
454 `Line ${step.lineNum}: Variable '${varName}' has type ${actualType}, expected ${expectedType}`
455 );
456 }
458 return false; // Does not resolve goal
459}
461/**
462 * Verify define: define name : eq(lhs, rhs).
463 */
464function verifyDefine(step: Block, context: Context): boolean {
465 if (step.args.length !== 1) {
466 throw new VerificationError(`Line ${step.lineNum}: 'define' must have exactly one argument`);
467 }
469 const arg = step.args[0];
470 if (arg.name !== 'var' || arg.children.length !== 2) {
471 throw new VerificationError(`Line ${step.lineNum}: 'define' argument must be of form 'name : type'`);
472 }
474 const varName = arg.children[0].name;
475 const varType = arg.children[1];
477 if (context.hasVariable(varName)) {
478 throw new VerificationError(`Line ${step.lineNum}: Variable '${varName}' already in context`);
479 }
481 // Check that type is an eq expression
482 if (varType.name !== 'eq' || varType.children.length !== 2) {
483 throw new VerificationError(`Line ${step.lineNum}: 'define' type must be eq(lhs, rhs)`);
484 }
486 context.addVariable(varName, varType);
488 return false; // Does not resolve goal
489}
491/**
492 * Verify consider: goal must be forall(var(name, type), body).
493 */
494function verifyConsider(step: Block, context: Context): boolean {
495 if (step.args.length !== 1) {
496 throw new VerificationError(`Line ${step.lineNum}: 'consider' takes exactly one argument`);
497 }
499 const varName = step.args[0].name;
500 if (step.args[0].children.length > 0) {
501 throw new VerificationError(`Line ${step.lineNum}: 'consider' argument must be a simple identifier`);
502 }
504 if (context.goal === null) {
505 throw new VerificationError(`Line ${step.lineNum}: No goal for consider`);
506 }
508 if (context.goal.name !== 'forall' || context.goal.children.length !== 2) {
509 throw new VerificationError(
510 `Line ${step.lineNum}: Goal must be forall(var(name, type), body), got ${context.goal}`
511 );
512 }
514 const varExpr = context.goal.children[0];
515 if (varExpr.name !== 'var' || varExpr.children.length !== 2) {
516 throw new VerificationError(
517 `Line ${step.lineNum}: forall must have var(name, type) as first argument`
518 );
519 }
521 const boundVarName = varExpr.children[0].name;
522 const varType = varExpr.children[1];
523 const body = context.goal.children[1];
525 if (boundVarName !== varName) {
526 throw new VerificationError(
527 `Line ${step.lineNum}: Expected variable '${boundVarName}', got '${varName}'`
528 );
529 }
531 context.addVariable(varName, varType);
532 context.goal = body;
534 return false; // Does not resolve goal
535}
537/**
538 * Verify forall-apply: apply forall to an argument.
539 */
540function verifyForallApply(step: Block, context: Context): boolean {
541 if (step.args.length !== 3) {
542 throw new VerificationError(`Line ${step.lineNum}: 'forall-apply' takes exactly 3 arguments`);
543 }
545 const forallVar = step.args[0].name;
546 const argVar = step.args[1].name;
547 const resultVar = step.args[2].name;
549 if (step.args[0].children.length > 0 || step.args[1].children.length > 0 || step.args[2].children.length > 0) {
550 throw new VerificationError(
551 `Line ${step.lineNum}: 'forall-apply' arguments must be simple identifiers`
552 );
553 }
555 if (!context.hasVariable(forallVar)) {
556 throw new VerificationError(`Line ${step.lineNum}: Variable '${forallVar}' not in context`);
557 }
559 if (!context.hasVariable(argVar)) {
560 throw new VerificationError(`Line ${step.lineNum}: Variable '${argVar}' not in context`);
561 }
563 if (context.hasVariable(resultVar)) {
564 throw new VerificationError(`Line ${step.lineNum}: Variable '${resultVar}' already in context`);
565 }
567 const forallType = context.getVariableType(forallVar)!;
568 if (forallType.name !== 'forall' || forallType.children.length !== 2) {
569 throw new VerificationError(
570 `Line ${step.lineNum}: Variable '${forallVar}' must have type forall(var(name, type), body)`
571 );
572 }
574 const varExpr = forallType.children[0];
575 if (varExpr.name !== 'var' || varExpr.children.length !== 2) {
576 throw new VerificationError(
577 `Line ${step.lineNum}: forall must have var(name, type) as first argument`
578 );
579 }
581 const boundVarName = varExpr.children[0].name;
582 const expectedArgType = varExpr.children[1];
583 const body = forallType.children[1];
585 const argType = context.getVariableType(argVar)!;
586 if (!argType.equals(expectedArgType)) {
587 throw new VerificationError(
588 `Line ${step.lineNum}: Argument '${argVar}' has type ${argType}, expected ${expectedArgType}`
589 );
590 }
592 // Substitute argVar for boundVarName in body
593 const resultType = body.substitute(boundVarName, new Expression(argVar));
594 context.addVariable(resultVar, resultType);
596 return false; // Does not resolve goal
597}
599/**
600 * Verify deconstruct-exists: extract witness and hypothesis from exists.
601 */
602function verifyDeconstructExists(step: Block, context: Context): boolean {
603 if (step.args.length !== 3) {
604 throw new VerificationError(`Line ${step.lineNum}: 'deconstruct-exists' takes exactly 3 arguments`);
605 }
607 const existsVar = step.args[0].name;
608 const witnessVar = step.args[1].name;
609 const hypVar = step.args[2].name;
611 if (step.args[0].children.length > 0 || step.args[1].children.length > 0 || step.args[2].children.length > 0) {
612 throw new VerificationError(
613 `Line ${step.lineNum}: 'deconstruct-exists' arguments must be simple identifiers`
614 );
615 }
617 if (!context.hasVariable(existsVar)) {
618 throw new VerificationError(`Line ${step.lineNum}: Variable '${existsVar}' not in context`);
619 }
621 if (context.hasVariable(witnessVar)) {
622 throw new VerificationError(`Line ${step.lineNum}: Variable '${witnessVar}' already in context`);
623 }
625 if (context.hasVariable(hypVar)) {
626 throw new VerificationError(`Line ${step.lineNum}: Variable '${hypVar}' already in context`);
627 }
629 const existsType = context.getVariableType(existsVar)!;
630 if (existsType.name !== 'exists' || existsType.children.length !== 2) {
631 throw new VerificationError(
632 `Line ${step.lineNum}: Variable '${existsVar}' must have type exists(var(name, type), body)`
633 );
634 }
636 const varExpr = existsType.children[0];
637 if (varExpr.name !== 'var' || varExpr.children.length !== 2) {
638 throw new VerificationError(
639 `Line ${step.lineNum}: exists must have var(name, type) as first argument`
640 );
641 }
643 const boundVarName = varExpr.children[0].name;
644 const witnessType = varExpr.children[1];
645 const body = existsType.children[1];
647 // Add witness variable and hypothesis variable
648 context.addVariable(witnessVar, witnessType);
649 const hypType = body.substitute(boundVarName, new Expression(witnessVar));
650 context.addVariable(hypVar, hypType);
652 return false; // Does not resolve goal
653}
655/**
656 * Verify we-have: prove intermediate result.
657 */
658function verifyWeHave(step: Block, context: Context, axiomsAndTheorems: Map<string, Block>, verbose: boolean): boolean {
659 if (step.args.length !== 1) {
660 throw new VerificationError(`Line ${step.lineNum}: 'we-have' must have exactly one argument`);
661 }
663 const arg = step.args[0];
664 if (arg.name !== 'var' || arg.children.length !== 2) {
665 throw new VerificationError(`Line ${step.lineNum}: 'we-have' argument must be of form 'name : type'`);
666 }
668 const varName = arg.children[0].name;
669 const varType = arg.children[1];
671 if (context.hasVariable(varName)) {
672 throw new VerificationError(`Line ${step.lineNum}: Variable '${varName}' already in context`);
673 }
675 if (step.children.length !== 1 || step.children[0].blockType !== 'proof') {
676 throw new VerificationError(`Line ${step.lineNum}: 'we-have' must have exactly one 'proof' child`);
677 }
679 // Verify the proof with the new goal
680 const subContext = context.copy();
681 subContext.goal = varType;
682 const resolved = verifyProof(step.children[0], subContext, axiomsAndTheorems, verbose);
684 if (!resolved) {
685 throw new VerificationError(`Line ${step.lineNum}: Proof does not establish ${varType}`);
686 }
688 context.addVariable(varName, varType);
690 return false; // Does not resolve goal
691}
693/**
694 * Verify focus-or: goal must be or(a, b), focus on left or right.
695 */
696function verifyFocusOr(step: Block, context: Context): boolean {
697 if (step.args.length !== 1) {
698 throw new VerificationError(`Line ${step.lineNum}: 'focus-or' takes exactly one argument`);
699 }
701 const direction = step.args[0].name;
702 if (step.args[0].children.length > 0 || (direction !== 'left' && direction !== 'right')) {
703 throw new VerificationError(`Line ${step.lineNum}: 'focus-or' argument must be 'left' or 'right'`);
704 }
706 if (context.goal === null) {
707 throw new VerificationError(`Line ${step.lineNum}: No goal for focus-or`);
708 }
710 if (context.goal.name !== 'or' || context.goal.children.length !== 2) {
711 throw new VerificationError(`Line ${step.lineNum}: Goal must be or(a, b), got ${context.goal}`);
712 }
714 if (direction === 'left') {
715 context.goal = context.goal.children[0];
716 } else {
717 context.goal = context.goal.children[1];
718 }
720 return false; // Does not resolve goal
721}