MLIR passage 1: LLVM poison-flagged zero counts

{"entries":[{"file_sha256":"bfc1e646e91fe0ba6d7d16e43994100b05c3b8ff79c2e07288e8955c43d9d79d","kind":"documentation_input","lines":"254-258","path":"docs/spec-compiler-part-2-scf.md","roles":["applicability","context","input_construction"],"text":"LLVM leading- and trailing-zero count intrinsics with\n`is_zero_poison = false` normalize mechanically to `math.ctlz` and\n`math.cttz`. The poison-flagged forms retain their LLVM spelling and project\nthat flag through the registered typed semantic case; the standard Math ops\ncannot carry the poison-on-zero contract.","why":"Governing context and sampled obligation: zero-count intrinsics with is_zero_poison = false normalize to math.ctlz/math.cttz, while the poison-flagged forms retain their LLVM spelling. Selects both the applicable inputs (llvm.intr.ctlz/cttz with either flag value) and the terminology of the output condition."},{"file_sha256":"bfc1e646e91fe0ba6d7d16e43994100b05c3b8ff79c2e07288e8955c43d9d79d","kind":"documentation_input","lines":"141-146","path":"docs/spec-compiler-part-2-scf.md","roles":["input_construction","input_well_formedness"],"text":"Mechanical raising uses the standard `arith` or `math` operation schema when\nit exactly represents an LLVM computation under the complete operation type,\noperation attributes, overflow and exact flags, fast-math policy, rounding\nmode, enclosing function floating-point environment, and DataLayout. An\napparent LLVM alias does not normalize merely because it has a familiar\nopcode. Exact normalization gives Canonical Dataflow one operation-schema","why":"Linked input passage: a standard arith/math spelling applies only under the complete operation type, attributes, and flags, so sampled operand/result types and the intrinsic's attribute must be exact and complete."},{"file_sha256":"bfc1e646e91fe0ba6d7d16e43994100b05c3b8ff79c2e07288e8955c43d9d79d","kind":"documentation_input","lines":"150-154","path":"docs/spec-compiler-part-2-scf.md","roles":["input_construction"],"text":"An LLVM-dialect compute intrinsic may remain only when no exact standard MLIR\noperation represents it and it later satisfies the canonical actor contract.\nTarget-specific intrinsics should be normalized to target-neutral scalar or\nvector operations when such a representation exists. Otherwise, preserving\nthe registered LLVM operation is preferable to weakening its semantics.","why":"Linked input passage: registered LLVM operations are preserved rather than weakened when no exact standard operation exists; motivates sampling the poison-flagged intrinsic form."},{"file_sha256":"bfc1e646e91fe0ba6d7d16e43994100b05c3b8ff79c2e07288e8955c43d9d79d","kind":"documentation_input","lines":"166-173","path":"docs/spec-compiler-part-2-scf.md","roles":["input_construction","input_well_formedness"],"text":"The LLVM dialect `passthrough` function attribute is an importer-owned lossless\ncontainer, not a floating-point-environment authority. Mechanical raising uses\none closed classifier owned by the exact-spelling projection. Typed LLVM\nfloating environment attributes, `strictfp`, incompatible exception policy,\nand unknown string attributes block standard spelling. LLVM enum function\nattributes and explicitly classified code-generation-only strings do not.\nClang's default `no-trapping-math=true` is compatible with the ordinary\nnon-constrained floating operation spelling; any other value fails closed.","why":"Linked input passage on the passthrough function-attribute classifier; drives sampling of enclosing llvm.func passthrough attributes (nounwind, strictfp, no-trapping-math=true, target-cpu) on the generated callables."},{"file_sha256":"bfc1e646e91fe0ba6d7d16e43994100b05c3b8ff79c2e07288e8955c43d9d79d","kind":"documentation_input","lines":"177-178","path":"docs/spec-compiler-part-2-scf.md","roles":["context"],"text":"FMA normalization is semantic rather than name based. An exact fused LLVM FMA\nbecomes `math.fma`. `llvm.intr.fmuladd` remains unchanged in S0 until one typed","why":"Linked input passage on semantic (non-name-based) normalization; establishes that spelling retention is decided by stated semantics, not opcode names."},{"file_sha256":"bfc1e646e91fe0ba6d7d16e43994100b05c3b8ff79c2e07288e8955c43d9d79d","kind":"documentation_input","lines":"266-268","path":"docs/spec-compiler-part-2-scf.md","roles":["input_well_formedness"],"text":"Fixed vectors may carry exceptional state per lane. A normalization is legal\nonly when it preserves the operation-specific rules for propagation,\nnon-observation, and undefined behavior.","why":"Linked input passage: a normalization is legal only when it preserves propagation, non-observation, and undefined-behavior rules; this is why a poison-on-zero input must stay well-formed as the registered LLVM operation."},{"file_sha256":"af4923a40d1fab8c6bbfe8bd954175a6ecefd8e6a9a3fc1e1d1f7a7221660da5","kind":"verifier","lines":"238-252","path":"lib/Frontend/Raising/LLVMArithToArithPass.cpp","roles":["applicability"],"text":"// The math zero-count operations define zero to return the operand width.\n// That is exactly the non-poisoning LLVM form. The poisoning form retains its\n// LLVM spelling because math has no attribute that can carry that contract.\ntemplate <typename LLVMOp, typename MathOp>\nstruct CountZerosAlias : public ::mlir::OpRewritePattern<LLVMOp> {\n  using ::mlir::OpRewritePattern<LLVMOp>::OpRewritePattern;\n\n  ::mlir::LogicalResult\n  matchAndRewrite(LLVMOp op, ::mlir::PatternRewriter &rewriter) const override {\n    if (op.getIsZeroPoison() || !restatesExactly(op, /*floating=*/false))\n      return ::mlir::failure();\n    rewriter.replaceOpWithNewOp<MathOp>(op, op.getRes().getType(), op.getIn());\n    return ::mlir::success();\n  }\n};","why":"CountZerosAlias acceptance implementation: the rewrite bails out when getIsZeroPoison() holds, confirming which sampled inputs fall under the retained-spelling case and which are rewritten."},{"file_sha256":"af4923a40d1fab8c6bbfe8bd954175a6ecefd8e6a9a3fc1e1d1f7a7221660da5","kind":"implementation","lines":"568-573","path":"lib/Frontend/Raising/LLVMArithToArithPass.cpp","roles":["applicability"],"text":"// zero-count aliases whose zero behavior is fully defined\n        CountZerosAlias<::mlir::LLVM::CountLeadingZerosOp,\n                        ::mlir::math::CountLeadingZerosOp>,\n        CountZerosAlias<::mlir::LLVM::CountTrailingZerosOp,\n                        ::mlir::math::CountTrailingZerosOp>,","why":"Pattern registration binding LLVM::CountLeadingZerosOp/CountTrailingZerosOp to the math counterparts, establishing that this stage is the owner of the sampled obligation."},{"file_sha256":"af4923a40d1fab8c6bbfe8bd954175a6ecefd8e6a9a3fc1e1d1f7a7221660da5","kind":"implementation","lines":"480-492","path":"lib/Frontend/Raising/LLVMArithToArithPass.cpp","roles":["applicability","input_construction"],"text":"struct LLVMArithToArithPass\n    : public ::mlir::PassWrapper<LLVMArithToArithPass,\n                                 ::mlir::OperationPass<>> {\n  MLIR_DEFINE_EXPLICIT_INTERNAL_INLINE_TYPE_ID(LLVMArithToArithPass)\n\n  ::llvm::StringRef getArgument() const final {\n    return \"loom-llvm-arith-to-arith\";\n  }\n  ::llvm::StringRef getDescription() const final {\n    return \"Rewrite each llvm computation whose complete semantics an arith \"\n           \"or math operation restates exactly into that standard operation, \"\n           \"scoped to callable regions.\";\n  }","why":"Pass declaration giving the --loom-llvm-arith-to-arith argument and its callable-region scoping, which is why generated intrinsics are placed inside llvm.func bodies."},{"file_sha256":"fc8794a0235430f2ab7b87b0fb63e4991acfa052ab630501b484fce956154a56","kind":"verifier","lines":"26-52","path":"lib/Frontend/Raising/ExactStandardSpelling.h","roles":["input_well_formedness","input_construction"],"text":"// True when `type` has an exact standard counterpart: a signless integer of\n// non-zero width, `index`, a float, or a fixed-shape vector of those.\n//\n// arith rejects zero-width and signed integers. A scalable vector's element\n// count is a runtime `vscale` multiple rather than a shape, so it fails closed\n// here and keeps its operations in llvm form: only once a typed structured\n// transform has materialized the computation as fixed-width chunks, loops, and\n// masks or tails do the resulting operations hold a fixed shape that these\n// aliases accept.\ninline bool isExactNumericType(::mlir::Type type) {\n  if (auto vectorType = ::mlir::dyn_cast<::mlir::VectorType>(type)) {\n    if (vectorType.isScalable())\n      return false;\n    type = vectorType.getElementType();\n  }\n  if (auto integerType = ::mlir::dyn_cast<::mlir::IntegerType>(type))\n    return integerType.isSignless() && integerType.getWidth() > 0;\n  return ::mlir::isa<::mlir::IndexType, ::mlir::FloatType>(type);\n}\n\ninline bool allExactNumericTypes(::mlir::ValueRange values) {\n  for (::mlir::Value value : values) {\n    if (!isExactNumericType(value.getType()))\n      return false;\n  }\n  return true;\n}","why":"isExactNumericType defines the exact standard counterpart types (signless non-zero-width integers, index, float, fixed-shape vectors); the grammar samples only such types so type exactness never masks the poison-flag behavior."},{"file_sha256":"fc8794a0235430f2ab7b87b0fb63e4991acfa052ab630501b484fce956154a56","kind":"verifier","lines":"142-161","path":"lib/Frontend/Raising/ExactStandardSpelling.h","roles":["input_well_formedness"],"text":"// True when the enclosing callable states a floating-point environment the\n// standard operation cannot restate.\ninline bool enclosingFloatingPolicyBlocksRewrite(::mlir::Operation *op) {\n  auto funcOp = ::mlir::dyn_cast_or_null<::mlir::LLVM::LLVMFuncOp>(\n      getNearestCallableOp(op));\n  return funcOp && statesFloatingPolicy(funcOp);\n}\n\n// True when every operand and the single result of `op` have an exact standard\n// counterpart and, for a computation that reads or produces a floating value,\n// the enclosing callable states no environment the standard operation cannot\n// restate. An integer computation is independent of that environment and is\n// never blocked by it.\ninline bool restatesExactly(::mlir::Operation *op, bool floating) {\n  if (!allExactNumericTypes(op->getOperands()))\n    return false;\n  if (!isExactNumericType(op->getResult(0).getType()))\n    return false;\n  return !floating || !enclosingFloatingPolicyBlocksRewrite(op);\n}","why":"restatesExactly states that an integer computation is never blocked by the enclosing floating-point environment, so sampled passthrough attributes do not confound the poison-flag case."},{"file_sha256":"fc8794a0235430f2ab7b87b0fb63e4991acfa052ab630501b484fce956154a56","kind":"verifier","lines":"74-140","path":"lib/Frontend/Raising/ExactStandardSpelling.h","roles":["input_construction"],"text":"inline bool passthroughEntryStatesFloatingPolicy(::mlir::Attribute entry) {\n  ::llvm::StringRef name;\n  ::std::optional<::llvm::StringRef> value;\n  if (auto nameAttr = ::mlir::dyn_cast<::mlir::StringAttr>(entry)) {\n    name = nameAttr.getValue();\n  } else if (auto pair = ::mlir::dyn_cast<::mlir::ArrayAttr>(entry);\n             pair && pair.size() == 2) {\n    auto nameAttr = ::mlir::dyn_cast<::mlir::StringAttr>(pair[0]);\n    auto valueAttr = ::mlir::dyn_cast<::mlir::StringAttr>(pair[1]);\n    if (!nameAttr || !valueAttr)\n      return true;\n    name = nameAttr.getValue();\n    value = valueAttr.getValue();\n  } else {\n    return true;\n  }\n\n  // The LLVM importer places every function attribute that LLVMFuncOp does\n  // not model explicitly in one passthrough array. LLVM enum attributes still\n  // retain their stable native spelling there. Of those function attributes,\n  // strictfp alone changes the floating execution environment; the others\n  // describe effects, control, ABI, or code generation without changing the\n  // meaning of an ordinary floating instruction.\n  const ::llvm::Attribute::AttrKind kind =\n      ::llvm::Attribute::getAttrKindFromName(name);\n  if (kind != ::llvm::Attribute::None)\n    return kind == ::llvm::Attribute::StrictFP;\n\n  // These string attributes are emitted by ordinary Clang compilation but\n  // are not all modeled as typed LLVMFuncOp fields by the pinned importer.\n  // Keep this list closed: an unknown string attribute may carry target\n  // floating semantics and therefore fails closed.\n  const bool codegenOnly = ::llvm::StringSwitch<bool>(name)\n                               .Cases({\"min-legal-vector-width\",\n                                       \"stack-protector-buffer-size\",\n                                       \"target-cpu\"},\n                                      true)\n                               .Default(false);\n  if (codegenOnly)\n    return false;\n\n  // Clang's default -ffp-exception-behavior=ignore spelling. A false or\n  // malformed value cannot be represented by an unconstrained arith/math op.\n  if (name == \"no-trapping-math\")\n    return !value || *value != \"true\";\n\n  return true;\n}\n\ninline bool statesFloatingPolicy(::mlir::LLVM::LLVMFuncOp funcOp) {\n  if (auto env = funcOp.getDenormalFpenvAttr())\n    if (!statesDefaultDenormalEnvironment(env))\n      return true;\n  if (auto noSignedZeros = funcOp.getNoSignedZerosFpMathAttr())\n    if (noSignedZeros.getValue())\n      return true;\n  if (auto contraction = funcOp.getFpContractAttr())\n    if (contraction.getValue() != \"off\")\n      return true;\n  if (funcOp.getReciprocalEstimatesAttr())\n    return true;\n  if (auto passthrough = funcOp.getPassthroughAttr())\n    for (::mlir::Attribute entry : passthrough)\n      if (passthroughEntryStatesFloatingPolicy(entry))\n        return true;\n  return false;\n}","why":"Closed passthrough/floating-policy classifier; fixes the concrete accepted spellings of the function attributes the grammar samples on the enclosing llvm.func."},{"file_sha256":"cccfb541a40fcf45a23917c929f75862b06c996af3a8e06caa4533d971720279","kind":"test","lines":"1-13,376-388","path":"test/raise/llvm-arith-to-arith.mlir","roles":["input_construction","input_well_formedness"],"text":"// RUN: loom-raise-opt --loom-llvm-arith-to-arith %s | FileCheck %s\n\n// Verify that each LLVM computation whose complete semantics an arith or math\n// operation restates exactly is rewritten into that standard operation, and\n// that every source fact the standard operation cannot carry keeps its\n// operation in llvm form. Pointer-typed ops (gep/load/store/alloca) stay in\n// the llvm dialect on purpose.\n//\n// The pass rewrites every callable region in place, so an imported llvm.func\n// is normalized where it stands and stays the sole owner of its ABI envelope.\n// A case whose values are only observable as several results states its\n// container as a func.func, which anchors the same rewrite on the other\n// callable kind.\n\n// CHECK-LABEL: llvm.func @zero_count_aliases\nllvm.func @zero_count_aliases(%value: i32) -> i32 {\n    // CHECK: %[[CTLZ:.*]] = math.ctlz %arg0 : i32\n    %ctlz = \"llvm.intr.ctlz\"(%value) <{is_zero_poison = false}> : (i32) -> i32\n    // CHECK: %[[CTTZ:.*]] = math.cttz %arg0 : i32\n    %cttz = \"llvm.intr.cttz\"(%value) <{is_zero_poison = false}> : (i32) -> i32\n    // CHECK: %[[CTLZ_POISON:.*]] = \"llvm.intr.ctlz\"(%arg0) <{is_zero_poison = true}> : (i32) -> i32\n    %ctlz_poison = \"llvm.intr.ctlz\"(%value) <{is_zero_poison = true}> : (i32) -> i32\n    // CHECK: %[[CTTZ_POISON:.*]] = \"llvm.intr.cttz\"(%arg0) <{is_zero_poison = true}> : (i32) -> i32\n    %cttz_poison = \"llvm.intr.cttz\"(%value) <{is_zero_poison = true}> : (i32) -> i32\n    llvm.return %ctlz : i32\n}","why":"Accepted concrete input spelling for the zero-count intrinsics (generic form with the is_zero_poison property inside an llvm.func) and the pass invocation used for this stage; non-normative evidence of syntax only."}],"primary_bundle_sha256":"4748aa2894227784ac5cec7ed36d55b8fcde2e8fd4980afd13601f599d5f63e5","project":"PolyArch/loom","revision":"48615bc5925ef4b9db8b4550b5d4322933cf4b7b","schema":"spectriad.authoring-context/v1","selection_sha256":"31ccf46b27fcc8366d175267a6bf6c666d3e6462ef32554a9b26e325f50e4455"}

