github/powdr
1
1
Fork 0
mirror of https://github.com/powdr-labs/powdr.git synced 2026-04-20 03:03:25 -04:00
Code Issues Packages Projects Releases Wiki Activity

improve compiler pipeline

Browse Source
This commit is contained in:
schaeff
2023-05-24 17:24:17 +02:00
parent 936361de93
commit 3bbdd1c243
34 changed files with 823 additions and 549 deletions
Download Patch File Download Diff File Expand all files Collapse all files

38
test_data/pil/simple_sum_asm.pil
View File

@@ -1,38 +0,0 @@
namespace Main(2**10);
col witness XInv;
col witness XIsZero;
XIsZero * (1 - XIsZero) = 0;
assembly {
reg pc[@pc];
reg X[<=];
reg A;
reg CNT;
pil {
// Just to test if pil-inside-assembly-inside-pil works.
XIsZero = 1 - X * XInv;
XIsZero * X = 0;
}
instr jmpz X, l: label { pc' = XIsZero * l + (1 - XIsZero) * (pc + 1) }
instr jmp l: label { pc' = l }
instr dec_CNT { CNT' = CNT - 1 }
instr assert_zero X { XIsZero = 1 }
CNT <=X= ${ ("input", 1) };
start::
jmpz CNT, check;
A <=X= A + ${ ("input", CNT + 1) };
// Could use "CNT <=X= CNT - 1", but that would need X.
dec_CNT;
jmp start;
check::
A <=X= A - ${ ("input", 0) };
assert_zero A;
end::
jmp end;
};

42
test_data/pil/simple_sum_asm_macro.pil
View File

@@ -1,42 +0,0 @@
namespace Main(2**10);
col witness XInv;
col witness XIsZero;
XIsZero * (1 - XIsZero) = 0;
macro if_then_else(condition, true_value, false_value) { condition * true_value + (1 - condition) * false_value };
macro jump_to(target) { pc' = target; };
macro jump_to_if(condition, target) { jump_to(if_then_else(condition, target, pc + 1)); };
assembly {
reg pc[@pc];
reg X[<=];
reg A;
reg CNT;
pil {
// Just to test if pil-inside-assembly-inside-pil works.
XIsZero = 1 - X * XInv;
XIsZero * X = 0;
}
instr jmpz X, l: label { jump_to_if(XIsZero, l) }
instr jmp l: label { jump_to(l) }
instr dec_CNT { CNT' = CNT - 1 }
instr assert_zero X { XIsZero = 1 }
CNT <=X= ${ ("input", 1) };
start::
jmpz CNT, check;
A <=X= A + ${ ("input", CNT + 1) };
// Could use "CNT <=X= CNT - 1", but that would need X.
dec_CNT;
jmp start;
check::
A <=X= A - ${ ("input", 0) };
assert_zero A;
end::
jmp end;
};