# Open work

The [type-system roadmap](type-system-analysis.md#7-open-obligations-and-extensions) and [compiler roadmap](compiler-architecture.md#5-delivery-roadmap-and-validation) set priorities and acceptance criteria. This backlog records remaining work, not completed milestones or benchmark results. D-numbers refer to the [current decision record](decisions.md). Superseded decisions are kept in Git rather than in a second backlog.

## Correctness first

The original signature/result-check, nested-negation, scalar-cap and rule-certainty failures are repaired; union equivalence and the common-supertype contract are corrected too. Follow-ups fix signature stability across tiers and optimization, runtime argument diagnostic differences, exact excluded-set accumulation for range proofs, and DMN wildcard/scope handling (D-219, DD-43). The [open obligations](type-system-analysis.md#7-open-obligations-and-extensions) separate what is in place from the broader obligations below.

- [ ] Complete the remaining R1–R8 audit and validation work before claiming general soundness. Extend the permanent counterexamples into independent constructor, variance and bound-direction checks across every proof consumer and declaration/projection path. Path and descendant readers now approximate inspected unions locally. The remaining-reader audit repairs filter binding, recursive equality, descendant shapes, context/callback images and generic flattening; its bounded independent oracle covers structural declarations and positive subtype claims. Extend this to functions, recursive names, arbitrary host contexts and the full constructor space.
- [ ] Distinguish exact sets, possible-value upper bounds and certain-input lower bounds throughout analysis. A failed subtype proof must not be treated as proof of non-inclusion.
- [ ] Validate rule witnesses against the original unary tests. Coverage, overlap and dead-rule reports need the correct approximation direction and explicit assumptions.
- [ ] Track observable errors and effects separately from returned values. A non-null or constant result type does not establish that evaluation reports no error or cannot stop in strict mode.
- [ ] Strengthen independent semantic oracles and optimized/unoptimized comparisons on both backends, including strict-mode diagnostics, composite declarations, cap boundaries and higher-order values. Keep a reproducer when a sweep finds a failure; see the [sweep workflow](https://github.com/FeeJai/BDM/blob/main/apps/feel/scripts/sweep/README.md).

## Type precision and modeling

- [ ] Use the [narrowing gap catalog](narrowing.md#13-does-it-narrow-as-far-as-it-can) and tagged construct-suite cases to choose precision work. Three-outcome facts and stored-condition origins already exist (D-194); extend their coverage rather than reimplementing them.
- [ ] Preserve more callable summaries across returned aliases, selections, containers and bounded alternatives (D-171, D-193, D-203). Literal signatures already stay fixed in their kind-only written environment (D-219); new call summaries must preserve that distinction and alternatives such as empty-list selection results. Summary exhaustion must lose precision safely, including in negative positions.
- [ ] Extend guarded recursive relations and independent oracle coverage (D-189). Complete finite-data membership is implemented; general recursive subtyping and equivalence are not. Exercise generated mutual graphs before broadening proof rules, and improve call precision lost through graph projection, overlapping runtime signatures and complete-callee bounds without turning call facts into signature proofs.
- [ ] Extend argument-dependent built-in result rules beyond the existing list-function rules; improve certain-mismatch reporting when only nullability or an empty range/list keeps an overload alive (D-56, D-151, D-155). Do not reject valid empty or unbounded values.
- [ ] Represent additional list cardinalities and ranges known to have endpoints before using them to prove indexing or range-call facts. Decide which refinements need public syntax.
- [ ] Complete grain propagation through parameters, paths, filters, conditionals and temporal values (D-161, D-170). Declared grain, inferred grain and runtime rounding need one explicit contract.
- [ ] Extend inverse reasoning for time/date-time arithmetic, duration failure regions and additional predicates. Exercise zones, calendar clamping, fractional seconds and representational boundaries.
- [ ] Improve correlations between repeated compound expressions and related declarations. Independent interval bounds do not keep a relation such as `age <= max age` when both values vary.
- [ ] Define how a component constraint of a named type refers to its containing value (D-51, D-170). A variable-specific path such as `emp.limit` does not solve that reusable-type problem.
- [ ] Complete supported inverse facts for boolean built-ins used directly as conditions, range-valued `x in r`, powers, string prefixes and case conversion (D-194). An explicit fact-table representation remains a separate refactor, not an implemented feature.
- [ ] Preserve repeated-value correlation in string addition. `s + s` for a string whose allowed values are `"a"` and `"b"` is `"aa"`, `"ab"`, `"ba"` or `"bb"`, where one value gives `"aa"` or `"bb"`; the numeric one-value sums have a correlation rule (D-170, D-207). Duration self-addition also needs work: it can still combine independent intervals and admit mixed sums.
- [ ] Add month-duration scaling failure regions with the actual rounding semantics (D-204).
- [ ] Extend table-entry facts to later entries and use earlier rules' failure facts for `FIRST` outputs. Current narrowing uses only the matching rule's own entries (D-195).

## Unresolved interpretation choices

- [ ] Decide whether declared context member names should guide parsing after `.` and inside filters. D-27 currently uses lexical boundaries; changing this requires an explicit parsing contract.

## Declarations and language boundaries

- [ ] Preserve the meaning of composite declarations while compiling reusable membership checks. Current union/negation declarations can rebuild an analysis representation during each check (D-178); optimize only after membership correctness is established.
- [ ] Define allowed-value refinement and conversion rules for unions and negations. Host API support does not imply expression syntax for unions, intersections or arbitrary differences.
- [ ] Test the constraint of a member or an element of the result against the type the expression has for it, and not against the declared one. `AllowedValues.result_member/4` gives the tests the declared member type, so `{name: "M", age: 200}` for a type whose `age` allows `[0..150]` gets no `:unsatisfiable_allowed_values` when it is prepared, whereas the scalar `200` does get it; `:value_not_allowed` at run time is right in both. The member type of the inferred type is `Feel.Analysis.Paths.select/2` along the steps, and the elements of the lists for `:each`, falling back to the declared member where the inferred type is not a context or a list. The analyzer's `unsatisfiable_result/5` speaks only of the result as a whole (`steps: []`) and says nothing about `each: true`, so the warning also needs a clause for a member path with its own consequence. Keep the run-time check.
- [ ] Give a member of a declared context type written as a string the key that a value has (D-213). `Feel.Type.parse/2` keeps `"first  name"` as it is, while the entry `{"first  name": 1}` is keyed `first name`, so the member is not found in the value. Decide it with the same predicate.
- [ ] Resolve non-null contracts consistently: function parameter/result metadata, public type projection, and the currently rejected non-null `result_type` constraint (D-48). Preserve the repaired distinction between nullable runtime result signatures and precise call results, and the variance checks in public function projection, when extending this contract.
- [ ] Specify per-binding declaration policies and the assumptions exposed to callers. `:trust`, `:audit`, `:report` and `:ignore` do not establish the same facts as `:enforce`.
- [ ] External function definitions are `:not_implemented` unless an extension adds the function for their kind; `feel_java` does this for Java (D-211). Not done there: instance methods and constructors, other kinds (`pmml`, `onnx`), a precompiled class instead of the source a start compiles, and parallel calls (calls are serialized per sidecar).
- [ ] Treat B-FEEL semantics as separate work; the existing S-FEEL option restricts syntax. Clarify the intended S-FEEL role restrictions before adding another compatibility mode (D-49).
- [ ] Select further Camunda compatibility features from reproduced cases. Additions belong in extensions with explicit behavior, rather than silently changing core FEEL semantics (D-81).

## Resource bounds

- [ ] Further reduce transfers of required large values and DMN diagnostic source metadata without relaxing validation or containment. Prepared FEEL binding projection and compact DMN dependency views are implemented; unknown metadata and uncertain spellings conservatively fall back. Compare protected public APIs separately from the trusted engine benchmark; a constant-time expression can still have input-linear cost when it consumes a large list or context.

The [security model](architecture.md#security-model) describes current limits and caller isolation. Remaining work includes:

- [ ] Reduce repeated body analysis, specialization and type expansion within the existing worker deadline and heap policy. Evaluate preparation-local memoization or optional precision caps on measured expensive shapes; exhausting optional analysis must not skip required semantic checks. No general step quota is planned.
- [ ] Earlier accounting in BEAM emission, including large constants, before allocating all generated forms. The final statement-count check happens after emission.
- [ ] Audit allocation before heap-policy checks: retained backing binaries, value copies and host calls. Per-value limits and a process heap policy do not measure all VM memory use.
- [ ] A bounded hostile-input harness for preparation and evaluation, with external timeout/heap containment and recorded inputs. Avoid running resource-exhaustion probes in the caller's process.

## Performance

Measure with `scripts/bench.exs`; keep the command, revision, toolchain, workload and raw results with any optimization proposal. Fitted scaling exponents over a finite range are evidence, not complexity proofs.

- [ ] Investigate large generated branch chains and compiler cost in `:compile.forms`; compare flatter emission against current splitting before choosing a representation.
- [ ] Reduce repeated analysis of function bodies and composite declarations with preparation-local caching and bounded specialization. Do not merge analyses with different assumptions or effects.
- [ ] Profile the `:full`/`:core` seam and decide whether another analysis tier earns its maintenance cost.
- [ ] Evaluate reuse and BEAM break-even cost on representative decision workloads, not only small scalar expressions. Include preparation, module lifetime and cleanup.

## Release and tooling

- [ ] Implement the currently rejected `profile: :explain` only with bounded traces and a defined event vocabulary. Trace the original execution so diagnostics and host calls are not replayed for explanation.
- [ ] Expand mutation coverage around algebra, caps and proof consumers; periodically run the full sweeps and both backends. A passing slice can miss a small class of counterexamples.
- [ ] Triage generated-mutation survivors: separate safely wider types from missed under-approximations, rerun flaky cases, and sample further seeds (200 of 4,107 sites are done, D-217; the twelve too-small types it left to unit tests are seen by the sweeps since D-218). Left from D-206, D-217 and D-218:
  - The survivors of the first sample (six undecided, thirty held by unit tests) cannot be run again by name: the site count moved from 2,351 to 2,612 and the names are not those of the notes.
  - Sample the analysis files outside D-217's 17 (temporal arithmetic, null reasons, iterations, filters).
  - A thin catch is noticed when it is gone, not when it thins; a floor on the count would flag it earlier (`date` with a year past the calendar is caught by one binding of each of two expressions).
  - The `mutants` job is slow on a hosted runner: 2 cores, 6 to 8 minutes a mutant at `--jobs 2`, so 90 to 120 minutes for 27 (the 45-minute limit cancelled it with 9 to 13 of 19 done; `timeout-minutes` is 150 now). A private repository has 3,000 Actions minutes a month for everything, so it is in `.github/workflows/weekly.yml`, weekly and on request, and not in `ci.yml`: a change to the sweeps or the analysis needs a manual run of it before the merge. Shards of a matrix would cut the wall time and pay for the copy unchanged in each.
  - Exercise numbers past 1E6 without multiplying every ordinary pool: the two overflow mutants are held by unit tests only.
- [ ] Keep fixture provenance, known failures and accepted flag mismatches explicit. Review changes to TCK baselines rather than accepting every change through `--update`.
- [ ] Document API stability before publishing. The release scope is `feel` and `dmn` (the Java packages are not released for now). No version has been released; the assessments distinguish existing behavior from the proposed target design.