Part of #11 (Gap 2).
The difference this buys
The technical leg is solo: Ferrocene's compiler source is public and CompCert can be used non-commercially, so "the rendered output compiles with that toolchain and agrees byte-for-byte with the reference leg and wasm" can be demonstrated in-house. What cannot be demonstrated in-house is the qualified attribute: the qualification document package (safety manual, qualification report, known-problems list) that a customer folds into their own tool-qualification argument. That package is licensed.
What is needed
Exit
A licensed, version-pinned qualified toolchain named in the chain, with its qualification material available to a customer.
Part of #11 (Gap 2).
The difference this buys
The technical leg is solo: Ferrocene's compiler source is public and CompCert can be used non-commercially, so "the rendered output compiles with that toolchain and agrees byte-for-byte with the reference leg and wasm" can be demonstrated in-house. What cannot be demonstrated in-house is the qualified attribute: the qualification document package (safety manual, qualification report, known-problems list) that a customer folds into their own tool-qualification argument. That package is licensed.
What is needed
Exit
A licensed, version-pinned qualified toolchain named in the chain, with its qualification material available to a customer.