Add exact text semantic reference and oracle

.github/workflows/exact-text.yml

@@ -0,0 +1,61 @@
+name: Exact text semantic oracle
+
+on:
+  pull_request:
+    paths:
+      - 'src/IB/ExactText.idric'
+      - 'src/ExactTextSmoke.idric'
+      - 'docs/exact-text-search.md'
+      - '.github/workflows/exact-text.yml'
+      - 'bin/ci_browser_foundation.grease'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  oracle:
+    runs-on: ubuntu-latest
+    env:
+      IDRIS2_CG: chez
+      SCHEME: scheme
+      IDRIC_REF: 61970be77769f607cca8650bf424c0f0b22ddee7
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Install compiler dependencies
+        run: sh bin/ci_browser_foundation.grease install-dependencies
+
+      - name: Restore Idric compiler
+        id: idric-cache
+        uses: actions/cache/restore@v4
+        with:
+          path: /tmp/idric
+          key: idric-${{ runner.os }}-61970be77769f607cca8650bf424c0f0b22ddee7
+
+      - name: Build and install Idric compiler
+        if: steps.idric-cache.outputs.cache-hit != 'true'
+        run: sh bin/ci_browser_foundation.grease build-idric
+
+      - name: Compile exact text oracle
+        run: |
+          cd src
+          /tmp/idric/bin/idris2 ExactTextSmoke.idric -o ib-exact-text 2>&1 | tee /tmp/exact-text-compile.txt
+          test -x ./build/exec/ib-exact-text
+          ! grep -q '^Error:' /tmp/exact-text-compile.txt
+
+      - name: Check exact positions and counts
+        run: |
+          src/build/exec/ib-exact-text | tee /tmp/exact-text.txt
+          grep -Fx 'absent-contains=False' /tmp/exact-text.txt
+          grep -Fx 'absent-positions=[]' /tmp/exact-text.txt
+          grep -Fx 'absent-count=0' /tmp/exact-text.txt
+          grep -Fx 'beginning-positions=[0]' /tmp/exact-text.txt
+          grep -Fx 'middle-positions=[2]' /tmp/exact-text.txt
+          grep -Fx 'end-positions=[2]' /tmp/exact-text.txt
+          grep -Fx 'overlap-positions=[0, 2]' /tmp/exact-text.txt
+          grep -Fx 'overlap-count=2' /tmp/exact-text.txt
+          grep -Fx 'one-byte-positions=[1, 3, 5]' /tmp/exact-text.txt
+          grep -Fx 'repeated-prefix-positions=[4]' /tmp/exact-text.txt
+          grep -Fx 'empty-positions=[0, 1, 2, 3]' /tmp/exact-text.txt
+          grep -Fx 'empty-count=4' /tmp/exact-text.txt

docs/exact-text-search.md

