Every fact traces to a byte this run read
Overview | What It Returns | What It Will Not Do | Quick Start | How It Works | The Numbers
DeForm6 reads a compiled Visual Basic 6 executable and writes back a Visual Basic project. The first milestone recovers the metadata only: the forms, the control trees, the property values, the names, and the procedure signatures. It does not recover statements. Do not add a claim that it does.
One rule decides almost everything else in this repository.
Every fact DeForm6 reports traces to a byte it read, and it names how sure it is of each one.
Tools in this field tend to state a single confident figure and leave the reader to guess what sits behind it. DeForm6 does the opposite. It grades each recovered fact with one of three words, it writes down every place the read did not resolve, and it lists every boundary the run reached. A thing it cannot prove is reported as a thing it cannot prove.
| It gives | Because |
|---|---|
| A claim you can check | Each fact carries a confidence word, and the report says which byte or which assumption produced it |
| A refusal instead of a guess | The reader stops and names the offset it did not understand, rather than printing a tree it cannot prove |
| A limit you can read before you run it | Every open gap is a row in this file, with the safe default the tool chose |
| A number you can recompute | Every figure below is pinned in tests/ratios.toml, in tests/fidelity.toml or in a named test, and asserted on every run |
|
A run of
The JSON report holds exactly three top level keys: |
|
DeForm6 grades every recovered fact with one of three words: proven,
inferred, unrecoverable.
These are the only three words the JSON report's confidence field can hold.
There is no fourth tier and no numeric score.
| Word | Meaning |
|---|---|
proven |
The exact byte this run read names the fact directly. |
inferred |
This run chose the fact because the file gives no other answer, and the item's own basis field says so. |
unrecoverable |
This run could not recover the fact at all. |
Three limits are deliberate, so that meeting one reads as a decision rather than as something unfinished.
DeForm6 does not recover statements. The forms, the control trees, the property values, the names, and the procedure signatures come back. The code inside a procedure does not.
DeForm6 does not produce Basic source that a compiler accepts as a proof of the original program's behaviour. Every recovered item carries a confidence word, and a confidence word is not a promise of correctness.
DeForm6 does not open the Visual Basic 6 IDE and it does not compile anything. No sentence in this file states a recovery figure as a share of one hundred. Every capability sentence in this file traces to a report field, a confidence word, or a limit the report states in its own words.
scripts/check-claim-surface.sh holds those
three rules as a test.
It scans this file, the --help output and the report vocabulary for six
shapes of forbidden claim, and on every run it plants a violation of every
shape into every surface and requires the scan to catch each one.
A check that passes because it reads the wrong place is worse than no check.
-
In a P-code program, a handler address is not the address of machine code.
ProjectInfo.lpNativeCodedecides whether DeForm6 reports a project as native code or P-code, and nothing else does.corpus-pcode/holds a P-code build of 42 corpus programs, which the author built from the corpus source on a Windows host. Tests findlpNativeCode0 in each of them. From each one, DeForm6 recovers the objects of the source, in their order, and writes the same project that it writes from the native build of the same source. Each bound event slot gives a handler address, as in the native build. In a P-code program, that address is the entry of the method table of the object for the handler procedure. The event stub gives it toMethCallEnginein the runtime. -
corpus/vb6-code/Hidden-Markov-model/frmHMM.frxis damaged upstream and is excluded by name. The file is 56 bytes, and its own record header declares 56 bytes of payload, but only 55 are present, because the upstream repository setstext=autoand git's line ending normalisation silently removed one carriage return.HMM.exeholds the same string as a whole, correct record, and is the second, independent source of truth for this fault. DeForm6's own test corpus excludes this one file by name, rather than papering over the missing byte. -
One Windows host built the projects, and no test does. On the author's Windows XP machine, the Visual Basic 6 IDE built all 44 projects that DeForm6 wrote, and 42 of the 44 projects in the corpus.
tests/builds.tomlholds each result and the lines that VB6 wrote. The two corpus projects that do not build areEdge_Detection, whosecCommonDialog.clsis not in its directory, andHMM, whosefrmHMM.frxis damaged, as fact 2 says. DeForm6 knows theObject=line of one control only: the Winsock control, which the corpus holds. For another control, it writes the class identifier of the control on that line, and VB6 does not load the line. With such a line, the Winsock projects gave'MSWINSCK.OCX' could not be loaded. No test starts VB6, because the test machine has no Windows. The gate fails when DeForm6 writes different files than the Windows host built.
You need the Rust toolchain the repository pins, which is 1.97.1.
git clone https://github.com/Stiven-Gjekaj/DeForm6
cd DeForm6
cargo build --release
Read one executable and print what DeForm6 found in it:
deform6 inspect <path-to-exe>
Read one executable and write a Visual Basic 6 project directory that VB6 can open:
deform6 extract <path-to-exe> -o <output-directory>
The file holds no name for an event. A types file that derive-vb-types
writes from a copy of VB6.OLB that you own gives the events of each
control, and of each OCX that you add. With it, inspect names each bound
event slot, and extract writes each event handler of a P-code form under
the name and the parameters of its event, such as
Private Sub Form_KeyPress(KeyAscii As Integer). A handler of a native build
keeps its generated name.
cargo run -p xtask -- derive-vb-types <path-to-VB6.OLB> [<path-to-OCX>...]
deform6 extract <path-to-exe> -o <output-directory> --vb-types derived/vb-types.toml
The properties of a form need a property opcode table. The table built into
DeForm6 names few properties. derive-opcode-table writes a table from the
same copy of VB6.OLB. With it, extract gives 4788 of the 5113 property
lines of the source .frm files of the corpus. The built-in table gives
193.
cargo run -p xtask -- derive-opcode-table <path-to-VB6.OLB>
deform6 extract <path-to-exe> -o <output-directory> --opcode-table derived/opcode-table.toml
Print the P-code of each procedure of a P-code program. The opcode table is
not in this repository. Fetch the symbols of a copy of MSVBVM60.DLL that you
own, derive the table from the two files, and check it against the P-code
corpus:
cargo run -p xtask -- fetch-pcode-symbols <path-to-MSVBVM60.DLL>
cargo run -p xtask -- derive-pcode-table <path-to-MSVBVM60.DLL> derived/symbols/MSVBVM60.pdb
cargo run -p xtask -- check-pcode-table
deform6 disasm <path-to-exe> --pcode-table derived/pcode-table.toml
The interfaces of the controls are not in this repository either. Derive
them from a copy of VB6.OLB that you own. Give MSVBVM60.DLL too, and the
file also holds the VBA library of the runtime, such as Err and
Collection. Give an OCX too, such as MSWINSCK.OCX, and the file names
the members of its controls:
cargo run -p xtask -- derive-vb-types <path-to-VB6.OLB> <path-to-MSVBVM60.DLL> [<path-to-OCX>...]
cargo run -p xtask -- check-pcode-table --vb-types derived/vb-types.toml
deform6 disasm <path-to-exe> --pcode-table derived/pcode-table.toml --vb-types derived/vb-types.toml --lift
The listing gives each opcode, its bytes and the name of its handler. It is not Basic.
With --lift, disasm prints a procedure as statements when it can follow
the stack of every opcode: 239 of the 680 procedures of the P-code corpus,
673 with --vb-types from VB6.OLB, and 680 when the file also holds the
VBA library. The statements name each variable by its offset, such as
local_88 or field_54. They name a called procedure of the project by
its name when it is public, such as Me.makeSpecialString, and else by its
index, such as Me.method_16. A call of a module gives the module, such as
Sub_Module.method_1(), and a call of a Declare gives its export name,
such as GetObjectA. With --vb-types they name the controls and
their properties, such as Me.chkAutomatic.Value, and the functions of the
runtime, such as VBA.Err().Clear(). A late-bound call on a control of an
OCX names its member when the file holds the OCX, such as
Me.WskClient.SendData("Msg_Eof_"), and else it gives its DISPID, such as
Me.WskClient.[DISPID 0x43]("Msg_Eof_").
They take the forms of Basic where the lift knows them: ReDim a(0 To 7),
Open p For Binary As #1, Exit Sub or Exit Function, Screen.Width,
frmAbout.Visible, and an empty place for an argument that a call leaves
out.
The statements are not the source. extract writes none of them unless
you give --lift:
deform6 extract <path-to-exe> -o <output-directory> --pcode-table derived/pcode-table.toml --vb-types derived/vb-types.toml --lift
With --lift, extract writes the lift of each procedure into its body,
with a Dim or a declaration for each variable that the lift names. It
writes each branch that fits a block as that block, such as If, Else,
Do While, Loop While, For and Exit For, and each other branch as a
GoTo and a label. In the P-code corpus, 2 GoTo statements stay.
cargo run -p xtask -- export-lift-builds <dir> writes each P-code program
of the corpus this way, for a build with the Visual Basic 6 IDE on a
Windows host. On the author's Windows XP host, VB6 builds 42 of the 42
lifted projects. Both sides build as P-code, as the corpus binary was
built. runs.bat starts each rebuilt program and its original, and sends
the same keys to each, from scripts/vm/steps.toml. With a table from
derive-opcode-table, each of the 226 screens of the 41 programs is the
same as the original: 205 pixel for pixel, 15 in the window of a program
that Windows places, and 6 outside the boxes where a program draws random
values. 175 of the 185 steps change the screen of the original. The
variables keep the names of their offsets, such as local_88, apart from
the public variables.
scripts/vm/README.md gives the steps of such a run.
check-pcode-table holds the statements against the source: 3246 of the 4093 string
literals and names after a . of the source are in the lift. Most of the
others are the fields of a user-defined type, which the lift names by their
offsets.
Run everything the gate runs, in one command:
cargo fmt --all --check && cargo clippy --all-targets -- -D warnings && cargo test --workspace
DeForm6 gives one of six exit codes.
| Code | Meaning |
|---|---|
| 0 | The file was read. |
| 1 | Not a PE file. |
| 2 | A PE file, but it holds no Visual Basic runtime. |
| 3 | Visual Basic, but not version 6. |
| 4 | Visual Basic 6, but damaged. |
| 5 | An internal error, including a usage error. |
one Visual Basic 6 executable
-> the PE reader resolves the entry point through the section table
-> the entry stub leads to the VB header, and the runtime DLL name
separates VB6 from VB5
-> the object table gives the objects, their kinds and their names
-> the prototype walk gives the procedure signatures
-> the GUI table gives the forms, and each form gives its control tree
-> the property walk gives the property records and the resource blobs
-> every write is planned, and the whole run refuses before it writes
anything if one planned path escapes the output directory
-> the project directory and one JSON report are written
--salvage changes what a recoverable defect costs.
| Severity | Strict | Salvage |
|---|---|---|
Fatal |
Refuses the run | Refuses the run |
Recoverable |
Refuses the run | Loses that one item and continues |
Tolerated |
Loses that one item and continues | Loses that one item and continues |
Both modes collect the same defect list, because the whole list is recorded before the run refuses on any of it. A strict run that stopped at the first error would only ever show a prefix of it.
| Layer | Choice |
|---|---|
| Language | Rust 2024, pinned at 1.97.1 |
| Memory safety | #![forbid(unsafe_code)] across the workspace |
| Arithmetic | checked_add on every file derived offset, with clippy::arithmetic_side_effects denied |
| Slicing | A bounded Region reader with no infallible accessor, with clippy::indexing_slicing denied |
| Panics | unwrap, expect and panic denied on any path that touches file derived data |
| Library | crates/deform6, which never opens a file |
| Command line | crates/deform6-cli, which owns the file system |
| Build tasks | crates/xtask, including the licence audit that writes LICENSES.md |
| Fuzzing | cargo-fuzz over the parser, run by its own workflow |
The numbers below are measured, not estimated. Each one is the number a pinned file or a pinned constant states, and the gate test named beside it, or above its table, asserts it on every run, never a single derived figure calculated from a part.
| Measured | Against | Asserted by |
|---|---|---|
| 44 Visual Basic 6 programs in the test corpus | cargo test -p deform6 --test corpus_sweep |
|
| 185 procedure signatures recovered | 904 declared | cargo test -p deform6 --test ratios |
| 53 forms recovered | 53 declared | cargo test -p deform6 --test ratios |
| 708 controls recovered | 708 declared | cargo test -p deform6 --test ratios |
935 property records recovered with the built-in opcode table, of which 242 written lines reach the .frm |
cargo test -p deform6 --test ratios |
When a form refuses, the refusal names the byte offset and the byte the code expected to find there. A refusal is the correct result, because the tool does not print a tree it cannot prove. No corpus form refuses now.
A single recovered Position record becomes four written lines and a single
Font record becomes seven, so the property pair is a coverage count for
DeForm6's own writer, not a recovery count against source.
DeForm6 writes each structure back over the place it was read from and
compares the result with what is there.
A byte that goes back unchanged is one the reader reproduces.
cargo test -p deform6 --test byte_fidelity asserts every row.
tests/fidelity.toml holds these numbers for each corpus program.
cargo run -p xtask -- update-fidelity writes that file, and
cargo test -p deform6 --test fidelity_map fails when a value in it moves.
| Structure | Bytes reproduced | Record length | Records |
|---|---|---|---|
| VB header | 50 | 104 | 44 |
ProjectInfo |
20 | 572 | 44 |
Declare table entry |
8 | 8 | 249 |
Declare descriptor |
8 | 24 | 220 |
| GUI table entry | 8 | 80 | 53 |
GUIObjectInfo |
4 | 93 | 53 |
| Object table | 12 | 84 | 44 |
Object |
20 | 48 | 105 |
ObjectInfo |
6 | 56 | 105 |
PrivateObj |
16 | 64 | 97 |
OptionalObjectInfo |
8 | 64 | 97 |
ControlInfo |
16 | 40 | 706 |
| Event stub | 13 | 13 | 390 |
No reproduced byte differs from the file in any of the 2207 records, and no two records claim the same byte.
The reader keeps what 8 of the 13 bytes of an event stub hold. The other 5 are the opcodes of the native stub. The reader checks them and keeps no field for them, and the emitter writes them back as constants.
A Declare descriptor is written back only for an entry of type 7.
The reader keeps its first 8 bytes, which hold the addresses of the library
name and the export name.
This is a coverage figure and not a proof of correctness.
A field that is read at one offset and written back at the same offset cannot
disagree with itself.
The information is in the bytes that no field of the model claims at all.
docs/STRUCTURES.md names most of them, so they are mostly work not yet done.
Some are real unknowns: the GUI table entry holds several words that no
source names.
Most of the reader's clamps bound a loop and change no byte, so the table
above cannot see them.
A clamp makes the reader return fewer items than the file declares, so a
second measurement counts both.
cargo test -p deform6 --test array_census asserts every row.
| Array | Declared | Returned |
|---|---|---|
Declare table entries |
249 | 249 |
| GUI table entries | 53 | 53 |
| Objects | 105 | 105 |
ControlInfo entries |
706 | 706 |
| Event slots | 11862 | 11862 |
No array in any corpus program comes up short. The same test changes a file in memory to make each kind of shortfall happen, and requires the count to name it.
The 706 ControlInfo entries are not controls.
ControlInfo is the table that binds controls to their events, and the 708 in
the first table count the nodes in the control tree, which is a different
quantity.
A gap that is still open at release is a documented limit, not a silent one.
The rows below come from two surveys: docs/STRUCTURES.md
section 11, the structure gap register, and
docs/FILE-FORMATS.md section 9, the file format gap
list.
| Limit | What is not known | What the tool does instead |
|---|---|---|
| S-02 | Which bit of fObjectType reliably marks that the optional half of ObjectInfo is present. Two published tests disagree with the corpus. |
The tool tests bit 0x2, the only bit that separates a standard module from every other kind across all seventeen tabulated values. It reports an object whose bit disagrees with its private object address. |
| S-03 | No source names the raw fObjectType value an MDIForm carries. |
The tool classifies any value outside the three the corpus proves as Unknown, and carries the raw number forward in the report instead of guessing a name. |
| S-04 | How a ParamArray argument modifier is encoded. No corpus source declares one. |
The tool never emits the ParamArray modifier. The argument decodes under its ordinary type code, because the documented modifier bits are indistinguishable from a plain ByRef Variant argument. |
| S-05 | What Visual Basic type sixteen of the type code positions name: 0x00-0x02, 0x04, 0x07, 0x09, 0x0E, 0x11, 0x12, 0x14-0x1A. None occurs in the corpus. |
The tool reports the type as Unknown and carries the raw byte forward, rather than guessing a name. |
| S-06 | Which of two disputed FuncTypDesc header layouts is correct. |
The tool checks a fixed marker word at this position on every record, and reports a defect instead of building a prototype when the marker does not match, rather than parsing the disputed alternate layout. |
| S-07 | Where the optionalVals pointer's value comes from, and what governs it at the source level. |
The tool walks a length prefixed run of default value records behind the pointer, and stops the walk and reports that record's own defaults as unrecoverable when it meets a value tag it does not recognise, rather than guessing a width. |
| S-08 | How wide one entry of the PubVarDesc array is, so the array can be walked. No stride hypothesis converges against the corpus. |
The tool carries the count field forward as an unexplained open question in the report, and does not walk the array at all. |
| S-09 | How to recover the source level name of an event slot. No corpus program carries a single EventDesc record. |
The tool walks the event pointer array and reports the address of each entry, and decodes no name from any of them. |
| S-10 | How a source level Alias "#123" ordinal import is encoded in the compiled file. |
When the Visual Basic level name is not present in the file, the tool reports the export as an inferred ordinal number, rather than guessing a name. |
| S-12 | Whether the byte at control block offset 0x02, named uni by one prior tool and never read by it, is a Unicode flag for the name that follows. |
The tool does not read this byte into any field. It is skipped as part of the fixed header the tool does not interpret. |
| S-13 | The exact character range and code page a written string obeys. | This run assumes a Western code page. Every character above U+00FF was replaced with a question mark and reported, never guessed at a different code page. |
| S-14 | Whether a menu that is itself a sibling within an already open menu group, opening its own child, reads the same as a confirmed sibling case; and one separate case where an expected separator byte is not present at all. | The tool decodes the two level deep menu close transitions measured across five transitions in two programs, and reports a defect naming the byte offset when the walk meets a byte that is not the expected separator, rather than guessing an ambiguous depth. |
| S-15 | The property name behind most control type and opcode pairs. | The tool ships a small, safe provenance "Opcode table" built into the binary, states its own size in the report's limits array, and reports a property it cannot name as present and not decoded, rather than guessing a name. A user can supply a larger table built on their own lawful Visual Basic 6 install. |
| S-16 | What the nine unknown dwords in GUIObjectInfo hold. |
The tool does not read these bytes into any field, and reports nothing from them. |
| S-17 | What the five unknown dwords in the external component entry hold. | The tool decodes only the two fields it uses, oUuid and the textual GUID offset and length. The other fields carry no struct field, and the tool reports nothing from them. |
| S-18 | Whether an entry point opcode other than the one all 44 corpus executables share is a valid, undocumented variant. | The tool accepts only the one push immediate opcode the whole corpus shares, and refuses any other opcode with an error naming what it expected at the entry point. |
| Limit | What is not known | What the tool does instead |
|---|---|---|
| F-01 | The exact character count where the IDE moves a string property from the .frm into the .frx. The corpus bounds it between 99 and 153 characters but does not fix it. |
The tool always writes the string inline when it is 97 characters or shorter and holds no line break, the proven floor of the open range. |
| F-02 | Whether a second, healthy multi line TextBox sample would confirm the reconstructed u8 count, or point to a different width. |
The tool writes the $ form with a u32 count, proved exactly by one corpus file, for every string that must go to the .frx. |
| F-03 | Whether the loader tolerates a missing Attribute line. No corpus file omits one, and no document states a requirement. |
The tool writes all five Attribute lines, always. |
| F-04 | Whether .vbp key order matters. Not documented, and the one independent parser the survey checked does not care. |
The tool matches the order the IDE itself writes. |
| F-05 | The List record layout for ListBox. One ComboBox of the corpus stores its List and ItemData in a .frx, and its record holds the same bytes as the form stream. No ListBox of the corpus stores a list. |
The tool copies the bytes of the form stream into the .frx for both controls. The .frx of PassGen.exe equals its source, byte for byte. |
| F-06 | A second record shape one prior tool documents for small to medium text, including an off by one bug that tool warns about. Unverified against this corpus. | The tool never writes this record shape. Every string routed to the .frx uses the one shape the corpus proves, the $ form with a u32 count. |
| F-07 | How DeForm6 should choose a code page for a Japanese or Cyrillic Visual Basic 6 project. Every corpus file is Western. | The tool assumes a Western code page on every run, and replaces every character above U+00FF with a question mark, reporting that it did so, rather than guessing a different code page. |
| F-08 | The .ctx record layout, assumed identical to .frx and not checked. This matters only when ActiveX control projects come into scope. |
The tool does not read or write .ctl or .ctx files. ActiveX control projects are out of scope for this milestone, per PROJECT.md. |
| F-09 | Whether an MDIForm project, root class VB.MDIForm and a child form carrying MDIChild = -1, reads the way the one cited source states. No corpus program is an MDIForm project. |
The tool classifies an MDIForm's fObjectType value as Unknown, the same fallback S-03 describes, and writes whatever property values it reads with no MDIForm-specific handling. |
| F-10 | Whether the VB6 IDE ever wrote a comma decimal separator, such as Size = 8,25, on a non-English machine. The corpus is English only. |
The tool always writes a period as the decimal separator, using Rust's own locale independent number formatting, regardless of the host machine's locale. |
Sixteen rows come from the structure survey and ten rows come from the file format survey: twenty six limits, still open at release, each with the default the tool chose in their place.
crates/
deform6/ the library: it never opens a file
src/read/ the PE reader and the bounded Region type
src/vb/ the VB6 structures: header, objects, prototypes, forms
src/write/ the project writer: .vbp, .frm, .frx, .bas, .cls
src/report.rs the JSON report: items, defects, limits
src/error.rs the defect vocabulary and its three severities
src/journal.rs the one place a severity decides whether a run continues
schema/ the JSON Schema every report is validated against
tests/ 26 integration suites, including the corpus sweep
deform6-cli/ the command line: it owns the file system
xtask/ build tasks, including the licence audit
docs/ the reverse engineering surveys the source cites
scripts/ the walls: each one proves a property and fails loudly
corpus/ 44 Visual Basic 6 programs, with sources, and a manifest
corpus-pcode/ a P-code build of 42 of those programs, with notices
tests/ratios.toml the pinned recovery figures the gate asserts
tests/fidelity.toml the committed fidelity map the gate asserts
tests/builds.toml the build record the gate holds the tree to
tests/pcode.toml the P-code record the gate holds the tree to
Two ideas carry the design.
The bounded region.
Region is the only way the library reads bytes, and it has no infallible
accessor.
A read that runs past the end of what the file actually holds returns an
error rather than a panic or a wrong value.
This is what lets #![forbid(unsafe_code)] and the clippy deny wall hold
across a parser that reads hostile input.
One place decides whether a run continues.
Journal::record holds one arm for each pair of severity and mode, six in
all, and no wildcard arm.
A new severity stops the build until somebody decides its policy in both
modes.
Every defect the run collected passes through it, in the order it was
collected.
cargo test --workspace
1646 tests run. The suite includes:
- The corpus sweep. All 44 programs are read and report what they hold.
- The structural check. Every extracted project is checked against the shape the IDE expects.
- The build record.
tests/builds.tomlholds what the Visual Basic 6 IDE built on the author's Windows host, for each corpus program. The gate fails when DeForm6 writes different files than that host built, until the host builds them again. - The P-code record.
tests/pcode.tomlholds what the same host built as P-code for each corpus program, andcorpus-pcode/holds each binary. The gate checks each binary against its hash, finds P-code in each one, and fails when a corpus source changes, until the host builds it again. - The P-code recovery. Each P-code binary gives the objects of its source
in their order, and DeForm6 writes the same project from it as from the
native build. Each handler address names the method of a source procedure
of its control, and each event stub goes to
MethCallEngine. - The schema check. Every one of the 44 reports is validated against
crates/deform6/schema/report.schema.json, and a doctored report is proved to fail. - The ratio gate. Every pinned figure in
tests/ratios.tomlmust hold unchanged. - The no-panic proof. Every corpus input, native and P-code, is swept through both modes, the writer and the byte fidelity walk. Every public entry point that takes untrusted bytes belongs in that sweep.
- The hostile corpus. Mutated and crafted inputs, including a form count
of
0xFFFFin a 4096 byte file, which must allocate nothing. - The byte fidelity map. The thirteen structures in the table above are written back over the bytes they were read from and compared against them, over all 44 programs. The bytes the reader reproduces and the bytes no field of it claims are both pinned.
- The committed fidelity map. The totals of each corpus program in
tests/fidelity.tomlmust hold unchanged. A value that moves fails the gate, and the message says whether the move is a regression. - The array census. For the five arrays in the table above, the count the file declares is compared with the number of items the reader returns, and the count is read back from the file at the offset the census names.
- The walls.
scripts/prove-*.sheach prove one property, by planting a violation and requiring the check to catch it.
The fuzz target lives in crates/deform6/fuzz and runs in its own workflow.
It is excluded from the stable workspace, so cargo test --workspace never
builds it.
Read AGENTS.md first. It states the rules this repository holds
itself to, and they are not style preferences:
- No
unsafe, anywhere. checked_addon every offset derived from a file. No bare arithmetic.- No
unwrap,expectorpanicon a path that touches file derived data. - A fact the tool cannot prove is reported as unproven. It is never guessed.
- A new claim in this file needs a measurement behind it, and
scripts/check-claim-surface.shis the test that says so.
The gate is nine steps and every one has to pass. Run them all with one
command, which is what .github/workflows/gate.yml runs, in the same order:
sh scripts/gate.sh
An earlier version of this file said the gate was three commands. It is not,
and the three it named leave out cargo doc, which denies a broken or private
documentation link and which neither cargo clippy nor cargo test reports.
scripts/gate.sh reads the workflow and refuses to run when the workflow names
a check the script does not, so the two cannot drift apart in silence.
MIT. See LICENSE.
Every third party licence in the dependency tree is audited into
LICENSES.md, which is re-derived from cargo metadata rather
than written by hand.