[
  {
    "api_error_status": null,
    "duration_api_ms": 31313,
    "duration_ms": 31349,
    "fast_mode_disabled_reason": "sdk_opt_in_required",
    "fast_mode_state": "off",
    "first_content_frame_ms": 1552,
    "is_error": false,
    "modelUsage": {
      "claude-opus-5": {
        "cacheCreationInputTokens": 3940,
        "cacheReadInputTokens": 0,
        "canonicalModel": "claude-opus-5",
        "contextWindow": 1000000,
        "costBasis": "list",
        "costUSD": 0.09601,
        "inputTokens": 2,
        "maxOutputTokens": 64000,
        "outputTokens": 2264,
        "provider": "firstParty",
        "thinkingTokens": 406,
        "webSearchRequests": 0
      }
    },
    "num_turns": 1,
    "permission_denials": [],
    "queued_turn_count": 0,
    "result": "## Preconditions\n\n1. Every emitted program is a single MLIR module written as `module {` \u2026 `}` containing only top-level `llvm.func` definitions and nothing else.\n2. Every function is a definition with a body (never a declaration), written as `llvm.func @NAME(%arg0: T) { \u2026 }` with exactly one block, no block label, and no explicit entry-block argument list beyond the function signature.\n3. Every function takes exactly one parameter, always named `%arg0`, and that parameter's type is a single type `T` fixed per function.\n4. Every function's signature declares no result type, and every function body ends with the terminator `llvm.return` carrying no operand, so the body is void-returning.\n5. The parameter/operand/result type `T` of a function is always an exact, statically shaped standard numeric type: either a signless integer type or a fixed-shape vector of signless integers; no scalable vectors, floats, pointers, index, opaque, or dialect-custom types occur.\n6. Within one function every operation consumes `%arg0` as its only source operand and produces a result whose type is identical to `T`, so all operand and result types inside a function coincide exactly with the function's parameter type.\n7. Zero-count operations are always spelled in generic operation form, `\"llvm.intr.ctlz\"`/`\"llvm.intr.cttz\"` applied to `(%arg0)`, and always carry the property dictionary `<{is_zero_poison = B}>` with a boolean `B`; the attribute is never omitted and never inherited by default.\n8. A zero-count operation's functional type is always written `(T) -> T`, a single operand type mapping to a single result type equal to it.\n9. Binary integer operations are always spelled in custom assembly form as `llvm.add`, `llvm.mul`, or `llvm.and` with both operands being `%arg0` and a single trailing type annotation `: T`.\n10. Every operation in a body defines a fresh SSA result named `%v` followed by its zero-based position index in that body, so result names are unique within a function and defined before the terminator.\n11. No SSA result defined in a body is ever used as an operand by any later operation or by the terminator; all defined values are dead except for their definitions.\n12. Every function body contains at least one operation before `llvm.return`, so no body consists of the terminator alone.\n13. Function bodies contain no control flow, no nested regions, no calls, no constants, no memory operations, and no operations other than the zero-count intrinsics, the three binary integer operations, and the final `llvm.return`.\n14. Function attribute dictionaries, when present, contain only importer-owned entries drawn from `passthrough` and `target_cpu`; no other function attributes (linkage, visibility, argument attributes, result attributes) are ever written.\n15. Function names are unique within the module, all sharing the prefix `@zero_counts_` followed by the function's zero-based index in the module.\n\n## Sampling conventions\n\n1. The module contains between 1 and 3 functions inclusive.\n2. Functions are named `@zero_counts_0`, `@zero_counts_1`, \u2026 using the running zero-based counter, rather than any other unique-name scheme.\n3. The per-function type `T` is drawn from exactly six choices: `i32`, `i8`, `i16`, `i64`, `vector<4xi32>`, and `vector<2xi64>`; other integer widths (e.g. `i1`, `i128`), other vector shapes, and multi-dimensional vectors are never emitted.\n4. The type is chosen once per function and reused verbatim for the parameter and for every operand/result type annotation in that function's body.\n5. Each function body contains between 1 and 4 operations, chosen independently per function.\n6. Each body operation is one of three kinds: a zero-count op with a freely chosen poison flag, a zero-count op with the flag pinned to `true`, or a binary op; the duplicated flagged alternative exists only to bias generation toward `is_zero_poison = true` and produces no syntactic form the first alternative could not.\n7. The intrinsic kind is drawn from exactly `ctlz` and `cttz`; no other LLVM intrinsics (e.g. `ctpop`, `bswap`, `abs`, `fshl`) are emitted.\n8. The `is_zero_poison` attribute value is one of the literals `true` or `false`, written as a bare boolean rather than as a typed or unit attribute.\n9. Binary operations are restricted to exactly `llvm.add`, `llvm.mul`, and `llvm.and`; no subtraction, division, shifts, comparisons, `or`/`xor`, or overflow/exact flags appear.\n10. Binary operations are never given operand flags or attributes, and always use `%arg0, %arg0` rather than distinct or previously defined operands.\n11. The function attribute clause is one of exactly four alternatives: absent, ` attributes {passthrough = [\"nounwind\"]}`, ` attributes {passthrough = [\"strictfp\"]}`, or ` attributes {passthrough = [[\"no-trapping-math\", \"true\"]], target_cpu = \"generic\"}`; these three dictionaries are fixed constants, not assembled from a larger attribute vocabulary.\n12. Result numbering restarts at `%v0` in each function, so the same SSA names recur across functions in the module.\n13. Formatting is fixed: two spaces of indentation for body operations and for `llvm.return`, one operation per line, the closing `}` of a function at column zero, and the module's closing `}` on its own final line.\n14. The module carries no name, no module-level attributes, and no data layout or target triple preamble.",
    "result_index": 0,
    "session_id": "ae5a50b6-b650-4f21-ba96-e71fbae8c2ab",
    "stop_reason": "end_turn",
    "subagent_stats": {
      "by_type": {},
      "completed": 0,
      "failed": 0,
      "killed": {
        "parent": 0,
        "system": 0,
        "user": 0
      },
      "max_depth": 0,
      "refused": {
        "budget": 0,
        "concurrency_limit": 0,
        "depth_limit": 0
      },
      "requested": {
        "background": 0,
        "foreground": 0,
        "unset": 0
      },
      "spawned": 0,
      "spawned_by_subagents": 0,
      "started_in_background": 0
    },
    "subtype": "success",
    "terminal_reason": "completed",
    "time_to_request_ms": 36,
    "total_cost_usd": 0.09601,
    "ttft_ms": 7596,
    "ttft_stream_ms": 1121,
    "type": "result",
    "usage": {
      "cache_creation": {
        "ephemeral_1h_input_tokens": 3940,
        "ephemeral_5m_input_tokens": 0
      },
      "cache_creation_input_tokens": 3940,
      "cache_read_input_tokens": 0,
      "inference_geo": "not_available",
      "input_tokens": 2,
      "iterations": [],
      "output_tokens": 2264,
      "output_tokens_details": {
        "thinking_tokens": 406
      },
      "server_tool_use": {
        "web_fetch_requests": 0,
        "web_search_requests": 0
      },
      "service_tier": "standard",
      "speed": "standard"
    },
    "uuid": "a8a4765a-0439-47a9-9302-525cb3fa9bca"
  }
]

