{"schema_version":1,"experiment_id":"eoa_inverse_innovation_exp04_retrieval_first_paired20_20260802","cell_id":"computability_boundary_mapping__engineering_design","hypothesis_id":"H1","search_queries":["program equivalence undecidable arbitrary imperative programs theorem primary source","firmware binary equivalence checking translation validation embedded systems research","equivalence checking compiled code bounded model checking product official documentation","DO-333 formal methods equivalence verification software certification scope unknown","patent firmware semantic equivalence checking program binaries","formal equivalence checking firmware certification workflow assurance case software substitution","translation validation CompCert executable equivalence official project","program equivalence checker returns unknown timeout product documentation"],"sources":[{"source_id":"PA-S1","title":"Well structured program equivalence is highly undecidable","publisher":"ACM Transactions on Computational Logic / arXiv","url":"https://arxiv.org/abs/1103.1433","source_class":"PRIMARY_RESEARCH","claims_supported":["Program-equivalence constructions already provide rigorous undecidability results, including for well-structured programs under specified dynamic-logic semantics.","The result's dependence on a particular equivalence definition and formal model supports requiring model matching before transferring an impossibility conclusion to firmware."]},{"source_id":"PA-S2","title":"Decidable Verification of Uninterpreted Programs","publisher":"Proceedings of the ACM on Programming Languages / arXiv","url":"https://arxiv.org/abs/1811.00192","source_class":"PRIMARY_RESEARCH","claims_supported":["Automatic verification is undecidable for the paper's general uninterpreted-program class.","A syntactically characterized coherent subclass has decidable verification in PSPACE, exemplifying the established response of narrowing an unrestricted problem to an enforceable decidable region."]},{"source_id":"PA-S3","title":"On Propositional Program Equivalence","publisher":"arXiv","url":"https://arxiv.org/abs/2507.07480","source_class":"PRIMARY_RESEARCH","claims_supported":["General program equivalence is identified as undecidable.","Abstracting statement semantics yields a decidable and practically feasible propositional-equivalence problem, demonstrating that the behavior model determines the boundary."]},{"source_id":"PA-S4","title":"Translation Validation for a Verified OS Kernel","publisher":"ACM PLDI / University of Cambridge and NICTA","url":"https://www.cl.cam.ac.uk/~mom22/pldi13.pdf","source_class":"PRIMARY_RESEARCH","claims_supported":["The seL4 work proves refinement between a specified C semantics and compiled ARM binary semantics for a concrete systems-software artifact.","Its scope is explicit: it uses a restricted intermediate language and omits assembly routines and volatile hardware accesses, closely matching the hypothesis's model-specific narrowing principle.","The work exposes proof obligations and assumptions rather than treating regression success as universal equivalence."]},{"source_id":"PA-S5","title":"The CompCert C Verified Compiler—User's Manual","publisher":"CompCert","url":"https://compcert.org/man/manual.pdf","source_class":"OFFICIAL_PRODUCT_DOCUMENTATION","claims_supported":["CompCert states a formally checked semantic-preservation theorem over defined source and target languages and an explicit notion of observable behavior.","The guarantee permits compilation refusal and is bounded by named unverified stages and language semantics, illustrating production use of scoped guarantees rather than unrestricted program-equivalence claims."]},{"source_id":"PA-S6","title":"Qualification of a Model Checker for Avionics Software Verification","publisher":"NASA Formal Methods / Springer","url":"https://homepage.cs.uiowa.edu/~tinelli/papers/WagEltAl-NFM-17.pdf","source_class":"PRIMARY_RESEARCH","claims_supported":["DO-178C, DO-330, and DO-333 practice requires confidence or qualification evidence when formal-method tools supply certification evidence.","The paper studies independent checking of proof certificates as an alternative to trusting or qualifying the entire model checker, substantially overlapping the proposed independent-review component.","It requires evidence of soundness and matching tools to problem domains, but does not prescribe a computability or reduction-direction review before funding an equivalence checker."]},{"source_id":"PA-S7","title":"Semantic Equivalence Checking of Decompiled Binaries","publisher":"Carnegie Mellon University Software Engineering Institute","url":"https://www.sei.cmu.edu/library/semantic-equivalence-checking-of-decompiled-binaries/","source_class":"PRIMARY_RESEARCH","claims_supported":["A DoD-oriented assurance pipeline already compares decompiled functions against independently lifted representations before passing them to downstream analysis.","The system reports functions as likely equivalent or unlikely equivalent rather than claiming a total exact decision procedure for arbitrary firmware."]},{"source_id":"PA-S8","title":"Detection of Semantic Equivalence of Program Source Codes (US11449317B2)","publisher":"United States Patent and Trademark Office, via Google Patents","url":"https://patents.google.com/patent/US11449317B2/en","source_class":"GOVERNMENT_OR_REGULATOR","claims_supported":["Patented prior art compares program versions through control-flow graphs, code sections, dependencies, types, and localized semantic analysis.","The patent overlaps automated equivalence assessment and changed-code localization but does not disclose an authorization-stage undecidability review or mandatory halting reduction."]}],"proximity":"ADJACENT_PRIOR_ART","closest_analogues":[{"name":"Model-specific C-to-binary translation validation for seL4 and CompCert","similarity":"These systems define source and target semantics, state observable behavior, discharge proof obligations, and publish exclusions or refusal conditions instead of promising arbitrary-program equivalence.","remaining_difference":"They establish scoped refinement or compiler semantic preservation; they do not impose a pre-funding gate requiring an independently direction-checked halting reduction whenever a project proposes unrestricted firmware equivalence.","source_ids":["PA-S4","PA-S5"]},{"name":"Avionics formal-tool qualification with independently checked proof certificates","similarity":"Certification practice already requires soundness evidence, qualification, explicit tool use, and sometimes an independent checker before formal results receive assurance credit.","remaining_difference":"The reviewed practice assesses trust in a chosen formal tool and its certificates, not whether the original universal equivalence requirement is computable or whether a source-to-target undecidability reduction is valid.","source_ids":["PA-S6"]},{"name":"Decidable-fragment responses to general verification and equivalence","similarity":"Research already maps an undecidable general class to restricted, mechanically analyzable subclasses or abstractions with narrower guarantees.","remaining_difference":"These results provide mathematical fragments and algorithms, not a firmware-substitution governance workflow that blocks funding until the universal requirement has a constructive decider or checked impossibility proof.","source_ids":["PA-S1","PA-S2","PA-S3"]},{"name":"Practical binary and source-code equivalence pipelines","similarity":"Existing research and patents compare code fragments or binaries, use independent representations, localize differences, and weaken outputs to likelihood where exact proof is unavailable.","remaining_difference":"They do not make computability classification and reduction-direction review an explicit authorization prerequisite, nor consistently require UNKNOWN rather than an unsupported Boolean result.","source_ids":["PA-S7","PA-S8"]}],"overlapping_components":["Formal behavioral-equivalence checking","Explicit source, target, and observation semantics","General undecidability recognition","Restriction to decidable or analyzable fragments","Translation validation and semantic refinement","Proof obligations and assumption disclosure","Independent proof or certificate checking","Certification-stage tool-confidence review","Partial or likelihood-based equivalence outputs","Scope exclusions, refusal, and incomplete coverage"],"remaining_contrastive_claim":"The bounded-search distinction is a mandatory authorization-stage control for unrestricted firmware-equivalence projects that requires either a model-specific constructive decider or an independently direction-checked, answer-preserving undecidability reduction, and otherwise narrows the requirement while preserving an explicit UNKNOWN outcome.","claim_falsifier":"A pre-2026 standard, certification manual, product workflow, patent, or empirical engineering study documenting that same pre-funding firmware-equivalence gate—with explicit computation model, constructive-decider-or-reduction alternatives, independent reduction-direction review, and mandatory UNKNOWN or scope narrowing—would falsify the remaining distinction; a total decider for the declared unrestricted firmware model or failure of the proposed reduction's totality, computability, or answer preservation would separately falsify its mathematical premise.","problem_support":"STRONG","recommendation":"RESEARCH","world_novelty_boundary":"No novelty is supportable for program-equivalence undecidability, halting-style reductions, decidable-fragment restriction, translation validation, scoped semantic-preservation proofs, formal-tool qualification, or independent certificate checking; the only potentially novel territory found in this eight-query bounded search is their codification as a mandatory pre-authorization governance gate specifically for unrestricted firmware-equivalence automation, and no direct evidence was found that this workflow improves funding or scoping decisions."}