|
12 | 12 | // If not, see <http://creativecommons.org/publicdomain/zero/1.0/>.
|
13 | 13 | //
|
14 | 14 |
|
15 |
| -use crate::core::{ProgramNode, Term, TypedNode, Value}; |
| 15 | +use crate::core::commit::CommitNodeInner; |
| 16 | +use crate::core::node::{NodeBounds, NodeType}; |
| 17 | +use crate::core::Value; |
| 18 | +use crate::core::{CommitNode, Node}; |
16 | 19 | use crate::jet::Application;
|
17 | 20 | use std::cmp;
|
| 21 | +use std::rc::Rc; |
18 | 22 |
|
19 |
| -/// Return an upper bound on the number of cells required by the given `node` |
20 |
| -/// inside the given `program` during execution on the Bit Machine. |
21 |
| -pub(crate) fn compute_extra_cells_bound<App: Application>( |
22 |
| - program: &[ProgramNode<App>], |
23 |
| - node: &TypedNode<Value, App>, |
| 23 | +/// Return the bounds for the given node, once finalized. |
| 24 | +/// |
| 25 | +/// Nodes with left children require their finalized left child, |
| 26 | +/// while nodes with right children require their finalized right child. |
| 27 | +/// Witness nodes require their node type. |
| 28 | +pub(crate) fn compute_bounds<Witness, App: Application>( |
| 29 | + untyped_node: &CommitNode<Witness, App>, |
| 30 | + left: Option<Rc<Node<Value, App>>>, |
| 31 | + right: Option<Rc<Node<Value, App>>>, |
| 32 | + ty: &NodeType, |
| 33 | +) -> NodeBounds { |
| 34 | + NodeBounds { |
| 35 | + extra_cells: compute_extra_cells_bound(untyped_node, left.clone(), right.clone(), ty), |
| 36 | + frame_count: compute_frame_count_bound(untyped_node, left, right), |
| 37 | + } |
| 38 | +} |
| 39 | + |
| 40 | +/// Return an upper bound on the number of cells required |
| 41 | +/// by the given node during execution on the Bit Machine. |
| 42 | +fn compute_extra_cells_bound<Witness, App: Application>( |
| 43 | + untyped_node: &CommitNode<Witness, App>, |
| 44 | + left: Option<Rc<Node<Value, App>>>, |
| 45 | + right: Option<Rc<Node<Value, App>>>, |
| 46 | + ty: &NodeType, |
24 | 47 | ) -> usize {
|
25 |
| - match node.term { |
26 |
| - Term::Iden | Term::Unit | Term::Fail(..) | Term::Hidden(..) | Term::Jet(..) => 0, |
27 |
| - Term::InjL(i) | Term::InjR(i) | Term::Take(i) | Term::Drop(i) => { |
28 |
| - program[node.index - i].extra_cells_bound |
| 48 | + match untyped_node.inner { |
| 49 | + CommitNodeInner::Iden |
| 50 | + | CommitNodeInner::Unit |
| 51 | + | CommitNodeInner::Fail(_, _) |
| 52 | + | CommitNodeInner::Hidden(_) |
| 53 | + | CommitNodeInner::Jet(_) => 0, |
| 54 | + CommitNodeInner::InjL(_) |
| 55 | + | CommitNodeInner::InjR(_) |
| 56 | + | CommitNodeInner::Take(_) |
| 57 | + | CommitNodeInner::Drop(_) => left.unwrap().bounds.extra_cells, |
| 58 | + CommitNodeInner::Comp(_, _) => { |
| 59 | + let left = left.unwrap(); |
| 60 | + left.ty.target.bit_width |
| 61 | + + cmp::max(left.bounds.extra_cells, right.unwrap().bounds.extra_cells) |
29 | 62 | }
|
30 |
| - Term::Comp(i, j) => { |
31 |
| - program[node.index - i].target_ty().bit_width |
32 |
| - + cmp::max( |
33 |
| - program[node.index - i].extra_cells_bound, |
34 |
| - program[node.index - j].extra_cells_bound, |
35 |
| - ) |
36 |
| - } |
37 |
| - Term::Case(i, j) | Term::AssertL(i, j) | Term::AssertR(i, j) | Term::Pair(i, j) => { |
38 |
| - cmp::max( |
39 |
| - program[node.index - i].extra_cells_bound, |
40 |
| - program[node.index - j].extra_cells_bound, |
41 |
| - ) |
| 63 | + CommitNodeInner::Case(_, _) |
| 64 | + | CommitNodeInner::AssertL(_, _) |
| 65 | + | CommitNodeInner::AssertR(_, _) |
| 66 | + | CommitNodeInner::Pair(_, _) => cmp::max( |
| 67 | + left.unwrap().bounds.extra_cells, |
| 68 | + right.unwrap().bounds.extra_cells, |
| 69 | + ), |
| 70 | + CommitNodeInner::Disconnect(_, _) => { |
| 71 | + let left = left.unwrap(); |
| 72 | + left.ty.source.bit_width |
| 73 | + + left.ty.target.bit_width |
| 74 | + + cmp::max(left.bounds.extra_cells, right.unwrap().bounds.extra_cells) |
42 | 75 | }
|
43 |
| - Term::Disconnect(i, j) => { |
44 |
| - program[node.index - i].source_ty().bit_width |
45 |
| - + program[node.index - i].target_ty().bit_width |
46 |
| - + cmp::max( |
47 |
| - program[node.index - i].extra_cells_bound, |
48 |
| - program[node.index - j].extra_cells_bound, |
49 |
| - ) |
50 |
| - } |
51 |
| - Term::Witness(..) => node.target_ty.bit_width, |
| 76 | + CommitNodeInner::Witness(_) => ty.target.bit_width, |
52 | 77 | }
|
53 | 78 | }
|
54 | 79 |
|
55 |
| -/// Return an upper bound on the number of frames required by the given `node` |
56 |
| -/// inside the given `program` during execution on the Bit Machine. |
57 |
| -pub(crate) fn compute_frame_count_bound<App: Application>( |
58 |
| - program: &[ProgramNode<App>], |
59 |
| - node: &TypedNode<Value, App>, |
| 80 | +/// Return an upper bound on the number of frames required |
| 81 | +/// by the given node during execution on the Bit Machine. |
| 82 | +fn compute_frame_count_bound<Witness, App: Application>( |
| 83 | + untyped_node: &CommitNode<Witness, App>, |
| 84 | + left: Option<Rc<Node<Value, App>>>, |
| 85 | + right: Option<Rc<Node<Value, App>>>, |
60 | 86 | ) -> usize {
|
61 |
| - match node.term { |
62 |
| - Term::Iden |
63 |
| - | Term::Unit |
64 |
| - | Term::Witness(..) |
65 |
| - | Term::Fail(..) |
66 |
| - | Term::Hidden(..) |
67 |
| - | Term::Jet(..) => 0, |
68 |
| - Term::InjL(i) | Term::InjR(i) | Term::Take(i) | Term::Drop(i) => { |
69 |
| - program[node.index - i].frame_count_bound |
70 |
| - } |
71 |
| - Term::Comp(i, j) => { |
| 87 | + match untyped_node.inner { |
| 88 | + CommitNodeInner::Iden |
| 89 | + | CommitNodeInner::Unit |
| 90 | + | CommitNodeInner::Witness(_) |
| 91 | + | CommitNodeInner::Fail(_, _) |
| 92 | + | CommitNodeInner::Hidden(_) |
| 93 | + | CommitNodeInner::Jet(_) => 0, |
| 94 | + CommitNodeInner::InjL(_) |
| 95 | + | CommitNodeInner::InjR(_) |
| 96 | + | CommitNodeInner::Take(_) |
| 97 | + | CommitNodeInner::Drop(_) => left.unwrap().bounds.frame_count, |
| 98 | + CommitNodeInner::Comp(_, _) => { |
72 | 99 | 1 + cmp::max(
|
73 |
| - program[node.index - i].frame_count_bound, |
74 |
| - program[node.index - j].frame_count_bound, |
75 |
| - ) |
76 |
| - } |
77 |
| - Term::Case(i, j) | Term::AssertL(i, j) | Term::AssertR(i, j) | Term::Pair(i, j) => { |
78 |
| - cmp::max( |
79 |
| - program[node.index - i].frame_count_bound, |
80 |
| - program[node.index - j].frame_count_bound, |
| 100 | + left.unwrap().bounds.frame_count, |
| 101 | + right.unwrap().bounds.frame_count, |
81 | 102 | )
|
82 | 103 | }
|
83 |
| - Term::Disconnect(i, j) => { |
| 104 | + CommitNodeInner::Case(_, _) |
| 105 | + | CommitNodeInner::AssertL(_, _) |
| 106 | + | CommitNodeInner::AssertR(_, _) |
| 107 | + | CommitNodeInner::Pair(_, _) => cmp::max( |
| 108 | + left.unwrap().bounds.frame_count, |
| 109 | + right.unwrap().bounds.frame_count, |
| 110 | + ), |
| 111 | + CommitNodeInner::Disconnect(_, _) => { |
84 | 112 | 2 + cmp::max(
|
85 |
| - program[node.index - i].frame_count_bound, |
86 |
| - program[node.index - j].frame_count_bound, |
| 113 | + left.unwrap().bounds.frame_count, |
| 114 | + right.unwrap().bounds.frame_count, |
87 | 115 | )
|
88 | 116 | }
|
89 | 117 | }
|
|
0 commit comments