ChanServ changed the topic of ##yamahasynths to: Channel dedicated to questions and discussion of Yamaha FM Synthesizer internals and corresponding REing. Discussion of synthesis methods similar to the Yamaha line of chips, Sound Blasters + clones, PCM chips like RF5C68, and CD theory of operation are also on-topic. Channel logs: https://freenode.irclog.whitequark.org/~h~yamahasynths
ej5 has joined ##yamahasynths
Lord_Nightmare has quit [Read error: Connection reset by peer]
andlabs has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
cr1901_modern1 has joined ##yamahasynths
cr1901_modern has quit [Ping timeout: 240 seconds]
cr1901_modern has joined ##yamahasynths
cr1901_modern1 has quit [Ping timeout: 240 seconds]
andlabs has joined ##yamahasynths
andlabs has quit [Client Quit]
<cr1901_modern>
whitequark: Is your plan to create an SMT2/Z3 model of 8051 to do program synthesis since Rosette hardcodes too many assumptions?
andlabs has joined ##yamahasynths
<whitequark>
um
<whitequark>
it doesn't hardcode any
<whitequark>
Rosette is a library that lifts Racket constructs to SMT constructs
<whitequark>
it has zero CPU-specific knowledge. in fact it's about as general purpose as it gets
<whitequark>
a bit *too* general purpose for my taste, but definitely usable
<cr1901_modern>
Anyways it appears you continued the thread since that tweet and so I retract my q
<whitequark>
no, it's more like
<whitequark>
you know how C compilers assume UB never happens?
* cr1901_modern
nods
<whitequark>
when you use Rosette, each time you trigger an error--ANY error--it assumes that code path never happens
<whitequark>
silently and there is no way to make it non-silent
<whitequark>
this includes errors that are dependent on the lifting process itself, so you can't even easily reproduce them in REPL (vs running the synthesizer)
<whitequark>
this sort of makes sense conceptually, but in practice it means that you have to know every single error the primitives you use might trigger or your code will randomly fail to give you results without any indication
<cr1901_modern>
Ouch ._. (especially "this includes errors that are dependent on the lifting process itself")
<cr1901_modern>
I'm reading over the GH issue #137 for their reasoning. Anyways, I don't have any program synthesis needs right now, but I see myself using rosette for some retro bullshit in the future.
<cr1901_modern>
Might be funny to apply ej5's natural language spec of the DSP firmware to rosette and see what it spits out too :P
<whitequark>
the reasoning is the same as with UB
<whitequark>
you don't know if the error is because i wrote a bug, or because the synthesizer got itself into a corner
<whitequark>
there's no difference between these cases that something like rosette can determine
<whitequark>
you'd need to either add types (typed rosette is a thing but it's "experimental" and rosette is plenty experimental enough for my taste), or ditch lifting (i assume there are other approaches too but idk which)
<cr1901_modern>
Rosette is like a Library of Babel for assembly snippets
<andlabs>
my copies of the 101 and 102 cartridges+manuals for the CX-5M came
<andlabs>
this is gonna be fun when the machine itself comes
cr1901_modern has quit [Read error: Connection reset by peer]
<TD-Linux>
never used a SMT solver for that task, but a previous project used a superoptimizer to get an optimal x86 divide by 3 with certain rounding constraints
_whitelogger has joined ##yamahasynths
<andlabs>
shin megami tensei solver
<kode54>
andlabs: thanks, I was thinking that as I read it