@@ -7,29 +7,50 @@ namespace memTrace(256);
77 pol commit m_clk;
88 pol commit m_sub_clk;
99 pol commit m_addr;
10+ pol commit m_tag; // Memory tag (0: uninitialized, 1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6:field)
1011 pol commit m_val;
1112 pol commit m_lastAccess; // Boolean (1 when this row is the last of a given address)
13+ pol commit m_last; // Boolean indicating the last row of the memory trace (not execution trace)
1214 pol commit m_rw; // Enum: 0 (read), 1 (write)
13-
15+
16+ pol commit m_in_tag; // Instruction memory tag ("foreign key" pointing to avmMini.in_tag)
17+
18+ // Error columns
19+ pol commit m_tag_err; // Boolean (1 if m_in_tag != m_tag is detected)
20+
21+ // Helper columns
22+ pol commit m_one_min_inv; // Extra value to prove m_in_tag != m_tag with error handling
23+
1424 // Type constraints
1525 m_lastAccess * (1 - m_lastAccess) = 0;
26+ m_last * (1 - m_last) = 0;
1627 m_rw * (1 - m_rw) = 0;
17-
28+ m_tag_err * (1 - m_tag_err) = 0;
29+
30+ // TODO: m_addr is u32 and 0 <= m_tag <= 6
31+ // (m_in_tag will be constrained through inclusion check to main trace)
32+
33+ // Remark: m_lastAccess == 1 on first row and therefore any relation with the
34+ // multiplicative term (1 - m_lastAccess) implicitly includes (1 - avmMini.first)
35+ // Similarly, this includes (1 - m_last) as well.
36+
1837 // m_lastAccess == 0 ==> m_addr' == m_addr
19- (1 - avmMini.first) * (1 - m_lastAccess) * (m_addr' - m_addr) = 0;
38+ // Optimization: We removed the term (1 - avmMini.first)
39+ #[MEM_LAST_ACCESS_DELIMITER]
40+ (1 - m_lastAccess) * (m_addr' - m_addr) = 0;
2041
2142 // We need: m_lastAccess == 1 ==> m_addr' > m_addr
2243 // The above implies: m_addr' == m_addr ==> m_lastAccess == 0
2344 // This condition does not apply on the last row.
2445 // clk + 1 used as an expression for positive integers
2546 // TODO: Uncomment when lookups are supported
26- // (1 - first) * (1 - last ) * m_lastAccess { (m_addr' - m_addr) } in clk + 1; // Gated inclusion check. Is it supported?
47+ // (1 - first) * (1 - m_last ) * m_lastAccess { (m_addr' - m_addr) } in clk + 1; // Gated inclusion check. Is it supported?
2748
2849 // TODO: following constraint
2950 // m_addr' == m_addr && m_clk == m_clk' ==> m_sub_clk' - m_sub_clk > 0
30- // Can be enforced with (1 - first) * (1 - last) * (1 - m_lastAccess) { 6 * (m_clk' - m_clk) + m_sub_clk' - m_sub_clk } in clk + 1
51+ // Can be enforced with (1 - first) * (1 - m_lastAccess) { 6 * (m_clk' - m_clk) + m_sub_clk' - m_sub_clk } in clk + 1
3152
32- // Alternatively to the above, one could require
53+ // Alternatively to the above, one could require
3354 // that m_addr' - m_addr is 0 or 1 (needs to add placeholders m_addr values):
3455 // (m_addr' - m_addr) * (m_addr' - m_addr) - (m_addr' - m_addr) = 0;
3556 // if m_addr' - m_addr is 0 or 1, the following is equiv. to m_lastAccess
@@ -40,8 +61,46 @@ namespace memTrace(256);
4061 // Note: in barretenberg, a shifted polynomial will be 0 on the last row (shift is not cyclic)
4162 // Note2: in barretenberg, if a poynomial is shifted, its non-shifted equivalent must be 0 on the first row
4263
43- (1 - avmMini.first) * (1 - avmMini.last) * (1 - m_lastAccess) * (1 - m_rw') * (m_val' - m_val) = 0;
64+ // Optimization: We removed the term (1 - avmMini.first) and (1 - m_last)
65+ #[MEM_READ_WRITE_VAL_CONSISTENCY]
66+ (1 - m_lastAccess) * (1 - m_rw') * (m_val' - m_val) = 0;
4467
45- // TODO: Constraint the first load from a given adress has value 0. (Consistency of memory initialization.)
68+ // m_lastAccess == 0 && m_rw' == 0 ==> m_tag == m_tag'
69+ // Optimization: We removed the term (1 - avmMini.first) and (1 - m_last)
70+ #[MEM_READ_WRITE_TAG_CONSISTENCY]
71+ (1 - m_lastAccess) * (1 - m_rw') * (m_tag' - m_tag) = 0;
72+
73+ // Constrain that the first load from a given address has value 0. (Consistency of memory initialization.)
74+ // We do not constrain that the m_tag == 0 as the 0 value is compatible with any memory type.
75+ // If we set m_lastAccess = 1 on the first row, we can enforce this (should be ok as long as we do not shift m_lastAccess):
76+ #[MEM_ZERO_INIT]
77+ m_lastAccess * (1 - m_rw') * m_val' = 0;
78+
79+ // Memory tag consistency check
80+ // We want to prove that m_in_tag == m_tag <==> m_tag_err == 0
81+ // We want to show that we can invert (m_in_tag - m_tag) when m_tag_err == 1,
82+ // i.e., m_tag_err == 1 ==> m_in_tag != m_tag
83+ // For this purpose, we need an extra column to store a witness
84+ // which can be used to show that (m_in_tag - m_tag) is invertible (non-zero).
85+ // We re-use the same zero (non)-equality technique as in SUBOP_DIVISION_ZERO_ERR1/2 applied
86+ // to (m_in_tag - m_tag) by replacing m_tag_err by 1 - m_tag_err because here
87+ // the equality to zero is not an error. Another modification
88+ // consists in storing 1 - (m_in_tag - m_tag)^(-1) in the extra witness column
89+ // instead of (m_in_tag - m_tag)^(-1) as this allows to store zero by default (i.e., when m_tag_err == 0).
90+ // The new column m_one_min_inv is set to 1 - (m_in_tag - m_tag)^(-1) when m_tag_err == 1
91+ // but must be set to 0 when tags are matching and m_tag_err = 0
92+ #[MEM_IN_TAG_CONSISTENCY_1]
93+ (m_in_tag - m_tag) * (1 - m_one_min_inv) - m_tag_err = 0;
94+ #[MEM_IN_TAG_CONSISTENCY_2]
95+ (1 - m_tag_err) * m_one_min_inv = 0;
96+
97+ // Correctness of two above checks MEM_IN_TAG_CONSISTENCY_1/2:
98+ // m_in_tag == m_tag ==> m_tag_err == 0 (first relation)
99+ // m_tag_err == 0 ==> m_one_min_inv == 0 by second relation. First relation ==> m_in_tag - m_tag == 0
100+
46101 // TODO: when introducing load/store as sub-operations, we will have to add consistency of intermediate
47- // register values ia, ib, ic
102+ // register values ia, ib, ic
103+
104+ // Inter-table Constraints
105+
106+ // TODO: {m_clk, m_in_tag} IN {avmMini.clk, avmMini.in_tag}
0 commit comments