f_select_children.dfy 4.18 KB
Newer Older
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
// Types

type Position(==)

type PositionScorePair(==)
function method get_position(pair: PositionScorePair): Position
function method get_score(pair: PositionScorePair): real

// Language Constants

const undefined: real

// Program Constants

const PROBE_DEPTH: nat
const FORWARD_PRUNING_TARGET: real

// Functions to Make Assertions Easier to Write

function minimum_count_for(position: Position, taboo: set<Position>): real
  ensures minimum_count_for(position, taboo) == FORWARD_PRUNING_TARGET * |get_available_children(position, taboo)| as real

function score_at(position: Position, depth: nat): real

// Helper Methods

function method sort_by_static_evaluation(positions: seq<Position>): seq<Position>
  ensures |sort_by_static_evaluation(positions)| == |positions|

function method get_available_children(position: Position, taboo: set<Position>): seq<Position>

function method order_children_inexactly(request_number: nat, position: Position, taboo: set<Position>, depth: nat, is_book: Position -> bool): seq<PositionScorePair>
  ensures
    forall p | p in order_children_inexactly(request_number, position, taboo, depth, is_book) ::
    get_score(p) == score_at(get_position(p), depth)
  ensures
    forall i | 0 <= i < |order_children_inexactly(request_number, position, taboo, depth, is_book)| ::
    forall j | i < j < |order_children_inexactly(request_number, position, taboo, depth, is_book)|::
    get_score(order_children_inexactly(request_number, position, taboo, depth, is_book)[i]) >= get_score(order_children_inexactly(request_number, position, taboo, depth, is_book)[j])
  ensures |order_children_inexactly(request_number, position, taboo, depth, is_book)| == |get_available_children(position, taboo)|
  ensures |order_children_inexactly(request_number, position, taboo, depth, is_book)| as real >= minimum_count_for(position, taboo)

// Method to Verify

method select_children(request_number: nat, position: Position, taboo: set<Position>, depth: nat, is_book: Position -> bool) returns (children: seq<Position>)
  requires 0.0 < FORWARD_PRUNING_TARGET < 1.0
  ensures |children| <= |get_available_children(position, taboo)|
  ensures
    depth > PROBE_DEPTH ==>
    forall i | 0 <= i < |children| ::
    children[i] == get_position(order_children_inexactly(request_number, position, taboo, PROBE_DEPTH, is_book)[i])
  ensures
    depth > PROBE_DEPTH ==>
    forall i | 0 <= i < |children| ::
    forall j | i < j < |children| ::
    score_at(children[i], PROBE_DEPTH) >= score_at(children[j], PROBE_DEPTH)
  ensures
    depth > PROBE_DEPTH ==>
    |children| as real >= minimum_count_for(position, taboo)
  ensures
    depth > PROBE_DEPTH ==>
    forall i | 0 <= i < |children| ::
    minimum_count_for(position, taboo) <= i as real ==>
    score_at(children[i], PROBE_DEPTH) == score_at(children[i - 1], PROBE_DEPTH)
{
  if depth <= PROBE_DEPTH {
    return sort_by_static_evaluation(get_available_children(position, taboo));
  }
  var candidates := order_children_inexactly(request_number, position, taboo, PROBE_DEPTH, is_book);
  var minimum_count := FORWARD_PRUNING_TARGET * |candidates| as real;
  var results := [];
  var previous_score := undefined;
  var index := 0;
  while index < |candidates|
    invariant index == |results|
  {
    var candidate := get_position(candidates[index]);
    var score := get_score(candidates[index]);
    if score != previous_score && |results| as real >= minimum_count {
      break;
    }
    results := results + [candidate];
    previous_score := score;
    index := index + 1;
  }
  return results;
}

// Original JavaScript

// async function selectChildren(requestNumber, position, taboo, depth, isBook) {
//   if (depth <= PROBE_DEPTH) {
//     return getAvailableChildren(position, taboo).sort(byStaticEvaluation);
//   }
//   const candidates = await orderChildrenInexactly(requestNumber, position, taboo, PROBE_DEPTH, isBook);
//   const minimumCount = FORWARD_PRUNING_TARGET * candidates.length;
//   const results = [];
//   let previousScore = undefined;
//   for (const [candidate, score] of candidates) {
//     if (score !== previousScore && results.length >= minimumCount) {
//       break;
//     }
//     results.push(candidate);
//     previousScore = score;
//   }
//   return results;
// }