Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add method to compile geb to boolean circuits #108

Merged
merged 5 commits into from
May 3, 2023
Merged

Add method to compile geb to boolean circuits #108

merged 5 commits into from
May 3, 2023

Conversation

mariari
Copy link
Member

@mariari mariari commented Apr 28, 2023

This is just #105 rebased

@mariari mariari force-pushed the geb-bool branch 4 times, most recently from 788e481 to 5094320 Compare April 28, 2023 05:29
Copy link
Contributor

@AHartNtkn AHartNtkn left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks like the code I wrote.

@mariari
Copy link
Member Author

mariari commented Apr 28, 2023

Might be good to have a followup pr changing this to an actual CL bitvector. they have many efficient operations and can be easily done

https://novaspec.org/cl/f_bit-and

for an example of some oeprations on this. Esp if we want to add more operations

https://novaspec.org/cl/t_bit-vector

@mariari mariari force-pushed the geb-bool branch 4 times, most recently from 078071f to 3efb7d3 Compare April 28, 2023 06:14
Copy link
Contributor

@AHartNtkn AHartNtkn left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks fine

@mariari mariari force-pushed the geb-bool branch 2 times, most recently from 9f2bfb9 to ae2a70d Compare April 28, 2023 06:43
Copy link
Contributor

@AHartNtkn AHartNtkn left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Most of this is formatting and import stuff that I'm not qualified to comment on. The only substantial difference from my original code is the to-bitc refactoring. After a bit of squinting and local testing, I can see it does the same thing as the original code. It certainly looks nicer and after a bit of discussion with @mariari, we got it in a state I can approve of

@mariari
Copy link
Member Author

mariari commented Apr 28, 2023

I noticed a bug in one of the extractions

GEB-TEST> 
(bitc:to-circuit (geb:to-bitc (uncurry geb-bool:bool
                                       geb-bool:bool
                                       geb-bool:or))
                 :or)
def or x1 x2 = {
  ((1 - x1) * 1) + (x1 * x2)
};
GEB-TEST> (dom (uncurry geb-bool:bool geb-bool:bool geb-bool:or))
(× GEB-BOOL:BOOL GEB-BOOL:BOOL)
GEB-TEST>
(gapply (uncurry geb-bool:bool geb-bool:bool geb-bool:or)
        (list (left so1)
              (right so1)))
(right s-1)
GEB-TEST>
(gapply (uncurry geb-bool:bool geb-bool:bool geb-bool:or)
        (list (right so1)
              (left so1)))
(right s-1)
GEB-TEST> 
(gapply (uncurry geb-bool:bool geb-bool:bool geb-bool:or) (list (left so1)
                                                                (left so1)))
(left s-1)
GEB-TEST> (geb.main::reducer (uncurry geb-bool:bool geb-bool:bool geb-bool:or))
(∘ (case (∘ (<-left GEB-BOOL:BOOL GEB-BOOL:BOOL)
            (<-left (× GEB-BOOL:BOOL GEB-BOOL:BOOL) GEB-BOOL:FALSE))
         (∘ (<-right GEB-BOOL:BOOL GEB-BOOL:BOOL)
            (<-left (× GEB-BOOL:BOOL GEB-BOOL:BOOL) GEB-BOOL:TRUE)))
   (dist (× GEB-BOOL:BOOL GEB-BOOL:BOOL) GEB-BOOL:FALSE GEB-BOOL:TRUE)
   ((∘ (GEB-BOOL:BOOL (∘ GEB-BOOL:TRUE (->1 GEB-BOOL:BOOL)))
       (<-left GEB-BOOL:BOOL GEB-BOOL:BOOL))
    (<-right GEB-BOOL:BOOL GEB-BOOL:BOOL)))

https://pomf2.lain.la/f/1pm7rire.png

Here I have an overcomplicated or function seen by the image above.