[
  {
    "api_error_status": null,
    "duration_api_ms": 17178,
    "duration_ms": 17202,
    "fast_mode_disabled_reason": "sdk_opt_in_required",
    "fast_mode_state": "off",
    "first_content_frame_ms": 1855,
    "is_error": false,
    "modelUsage": {
      "claude-opus-5": {
        "cacheCreationInputTokens": 5737,
        "cacheReadInputTokens": 0,
        "canonicalModel": "claude-opus-5",
        "contextWindow": 1000000,
        "costBasis": "list",
        "costUSD": 0.08713,
        "inputTokens": 2,
        "maxOutputTokens": 64000,
        "outputTokens": 1190,
        "provider": "firstParty",
        "thinkingTokens": 395,
        "webSearchRequests": 0
      }
    },
    "num_turns": 1,
    "permission_denials": [],
    "queued_turn_count": 0,
    "result": "This postcondition quantifies over every operation in both programs in pre-order at any nesting depth, including the root module, using `input.operations` and `output.operations`; it never matches entities by identity, only by name, attribute presence, and count. It selects four sequences: the `llvm.intr.ctlz` operations and the `llvm.intr.cttz` operations, in each of the input and the output, that carry a key named `is_zero_poison` in their attributes/properties map whose boolean projection is true; operations with that key absent, or present but false, are excluded from the four selections. The first two assertions accept a program pair only when the output contains exactly as many true-`is_zero_poison` `llvm.intr.ctlz` operations as the input does, and likewise exactly as many true-`is_zero_poison` `llvm.intr.cttz` operations; any net increase or decrease in either count is rejected, while a deletion compensated by an unrelated addition of the same kind is accepted, since only cardinalities are compared and no operand, result, type, location, or containment correspondence is checked. The third assertion rejects any output operation named `math.ctlz` or `math.cttz` that has an `is_zero_poison` key at all, regardless of whether its value is true, false, or non-boolean; `math.ctlz`/`math.cttz` operations without that key are accepted without further constraint, and the input side is not examined by this assertion. Allowed value sources are limited to literal operation-name strings, the literal attribute key `\"is_zero_poison\"`, the total `in` membership test on the attribute map, the `.bool` projection, and `cardinality`; no helper definitions, symbol resolution, or segment decoding are used. The first two assertions are non-vacuous only when at least one side has a matching poison-flagged operation, and they pass trivially as `0 == 0` when neither program contains any; the third is vacuously satisfied whenever the output has no `math.ctlz` or `math.cttz` operations. Because the selections guard key presence with `in` before projecting, a missing `is_zero_poison` never errors, but an `is_zero_poison` attribute on an `llvm.intr.ctlz` or `llvm.intr.cttz` operation whose kind is not boolean makes `.bool` an evaluation error rather than a simple rejection. Nothing else about the two programs \u2014 other dialects, other `llvm.intr.*` operations, structure, or ordering \u2014 is constrained.",
    "result_index": 0,
    "session_id": "a7b2f31b-cf12-4793-8b33-f9bd5a1f9374",
    "stop_reason": "end_turn",
    "subagent_stats": {
      "by_type": {},
      "completed": 0,
      "failed": 0,
      "killed": {
        "parent": 0,
        "system": 0,
        "user": 0
      },
      "max_depth": 0,
      "refused": {
        "budget": 0,
        "concurrency_limit": 0,
        "depth_limit": 0
      },
      "requested": {
        "background": 0,
        "foreground": 0,
        "unset": 0
      },
      "spawned": 0,
      "spawned_by_subagents": 0,
      "started_in_background": 0
    },
    "subtype": "success",
    "terminal_reason": "completed",
    "time_to_request_ms": 24,
    "total_cost_usd": 0.08713,
    "ttft_ms": 6786,
    "ttft_stream_ms": 1567,
    "type": "result",
    "usage": {
      "cache_creation": {
        "ephemeral_1h_input_tokens": 5737,
        "ephemeral_5m_input_tokens": 0
      },
      "cache_creation_input_tokens": 5737,
      "cache_read_input_tokens": 0,
      "inference_geo": "not_available",
      "input_tokens": 2,
      "iterations": [],
      "output_tokens": 1190,
      "output_tokens_details": {
        "thinking_tokens": 395
      },
      "server_tool_use": {
        "web_fetch_requests": 0,
        "web_search_requests": 0
      },
      "service_tier": "standard",
      "speed": "standard"
    },
    "uuid": "0e923252-bf25-4243-b7b9-6331ab51db40"
  }
]