@@ -1742,39 +1742,97 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
17421742
17431743 // Non-padding multiplicity: sum of all ALU selector flags
17441744 let non_pad_mult = Multiplicity :: Linear ( vec ! [
1745- LinearTerm :: Column { coefficient: 1 , column: cols:: ADD } ,
1746- LinearTerm :: Column { coefficient: 1 , column: cols:: SUB } ,
1747- LinearTerm :: Column { coefficient: 1 , column: cols:: SLT } ,
1748- LinearTerm :: Column { coefficient: 1 , column: cols:: AND } ,
1749- LinearTerm :: Column { coefficient: 1 , column: cols:: OR } ,
1750- LinearTerm :: Column { coefficient: 1 , column: cols:: XOR } ,
1751- LinearTerm :: Column { coefficient: 1 , column: cols:: SHIFT } ,
1752- LinearTerm :: Column { coefficient: 1 , column: cols:: JALR } ,
1753- LinearTerm :: Column { coefficient: 1 , column: cols:: BEQ } ,
1754- LinearTerm :: Column { coefficient: 1 , column: cols:: BLT } ,
1755- LinearTerm :: Column { coefficient: 1 , column: cols:: LOAD } ,
1756- LinearTerm :: Column { coefficient: 1 , column: cols:: STORE } ,
1757- LinearTerm :: Column { coefficient: 1 , column: cols:: MUL } ,
1758- LinearTerm :: Column { coefficient: 1 , column: cols:: DIVREM } ,
1759- LinearTerm :: Column { coefficient: 1 , column: cols:: ECALL } ,
1760- LinearTerm :: Column { coefficient: 1 , column: cols:: EBREAK } ,
1745+ LinearTerm :: Column {
1746+ coefficient: 1 ,
1747+ column: cols:: ADD ,
1748+ } ,
1749+ LinearTerm :: Column {
1750+ coefficient: 1 ,
1751+ column: cols:: SUB ,
1752+ } ,
1753+ LinearTerm :: Column {
1754+ coefficient: 1 ,
1755+ column: cols:: SLT ,
1756+ } ,
1757+ LinearTerm :: Column {
1758+ coefficient: 1 ,
1759+ column: cols:: AND ,
1760+ } ,
1761+ LinearTerm :: Column {
1762+ coefficient: 1 ,
1763+ column: cols:: OR ,
1764+ } ,
1765+ LinearTerm :: Column {
1766+ coefficient: 1 ,
1767+ column: cols:: XOR ,
1768+ } ,
1769+ LinearTerm :: Column {
1770+ coefficient: 1 ,
1771+ column: cols:: SHIFT ,
1772+ } ,
1773+ LinearTerm :: Column {
1774+ coefficient: 1 ,
1775+ column: cols:: JALR ,
1776+ } ,
1777+ LinearTerm :: Column {
1778+ coefficient: 1 ,
1779+ column: cols:: BEQ ,
1780+ } ,
1781+ LinearTerm :: Column {
1782+ coefficient: 1 ,
1783+ column: cols:: BLT ,
1784+ } ,
1785+ LinearTerm :: Column {
1786+ coefficient: 1 ,
1787+ column: cols:: LOAD ,
1788+ } ,
1789+ LinearTerm :: Column {
1790+ coefficient: 1 ,
1791+ column: cols:: STORE ,
1792+ } ,
1793+ LinearTerm :: Column {
1794+ coefficient: 1 ,
1795+ column: cols:: MUL ,
1796+ } ,
1797+ LinearTerm :: Column {
1798+ coefficient: 1 ,
1799+ column: cols:: DIVREM ,
1800+ } ,
1801+ LinearTerm :: Column {
1802+ coefficient: 1 ,
1803+ column: cols:: ECALL ,
1804+ } ,
1805+ LinearTerm :: Column {
1806+ coefficient: 1 ,
1807+ column: cols:: EBREAK ,
1808+ } ,
17611809 ] ) ;
17621810
17631811 // prev_ts_lo = timestamp - 3*(1 - pc_double_read) + 2^32 * borrow
17641812 // = timestamp - 3 + 3*pc_double_read + 2^32 * borrow
17651813 let prev_ts_lo = BusValue :: linear ( vec ! [
1766- LinearTerm :: Column { coefficient: 1 , column: cols:: TIMESTAMP } ,
1814+ LinearTerm :: Column {
1815+ coefficient: 1 ,
1816+ column: cols:: TIMESTAMP ,
1817+ } ,
17671818 LinearTerm :: Constant ( -3 ) ,
1768- LinearTerm :: Column { coefficient: 3 , column: cols:: PC_DOUBLE_READ } ,
1769- LinearTerm :: Column { coefficient: 1i64 << 32 , column: cols:: PREV_PC_TIMESTAMP_BORROW } ,
1819+ LinearTerm :: Column {
1820+ coefficient: 3 ,
1821+ column: cols:: PC_DOUBLE_READ ,
1822+ } ,
1823+ LinearTerm :: Column {
1824+ coefficient: 1i64 << 32 ,
1825+ column: cols:: PREV_PC_TIMESTAMP_BORROW ,
1826+ } ,
17701827 ] ) ;
17711828
17721829 // prev_ts_hi = 0 - borrow
17731830 // The -1 cancels the +2^32 added to prev_ts_lo when borrow fires, keeping the
17741831 // 64-bit timestamp correct: (prev_ts_hi * 2^32 + prev_ts_lo) = timestamp - 3.
1775- let prev_ts_hi = BusValue :: linear ( vec ! [
1776- LinearTerm :: Column { coefficient: -1 , column: cols:: PREV_PC_TIMESTAMP_BORROW } ,
1777- ] ) ;
1832+ let prev_ts_hi = BusValue :: linear ( vec ! [ LinearTerm :: Column {
1833+ coefficient: -1 ,
1834+ column: cols:: PREV_PC_TIMESTAMP_BORROW ,
1835+ } ] ) ;
17781836
17791837 for i in 0 ..2u64 {
17801838 // PC read (sender, +1): consume old token
@@ -1805,12 +1863,19 @@ pub fn bus_interactions() -> Vec<BusInteraction> {
18051863 BusValue :: constant( 510 + i) ,
18061864 BusValue :: constant( 0 ) ,
18071865 BusValue :: linear( vec![
1808- LinearTerm :: Column { coefficient: 1 , column: cols:: TIMESTAMP } ,
1866+ LinearTerm :: Column {
1867+ coefficient: 1 ,
1868+ column: cols:: TIMESTAMP ,
1869+ } ,
18091870 LinearTerm :: Constant ( 1 ) ,
18101871 ] ) ,
18111872 BusValue :: constant( 0 ) ,
18121873 BusValue :: Packed {
1813- start_column: if i == 0 { cols:: NEXT_PC_0 } else { cols:: NEXT_PC_1 } ,
1874+ start_column: if i == 0 {
1875+ cols:: NEXT_PC_0
1876+ } else {
1877+ cols:: NEXT_PC_1
1878+ } ,
18141879 packing: Packing :: Direct ,
18151880 } ,
18161881 ] ,
0 commit comments