it seems that it evaluates fine with the interpreter I have, however it seems to produce the wrong vampir circuit where if both booleans are 0 it produces . I assume something simple is wrong

Adds category of boolean circuits (BITC). The objects in this category
are just natural numbers representing the type of bit vectors of a
certain length. There are nine methods for constructing morphisms;

- (compose x y), which composes morphisms x and y.
- (ident n), which is the identity on n.
- (fork n), which maps n onto 2*n by copying its inputs.
- (parallel x y), which (if x : a -> b and y : c -> d) will be a
  morphism from a + c -> b + d, running x and y on subvectors.
- (swap n m), which maps n + m onto m + n by swapping.
- ONE, which represents the map from 0 onto 1 producing a vector with only 1 in it.
- ZERO, which represents the map from 0 onto 1 producing a vector with only 0 in it.
- (drop n), which represents the unique morphism from n to 0.
- (branch x y), which (if x : a -> b and y : a -> b) maps 1+a to b by
  splitting on the first bit to decide which morphism to apply to the
  remaining bits.

There are other ways to formulate this category, but I think this
particular formulation is quite convenient.

I've implemented a `to-bitc` function in geb.trans which translates
geb objects and morphisms into bitc objects and
morphisms. Additionally, I've implemented a `to-vampir` function in
bitc.trans which translates a bit morphism into a vampire morphism.

I'm not sure what else is needed, but the core implementation is done
for now. In the future, this should be extended to a category whose
objects represent vectors over some finite set other than the
booleans. The reason I didn't do that hear is because coproducts are
only binary and there aren't finite sets beyond so0 and so1, so
bitvectors are quite natural and using anything else would require
post-hoc optimization, but future versions of geb may want more. Also,
I'd like to know what, if any, performance benefits this gives over
the univariate polynomial formulation. I didn't test that.
mariari added 3 commits May 2, 2023 14:38
This fixes the trans loading order issues, and allows the bitc and
poly backends to share the same method name along with other parts of
the codebase being more properly abstracted
we implement gapply for <bitc>, and add tests to make sure it properly
interpretets the backend.

Further, we fix the documentation string that properly explains how
branch works
@mariari mariari force-pushed the geb-bool branch 2 times, most recently from 6d8434d to cfa57ba Compare May 2, 2023 08:32
This commit fixes a bug with init where init a domain with less than 2
bits would cause init to crash

Further we move the default compilation pipeline to use the bitc backend
@rokopt
Copy link
Member

rokopt commented May 2, 2023

This is great -- I'd favor having it merged as soon as the conflicts are resolved. Thanks!

@mariari
Copy link
Member Author

mariari commented May 2, 2023

This is great -- I'd favor having it merged as soon as the conflicts are resolved. Thanks!

conflicts get resolved on merge, the conflicts aren't real, the PR is final as is, and will be merged as is, unless we find a bug or changes are requested

;; Conversion functions
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defgeneric to-bitc (morphism)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not currently of importance, but somewhere down the line probably a good idea to include some more documentation specifying the passes this makes.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Would be good, and a documentation string on each instance as well to explain how it can be used.

I may want to open a second PR that is based on this and the lambda changes that removes the trans ordering

@mariari mariari merged commit f14792d into main May 3, 2023
@rokopt
Copy link
Member

rokopt commented May 3, 2023

it seems that it evaluates fine with the interpreter I have, however it seems to produce the wrong vampir circuit where if both booleans are 0 it produces . I assume something simple is wrong

Was this one fixed in one of the later commits?

@mariari
Copy link
Member Author

mariari commented May 3, 2023

it seems that it evaluates fine with the interpreter I have, however it seems to produce the wrong vampir circuit where if both booleans are 0 it produces . I assume something simple is wrong

Was this one fixed in one of the later commits?

This was fixed in the first commit by AHartNtkn after it was brought to his attention

@mariari mariari deleted the geb-bool branch October 11, 2023 23:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants