Hacktoberfest 2026 : les issues que les mainteneurs ont marquées pour octobre, ouvertes et accessibles aux débutants. Parcourir les issues Hacktoberfest

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

Ouverte
  • Quelque chose ne va pas ?
#1,252 3 commentaires 0 réactions 0 personnes assignées Voir sur GitHub

Les mainteneurs répondent en général sous 1 jour

Personne n'a encore pris cette issue.

Évaluation

Difficulté
5/5
Temps estimé
Plus d'une semaine
Accessibilité débutants
30/100
Type d'issue
Fonctionnalité
Clarté
À clarifier
Activité
Active
Stack technique
csharp
Domaine
backend

Piste de recherche

Commencez par lire RewriteRule, RewriteStep, DerivationPath et le chemin des métadonnées via RuleRegistryGenerator, puis examinez MatchedRules.cs ainsi que les RuleConfluenceTest et RuleSetTerminationTest existants. La première étape consiste à déterminer si les conditions appartiennent aux règles ou sont dérivées lors des étapes de réécriture ; elle ne sera considérée comme terminée qu’une fois qu’une conception convenue aura été définie avant l’audit des 177 déclarations.

Rédigé par le modèle d'indexation à partir du texte de l'issue.

Description

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.

Langage dominant
C#
Étoiles
831
Forks
79
Merge moyen
1 h 16 min
PR mergées (30 j)
521

Préparer son environnement

Par où commencer

  1. Lisez l'issue en entier, puis le guide de contribution du projet.
  2. Signalez en commentaire que vous la prenez — cela évite que deux personnes fassent le même travail.
  3. Forkez le dépôt et travaillez sur une branche.
  4. Ouvrez une pull request qui référence le numéro de l'issue.

Autres issues de ASC-Community/AngouriMath

Toutes les issues de ASC-Community/AngouriMath

Issues similaires

Plus d'issues C#

Recevez les nouvelles issues par e-mail

Un résumé court des issues GitHub adaptées aux débutants.