search

silq-lang / silq

Boost Software License 1.0
609 stars 52 forks source link

Constructing an array of parametrized length #19

Closed j6k4m8 closed 3 years ago

j6k4m8 commented 3 years ago

Excited to share what I suspect is my silly mistake with you :)

Background

I want to compute the function ;

in other words, x0 XOR (x1 AND x2 AND ... AND xn)

My approach to do this is to first construct an array of length n-1, and then use something like this function to construct the all of that array.

My challenge:

I am trying to construct an array inside a parametrized function, like so:

def x1_xor_xn[n: !β„•](input: uint[n]) {

    xn := 0:𝔹^(n-1);

    ...
}

But it doesn't seem I can construct new primitives with my parameter n even though I define it to be of classical-β„• type:

❌ vector length should be of type !β„•, not !β„€

Likewise, constructing an int array fails:

xn := 0:uint[n-1]; // ❌ expected argument types !β„•, but !β„€ was provided

And so does this silliness:

xn := 0:𝔹^((n-(1 as !β„•)) as !β„•);
// or:
xn := 0:uint[max(1, n-1) as !β„•];

It appears that 1 is interpreted as !β„€ and nothing I do can convince the compiler that I actually mean !β„•, perhaps because β„•-β„•β†’β„€...

What is the correct way to construct something like this? Is this possible in silq right now? (Is there some magical way to parametrize the n type?)

tgehr commented 3 years ago

You can use n-1 coerce !β„• or n sub 1. Both will check at runtime that the result indeed fits into !β„•. But I think what you want is just this:

def x1_xor_xn[n:!β„•](x:𝔹^n)lifted β‡’ x[0]βŠ•all(x[1..n]);
j6k4m8 commented 3 years ago

Aha!! It was that indexing notation precisely that I was looking for, too! I was trying all sorts of numpy flavored things like x[1:] etc. this is perfect, thank you!!

On Sun, Dec 20, 2020 at 8:36 PM Timon Gehr notifications@github.com wrote:

You can use n-1 coerce !β„• or n sub 1. Both will check at runtime that the result indeed fits into !β„•. But I think what you want is just this:

def x1_xor_xn[n:!β„•](x: 𝔹^n)lifted β‡’ x[0]βŠ•all(x[1..n]);

β€” You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/eth-sri/silq/issues/19#issuecomment-748710681, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAFJKBYBD56JRFZJZBPT5R3SV2RATANCNFSM4VCSYPIQ .

j6k4m8 commented 3 years ago

@tgehr I also learned about "fat-arrow" β‡’ function notation from your comment! Super helpful, thanks!