Bex is awesome. perfect for symbolic machinery. https://vxtwitter.com/starbaser/status/2096415026521497678

Whoa, did you add function decorators into BAML?

@Vaibhav (BAML 🐑) the people yearn for attribute syntax

kinda... it's a big project! compile-based symbolic execution, a la concolic testing. via an MIR extension interface. i was almost done writing a text with full details and my phone died i have to sit down to give a proper response when i get home https://cdn.discordapp.com/attachments/1545996959633113088/1546992177916154028/HRpM5McaQAAuEif.jpg?ex=6aa1cc3c&is=6aa07abc&hm=2d446583a7bbc3e9d707d4279b796b21f5502a1814de2ddd12cf6c1969ac3a5b&

This is... a lot to wrap my head around, wow So the symbolic execution target is a bag of tensors? Presumably you're bridging pytorch via the python bridge ...but where do the MIR extensions fit into this?

The MIR extension is for practicality. Before losing the draft, my message described it as a compiler protocol, but thats more toward how its leveraged than what it is, it's essentially an API over the MIR to minimize the surface area that I have to implement against. It's to avoid a hard fork as well as a crucial correctness buffer between us. Effectively I lower the MIR to other representations alongside the "authenticated" BEX bytecode include "custom" BEX bytecode for operating the symbolic machinery. also packing. it also kinda comes from there... but i will write more as I can!

Hm, OK, I think I'm making more sense of this now: - the use case is to implement symbolic execution of models, i.e. bags of tensors - your symbolic execution program is implemented with BAML syntax + BAML syntax extensions (this is where your

@@ingot

comes in?) - you also have a symbolic execution compiler stage that is implemented by consuming the MIR - and then you have custom bytecode extensions, and your own symbolic execution VM Is that right?

yes more or less but im so sorry to keep you guessing. i am trying to improve my social media maxxing but a vague post is not a good professional medium to reason over I typically have mid-work week bandwidth but this week but it's not a gaurentee 🤧 I'll sit down when I next can but im still happy to entertain questions until then The

@ingot

/

@@ingot

annotation layer is just source preprocessing that harvests annotation data for code generation and runtime use, where it's exposed through

_meta.ingot

. It's intentionally general purpose, I use it for MCP annotations, CLI help/usage, and other external integrations. I avoid syntax extensions wherever possible, and no custom bytecode extension is needed for this approach. My earlier “custom bytecode” wording muddied that, sorry. [§4.1 of the SymCC paper](https://www.s3.eurecom.fr/docs/usenixsec20_symcc.pdf) is relevant here: the compiler prepares instrumentation, but the symbolic computations happen when the program executes. The program still executes concretely; alongside that, the instrumentation builds symbolic expressions and records the conditions that led down the actual path. That's the principle I'm borrowing, rather than SymCC's execution target. SymCC instruments LLVM IR and ultimately produces native code; here, BEX remains the concrete executor. The compiler prepares symbolic transfer information tied to the BEX instructions it emits, and an opt-in extension tracks the corresponding symbolic state during execution. So I do make compiler/runtime changes, but not a separate replacement VM or a new symbolic language constructs. This is also where the MIR interface helps. I want a small, compiler-owned interface to the resolved program and its semantics, rather than independently reconstructing those facts. I must avoid depending on the internal MIR detail, or else I lose that shared boundary to implement the symbolic machinery and other consumers like packing against. And one correction to the first point: the target is general concolic execution of BAML programs, not specifically bags of tensors Training is an application of it. BAML can describe data preparation, packing, model composition and control, while bindings call ordinary PyTorch through Python and still owns tensor operations and autograd. So: ordinary BAML is the program being analyzed, the compiler prepares the symbolic tracking, and BEX executes it with that tracking enabled when requested.