@@ -0,0 +1,70 @@
+# Exact interior-text search
+
+IB now has a deliberately plain Idriç semantic reference for exact substring search in `src/IB/ExactText.idric`.
+
+This is the operation that PR #9 described only as a future "grep-like pass". It is unrelated to PR #17's exact vector scan: that scan walks a 10,000 × 384 Float32 vector index and computes dot products, while this one walks ordinary text looking for an exact literal.
+
+## Semantic reference
+
+The portable reference is intentionally boring:
+
+1. test whether the wanted characters are a prefix at the current position;
+2. if not, move forward by one character;
+3. repeat until a match or the end.
+
+`contains_string` short-circuits on the first match. `match_positions` records every zero-based character position, including overlaps, and `match_count` is its length. The empty pattern matches every character boundary, including the end.
+
+That source remains the oracle even if production lowering later uses a completely different algorithm.
+
+## First deterministic fixtures
+
+`ExactTextSmoke.idric` fixes the cases we need before optimizing anything:
+
+- absent match;
+- beginning, middle, and end matches;
+- overlapping matches (`aba` in `ababa`);
+- one-character pattern;
+- repeated-prefix/adversarial input (`aaaaab` in `aaaaaaaaab`);
+- empty-pattern behavior.
+
+The first ARM benchmark should stay ASCII so byte offsets and character offsets coincide. Unicode text can be added after the backend API says explicitly whether it returns byte offsets, character offsets, only a Boolean, or a count.
+
+## Compiler/backend experiment
+
+The architectural question is not whether C is slow. A competent C/library implementation is a required baseline.
+
+The question is whether preserving the semantic operation long enough lets a target backend choose a better realization than flattening the request immediately into generic character iteration and nested branches.
+
+For ARM/Thumb, candidates include:
+
+- ordinary scalar comparison;
+- short-literal word comparisons;
+- packed Shift-And/Shift-Or state when the literal fits the usable machine word;
+- candidate-byte filtering plus verification;
+- table/state-machine dispatch where that shape actually wins;
+- NEON/SIMD only on targets where it is available and profitable.
+
+The corresponding compiler-design note is `isomorphisms/Idric#21`. ARM/Thumb experiments are tracked in `isomorphisms/idric-arm-thumb#9`, `#10`, and the IB-workload bridge `#11`. Browser-side tracking is `isomorphisms/ib#33`.
+
+## Current backend boundary
+
+The current ARM/Thumb backend is still a runtime-free straight-line numerical leaf backend. PR #8 deliberately adds branch/dispatch fixtures but does not yet add branches, loops, byte-buffer input, Bool/integer returns, strings, or general runtime support.
+
+So this branch makes the browser semantic workload executable first. The ARM implementation should be stacked separately and should not fake success by replacing the browser oracle with a backend-shaped toy.
+
+## Evidence rule
+
+For every backend realization, keep together:
+
+- the exact source fixture and literal/input bytes;
+- semantic result, match positions/count where applicable;
+- emitted assembly and object/disassembly;
+- code size;
+- bytes scanned;
+- setup/table cost separately from steady-state scan;
+- wall time/cycles on representative hardware;
+- target identity and SIMD capability;
+- a competent ordinary implementation as the comparison point;
+- non-wins and regressions as evidence.
+
+This gives IB a real browser workload and gives the compiler work a before/after benchmark without making unusual instructions the goal by themselves.

src/ExactTextSmoke.idric

@@ -0,0 +1,22 @@
+module ExactTextSmoke
+
+import IB.ExactText
+
+%default total
+
+emit_fixture : String → String → String → IO ()
+emit_fixture label wanted text = do
+  putStrLn (label ++ "-contains=" ++ show (contains_string wanted text))
+  putStrLn (label ++ "-positions=" ++ show (match_positions wanted text))
+  putStrLn (label ++ "-count=" ++ show (match_count wanted text))
+
+main : IO ()
+main = do
+  emit_fixture "absent" "needle" "haystack"
+  emit_fixture "beginning" "browser" "browser body"
+  emit_fixture "middle" "needle" "xxneedleyy"
+  emit_fixture "end" "needle" "xxneedle"
+  emit_fixture "overlap" "aba" "ababa"
+  emit_fixture "one-byte" "a" "banana"
+  emit_fixture "repeated-prefix" "aaaaab" "aaaaaaaaab"
+  emit_fixture "empty" "" "abc"

src/IB/ExactText.idric

@@ -0,0 +1,45 @@
+module IB.ExactText
+
+%default total
+
+-- This deliberately simple implementation is the semantic oracle for IB's
+-- exact interior-text search.  Keep it understandable even if a backend later
+-- replaces the scan with packed bits, SIMD, or another target-specific form.
+starts_with : List Char → List Char → Bool
+starts_with [] _ = True
+starts_with (_ :: _) [] = False
+starts_with (wanted :: more_wanted) (actual :: more_actual) =
+  if wanted == actual
+    then starts_with more_wanted more_actual
+    else False
+
+contains_chars : List Char → List Char → Bool
+contains_chars [] _ = True
+contains_chars (_ :: _) [] = False
+contains_chars wanted text@(_ :: rest) =
+  if starts_with wanted text
+    then True
+    else contains_chars wanted rest
+
+public export
+contains_string : String → String → Bool
+contains_string wanted text =
+  contains_chars (unpack wanted) (unpack text)
+
+match_positions_from : Nat → List Char → List Char → List Nat
+match_positions_from offset wanted [] =
+  if starts_with wanted [] then [offset] else []
+match_positions_from offset wanted text@(_ :: rest) =
+  let later = match_positions_from (S offset) wanted rest in
+    if starts_with wanted text then offset :: later else later
+
+-- Positions are zero-based character positions and overlapping matches count.
+-- The empty pattern matches every character boundary, including the end.
+public export
+match_positions : String → String → List Nat
+match_positions wanted text =
+  match_positions_from 0 (unpack wanted) (unpack text)
+
+public export
+match_count : String → String → Nat
+match_count wanted text = length (match_positions wanted text)