From af2b13214579d78827392e762149fa8824526aa9 Mon Sep 17 00:00:00 2001 From: ericmarin Date: Tue, 10 Mar 2026 16:29:33 +0100 Subject: added MLP --- rules.in | 71 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 71 insertions(+) create mode 100644 rules.in (limited to 'rules.in') diff --git a/rules.in b/rules.in new file mode 100644 index 0000000..2ff92dd --- /dev/null +++ b/rules.in @@ -0,0 +1,71 @@ +// Agents +// Built-in +// Eraser: delete other agents recursively +// Dup: duplicates other agents recursively + +// Implemented +// Linear(x, int q, int r): represent "q*x + r" +// Concrete(int k): represent a concrete value k +// Symbolic(id): represent the variable id +// Add(out, b): represent the addition (has various steps AddCheckLinear/AddCheckConcrete) +// Mul(out, b): represent the multiplication (has various steps MulCheckLinear/MulCheckConcrete) +// ReLU(out): represent "if x > 0 ? x ; 0" +// Materialize(out): transforms a Linear packet into a final representation of TermAdd/TermMul/TermReLU + +// TODO: add range information to enable ReLU elimination + +// Rules +Linear(x, int q, int r) >< Add(out, b) => b ~ AddCheckLinear(out, x, q, r); + +Concrete(int k) >< Add(out, b) + | k == 0 => out ~ b + | _ => b ~ AddCheckConcrete(out, k); + +Linear(y, int s, int t) >< AddCheckLinear(out, x, int q, int r) + | (q == 0) && (r == 0) && (s == 0) && (t == 0) => out ~ Concrete(0), x ~ Eraser, y ~ Eraser + | (s == 0) && (t == 0) => Linear(x, q, r) ~ Materialize(out), y ~ Eraser + | (q == 0) && (r == 0) => (*L)Linear(y, s, t) ~ Materialize(out), x ~ Eraser + | _ => Linear(x, q, r) ~ Materialize(out_x), (*L)Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermAdd(out_x, out_y), 1, 0); + +Concrete(int j) >< AddCheckLinear(out, x, int q, int r) => out ~ Linear(x, q, r + j); + +Linear(y, int s, int t) >< AddCheckConcrete(out, int k) => out ~ Linear(y, s, t + k); + +Concrete(int j) >< AddCheckConcrete(out, int k) + | j == 0 => out ~ Concrete(k) + | _ => out ~ Concrete(k + j); + +Linear(x, int q, int r) >< Mul(out, b) => b ~ MulCheckLinear(out, x, q, r); + +Concrete(int k) >< Mul(out, b) + | k == 0 => b ~ Eraser, out ~ (*L)Concrete(0) + | k == 1 => out ~ b + | _ => b ~ MulCheckConcrete(out, k); + +Linear(y, int s, int t) >< MulCheckLinear(out, x, int q, int r) + | (q == 0) && (r == 0) && (s == 0) && (t == 0) => out ~ Concrete(0), x ~ Eraser, y ~ Eraser + | (s == 0) && (t == 0) => Linear(x, q, r) ~ Materialize(out), y ~ Eraser + | (q == 0) && (r == 0) => (*L)Linear(y, s, t) ~ Materialize(out), x ~ Eraser + | _ => Linear(x, q, r) ~ Materialize(out_x), (*L)Linear(y, s, t) ~ Materialize(out_y), out ~ Linear(TermMul(out_x, out_y), 1, 0); + +Concrete(int j) >< MulCheckLinear(out, x, int q, int r) => out ~ Linear(x, q * j, r * j); + +Linear(y, int s, int t) >< MulCheckConcrete(out, int k) => out ~ Linear(y, s * k, t * k); + +Concrete(int j) >< MulCheckConcrete(out, int k) + | j == 0 => out ~ Concrete(0) + | j == 1 => out ~ Concrete(k) + | _ => out ~ Concrete(k * j); + +Linear(x, int q, int r) >< ReLU(out) => (*L)Linear(x, q, r) ~ Materialize(out_x), out ~ Linear(TermReLU(out_x), 1, 0); + +Concrete(int k) >< ReLU(out) + | k > 0 => out ~ (*L)Concrete(k) + | _ => out ~ Concrete(0); + +Linear(x, int q, int r) >< Materialize(out) + | (q == 0) => out ~ Concrete(r), x ~ Eraser + | (q == 1) && (r == 0) => out ~ x + | (q == 1) && (r != 0) => out ~ TermAdd(x, Concrete(r)) + | (q != 0) && (r == 0) => out ~ TermMul(Concrete(q), x) + | _ => out ~ TermAdd(TermMul(Concrete(q), x), Concrete(r)); -- cgit v1.2.3