Hacktoberfest 2026: los issues que los mantenedores marcaron para octubre, abiertos y aptos para principiantes. Explorar issues de Hacktoberfest

SoundUnderAssumptions names no assumption: 177 rules declare it and the condition exists only in comments

Abierto
  • ¿Algo no está bien?
#1,252 2 comentarios 0 reacciones 0 asignados Ver en GitHub

Los mantenedores suelen responder en 1 día

Nadie ha tomado este issue todavía.

Evaluación

Dificultad
5/5
Tiempo estimado
Más de una semana
Aptitud para principiantes
30/100
Tipo de issue
Nueva funcionalidad
Claridad
Necesita aclaración
Estado de actividad
Activo
Stack tecnológico
csharp
Área
backend

Línea de trabajo

Comienza leyendo RewriteRule, RewriteStep, DerivationPath y la ruta de metadatos a través de RuleRegistryGenerator; después, inspecciona MatchedRules.cs y los RuleConfluenceTest y RuleSetTerminationTest existentes. El primer paso es resolver si las condiciones pertenecen a las reglas o se derivan en los pasos de reescritura; este paso se considera completado cuando exista un diseño acordado antes de auditar las 177 declaraciones.

Escrito por el modelo de indexación a partir del texto del issue.

Descripción

Measured on 2dbeedf7: 177 rule declarations carry Soundness.SoundUnderAssumptions, against 188 that carry Soundness.Sound. Nothing records what any of those 177 assumptions are.

The tier is machine-readable. The assumption is prose. From MatchedRules.cs:

MatchPattern.Node<Divf>(MatchPattern.Any("a"), MatchPattern.Any("b")),
// a * (1/b) and a/b are undefined at exactly the same points, but the quotient
// is a quotient either way, so this inherits division's own condition rather
// than adding one. Left at the conservative tier until the audit reaches it.
Soundness.SoundUnderAssumptions,

RewriteRule exposes Soundness, Growth, GuardSource, PatternSource, ReplacementSource, SourceLine — and GuardSource is a string of source text, not a condition that can be evaluated, conjoined or checked.

Why this is the blocking piece rather than a tidiness complaint

#746's tier 5 asks for derivations "a third party can replay step by step and independently check". A step can currently be replayed but not checked: RewriteStep says which rule fired and that it was conditional, and there is no way to ask what has to hold for the answer to be right. The difference matters most exactly where it is hardest to see — a rewrite that is fine on the reals and wrong across a branch cut is SoundUnderAssumptions today, and the answer carries no trace of which reading it assumed.

That comment above is also its own evidence: it says the tier was chosen conservatively pending an audit that never happened. With 177 of them, prose cannot say which are genuinely conditional and which are unlabelled Sound, so the tier is currently a lower bound with unknown slack, and the weakest-across-a-step rule in DerivationPath propagates that slack to every answer.

What already exists to build it out of
  • DomainConditionIn(Domain) (#1090) applies a reading throughout a tree and narrows without widening — so "what must hold of the operands" is computable for a great many of these rather than needing to be authored by hand.
  • Providedf is already the node for an expression carrying a condition, and already travels through simplification.
  • Rules are data now (all 30 sets run the matcher), so a per-rule field has one place to go and RuleRegistryGenerator already reads per-rule metadata.
  • RuleConfluenceTest / RuleSetTerminationTest are precedent for checking a declaration by tooling instead of trusting the author — a declared condition can be tested numerically, by sampling points where it fails and asserting the rewrite changes the value there. A rule whose stated assumption cannot be falsified anywhere is a rule that was probably Sound all along.
Suggested shape, for discussion

Give RewriteRule an optional condition alongside Soundness — an Entity over the pattern's bound names, so the rule a/b -> a * (1/b) states b != 0 rather than describing it. Then:

  • a rule declaring SoundUnderAssumptions and no condition is a build failure once the audit is done, which is what makes the audit finish;
  • RewriteStep can expose the instantiated condition, and DerivationPath can conjoin them, so a path ends with the assumptions its answer rests on;
  • the numeric check above becomes a test, so the declaration is evidence rather than a claim.

Not proposing to land this at once — the audit is 177 rules. The first question is whether the condition belongs on the rule at all, or whether it should be derived from DomainConditionIn at the step.

Part of #746, tier 5.

Lenguaje dominante
C#
Estrellas
831
Forks
79
Merge medio
2 h 22 min
PR fusionados (30 d)
507

Preparar el entorno

Primeros pasos

  1. Lee el issue completo y luego la guía de contribución del proyecto.
  2. Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
  3. Haz un fork del repositorio y trabaja en una rama.
  4. Abre un pull request que haga referencia al número del issue.

Más de ASC-Community/AngouriMath

Todos los issues de ASC-Community/AngouriMath

Issues similares

Más issues de C#

Recibe los nuevos issues en tu correo

Un resumen breve de issues de GitHub para principiantes.