Skip to content

Lean audit: the fifty translation defects it refuted - #22

Merged
chenyueqi merged 1 commit into
mainfrom
sync/lean-audit
Sep 30, 2026
Merged

chenyueqi merged 1 commit into
mainfrom
sync/lean-audit

Conversation

@chenyueqi

@chenyueqi chenyueqi commented Sep 30, 2026 •

Copy link
Copy Markdown
Member

Carries the Lean-audit fixes: fifty refuted translation defects in the NumPy translator and the Fortran analysis (FNP-D0001–D0050) with their regression tests. Four of the review tests need translators an installation may lack and are not carried.

🤖 Generated with Claude Code

@chenyueqi chenyueqi changed the title Lean audit: the translation defects it refuted, and the JAX backend brought to their values Lean audit: the fifty translation defects it refuted Sep 30, 2026
- Evaluate a FORALL's values before storing any, and honour its mask
- Write through an ASSOCIATE name to the scalar variable it selects
- Fit a CHARACTER assignment to the variable's declared length
- Keep a SAVEd local the body changes from one call to the next
- Infer intent(out) only for a dummy every path stores, and for any data type
- Round ANINT halves away from zero instead of to even
- Convert INT and NINT into the INTEGER kind the source asks for
- Report LBOUND and UBOUND as the bounds the subscripts are shifted by
- Answer KIND, HUGE, TINY, EPSILON and PRECISION from the declared kind
- Spell DIGITS and the model inquiries, and refuse an intrinsic with no rule
- Hand the bit intrinsics their operands' declared width
- Keep INTEGER ** a negative exponent an integer
- Divide integer arrays, and map scalar-only intrinsics, elementwise
- Start DOT_PRODUCT's accumulator at the operands' own zero
- Spell an implied edge of a stepped section as the bound it stands for
- Keep an empty section's stop edge from counting from the end
- Translate RESHAPE with PAD, ORDER, and a source larger than the shape
- Pack in array element order, and give PACK its VECTOR
- Fill EOSHIFT's vacated end with its BOUNDARY
- Locate MAXLOC/MINLOC under their MASK, first in array element order
- Copy a mismatched OUT array back in storage order
- Hand an assumed-size dummy the whole storage tail, partial column and all
- Truncate a use-imported constant's integer quotient toward zero
- Keep INTEGER / and ** inside a constant expression integer arithmetic
- Spell NINT, MOD and SIGN in a constant expression as Fortran defines them
- Ask HUGE and DIGITS of an integer literal about the INTEGER kind
- Divide a module variable's integer initializer as integers
- Start a derived type's components at their default initialization
- Divide HUGE of an integer and an integer(8) quotient exactly in constants
- Convert a default or saved initializer to the type it initializes
- Read an INTEGER's kind from its spelling, not from the int32 it was typed
- Keep a default-kind NINT's low 32 bits of the 64-bit lround, as gfortran does
- Keep FLOOR's and CEILING's KIND over an array
- Map an intrinsic over a zero-size array, and keep a mapped bit result's width
- Hand an IN or INOUT dummy the leading storage of a larger whole array
- Pass over a NaN when MAXLOC and MINLOC look for the extremum
- Clamp a section's stop edge at a bound variable the body can redefine
- Count an array constructor's scalars as RESHAPE's literal source size
- Hand a kernel that calls a helper the Numba runtime lacks to the NumPy module
- Stop a FORALL counting down one past its last index, not one short
- Copy a FORALL's gathered sections before storing any
- Keep a FORALL's index to its construct
- Count a store through an ASSOCIATE name, a WRITE or a function as a store
- Read a DO loop that can CYCLE or EXIT as writing only part of an array
- Fit a CHARACTER store to its length on the CALL, component, module and array paths
- Keep an un-INTENTed assumed-length CHARACTER dummy intent(inout)
- Type the stop-edge, kind and constant helpers the review fixes added
- Read a callee's extent expression in the caller's names
- Allocate a zero-sized axis where the upper bound is below the lower one
- Hold an array's lower bound from where the array came into being
- Allocate an automatic array of zero size where its bounds cross
- Regenerate the corpus baseline and the CI summaries for the audit fixes

Signed-off-by: Qinrun Dai <mouseisnotalwaysmouse@outlook.com>

Carried-From: 35a8819089579f46f8156017d856b444ed8946f9
@chenyueqi
chenyueqi merged commit 93347bf into main Sep 30, 2026
13 checks passed
@chenyueqi
chenyueqi deleted the sync/lean-audit branch September 30, 2026 03:56
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants