Repository navigation
feat(foreign): code in c is translated to flang and judged by kernel - #338
Merged
Merged
Conversation
ADR-0058 is accepted: a foreign language enters through an untrusted translator, and every verdict is about the translation, shown in full. The first language is a subset of C (int functions, return, if/else, int locals with an initial value, arithmetic, comparisons, logic, ?:), chosen by measurement over the ten print targets. flang/foreign/c/translator.fscript reads the text AST dump of clang, prints the translation with the duties of C (int range of every arithmetic result, a divisor that is not zero, no fall off the end), derives a draft specification marked as derived, and holds three lying translators (dropped branch, shifted constant, swapped operands). flang/foreign/c/run.fscript has two plans. Demo translates the corpus, judges the translation and the draft with the kernel, prints the translation back to C and compares it with the original C under UBSan on a grid of inputs, confirms every counterexample with flang run and fails when any function disagrees with corpus/expected.tsv or a lying translator passes. Census counts the share of the hand written C files of the tree that falls in the subset and fails when it drops. The license guard and the tree inventory treat the corpus as foreign input; tasks 2196 and 8406 record what was done. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Verified on the tree of dev plus this branch (d160ace): the checker test set passes, the provability verdict is green with all four checks, the proved-share ledger and the rule tables agree with the tree, pre-push is green, commit messages follow the convention.
🤖 Generated with Claude Code