Hugging Face's logo

phanerozoic
/
threshold-computers

threshold-logic
neuromorphic
computer-architecture
recurrent-neural-network
in-memory-computing
self-replication
loihi
truenorth
akida
Model card Files
xet
 Community
threshold-computers / rocq /Assumptions.v
phanerozoic's picture
phanerozoic
Put the organism first and move serialization, sizes and the Rocq map to appendices
5ee1fb5
Raw History Blame Contribute Delete
6.53 kB
(* The assumptions of the main theorems, printed by src/paper.py rocq after the build. The theorems on the netlists,
the machines and the programs depend on no axiom; those on real numbers on the axioms of the standard library's
real numbers; the numbers evaluated by the interval tactic also on the specifications of the primitive integers and
floating-point numbers. *)
Set Warnings "-ambiguous-paths".
From TH Require Import PhysSem PhysMain PhysFacts NetMain Complete Decoder Run PassLemma Main HostSem Pstar
StoredBoot StoredPass StoredDev StoredOk StoredRun StoredWbr StoredMain StoredWidth
Recipe Lower Lev HostLev HostCount StoredProp StoredCount PhysLev Margin Erfc Choose Noise NoiseNum Restore FlipLower
AmpHost FoldHost Compile Schedule Gates Adder.
Set Warnings "ambiguous-paths".
Print Assumptions Gates.sAND_fire.
Print Assumptions Gates.sOR_fire.
Print Assumptions Adder.sub_value.
Print Assumptions Adder.carry_closed.
Print Assumptions PhysSem.netlist_step.
Print Assumptions PhysMain.network_orbit.
Print Assumptions PhysFacts.phys_size.
Print Assumptions PhysFacts.phys_ternary.
Print Assumptions Complete.describe_complete.
Print Assumptions PassLemma.machine_pass.
Print Assumptions Decoder.generation.
Print Assumptions Run.universal_construction.
Print Assumptions Run.uc_window.
Print Assumptions Main.builds_every_image.
Print Assumptions Main.reproduces.
Print Assumptions Main.copies.
Print Assumptions Main.periodic.
Print Assumptions NetMain.network_reproduces.
Print Assumptions NetMain.network_periodic.
Print Assumptions HostSem.host_step.
Print Assumptions Pstar.constructor_run.
Print Assumptions Pstar.selfrep_run.
Print Assumptions Pstar.image_Pstar_8.
Print Assumptions Pstar.image_P_8.
Print Assumptions StoredBoot.startup_run.
Print Assumptions StoredPass.step_view.
Print Assumptions StoredDev.device_run.
Print Assumptions StoredBoot.handover_run.
Print Assumptions StoredOk.stored_ok.
Print Assumptions StoredPass.pass_first.
Print Assumptions StoredPass.pass_next.
Print Assumptions StoredRun.machine_pass.
Print Assumptions StoredRun.stored_construct.
Print Assumptions StoredWbr.wbr_stored.
Print Assumptions StoredMain.reproduces.
Print Assumptions StoredMain.copies.
Print Assumptions StoredMain.periodic.
Print Assumptions StoredMain.network_reproduces.
Print Assumptions StoredMain.network_periodic.
Print Assumptions StoredWidth.width_exists.
Print Assumptions StoredWidth.recipe_of_image.
Print Assumptions StoredProp.stored_pass.
Print Assumptions Schedule.pass_run.
Print Assumptions Schedule.sched_run.
Print Assumptions Schedule.netlist_pass.
Print Assumptions Compile.atleast_rec.
Print Assumptions Compile.compile_unit.
Print Assumptions Compile.compile_records.
Print Assumptions Recipe.desc_spec.
Print Assumptions Recipe.describe_spec.
Print Assumptions Recipe.recipes_complete.
Print Assumptions Recipe.recipe_optimal.
Print Assumptions Recipe.describe_steps.
Print Assumptions Recipe.psteps_lower.
Print Assumptions Lev.lev_ok.
Print Assumptions Lev.lev_units.
Print Assumptions Lev.lev_widths.
Print Assumptions Lev.lev_size.
Print Assumptions HostLev.host_dmax.
Print Assumptions HostLev.host_lev_widths.
Print Assumptions HostLev.host_lev_rows.
Print Assumptions HostLev.host_lev_widths_8.
Print Assumptions HostLev.host_lev_rows_8.
Print Assumptions HostLev.host_lev_dense_8.
Print Assumptions HostLev.host_lev_widest_8.
Print Assumptions HostCount.host_units_count.
Print Assumptions HostCount.host_memory_count.
Print Assumptions HostCount.host_edges.
Print Assumptions HostCount.host_weights_biases.
Print Assumptions HostCount.host_lev_identity.
Print Assumptions HostCount.host_units_8.
Print Assumptions HostCount.host_edges_8.
Print Assumptions HostCount.host_memory_8.
Print Assumptions HostCount.host_lev_identity_8.
Print Assumptions HostCount.host_lev_nonzero_8.
Print Assumptions FoldHost.fold_wf.
Print Assumptions FoldHost.fold_step.
Print Assumptions FoldHost.fold_dmax.
Print Assumptions FoldHost.fold_units_count.
Print Assumptions FoldHost.fold_edges.
Print Assumptions FoldHost.fold_units_8.
Print Assumptions FoldHost.fold_edges_8.
Print Assumptions StoredCount.stored_records.
Print Assumptions StoredCount.alpha_bounds.
Print Assumptions StoredCount.width_least.
Print Assumptions StoredCount.generation_bounds.
Print Assumptions PhysLev.phys_dmax.
Print Assumptions PhysLev.phys_lev_depth.
Print Assumptions PhysLev.phys_lev_rows.
Print Assumptions PhysLev.phys_edges.
Print Assumptions PhysLev.phys_lev_rows_15.
Print Assumptions PhysLev.phys_lev_rows_S.
Print Assumptions Lower.read_needs_two_levels.
Print Assumptions Lower.onehot_needs_two_levels.
Print Assumptions Lower.branch_not_ternary.
Print Assumptions Lower.branch_unit.
Print Assumptions Margin.margin.
Print Assumptions Margin.margin_tight.
Print Assumptions Margin.mismatch_all.
Print Assumptions Margin.mismatch_run.
Print Assumptions Margin.amap_rep.
Print Assumptions Margin.amp_wrong.
Print Assumptions Margin.amp_margin.
Print Assumptions Margin.flip_ok.
Print Assumptions Erfc.gauss_square.
Print Assumptions Erfc.erfc_le_exp.
Print Assumptions Erfc.erfc_upper1.
Print Assumptions Erfc.erfc_upper3.
Print Assumptions Erfc.erfc_lower1.
Print Assumptions Choose.binom_bound.
Print Assumptions Noise.union_bound.
Print Assumptions Noise.union_gauss.
Print Assumptions Noise.profile_step.
Print Assumptions Noise.profile_le.
Print Assumptions Noise.copy_bound.
Print Assumptions Noise.union_profile.
Print Assumptions Noise.amp_union.
Print Assumptions Noise.amp_gauss.
Print Assumptions Noise.amp_profile.
Print Assumptions Noise.amp_choose.
Print Assumptions Noise.amp_choose_exp.
Print Assumptions Noise.synapse_bound.
Print Assumptions Noise.flip_bound.
Print Assumptions Noise.flip_choose.
Print Assumptions NoiseNum.p_005.
Print Assumptions NoiseNum.TMp_005.
Print Assumptions NoiseNum.TMp_010.
Print Assumptions NoiseNum.flip_threshold.
Print Assumptions NoiseNum.synapse_005.
Print Assumptions NoiseNum.synapse_010.
Print Assumptions NoiseNum.N3_first_order.
Print Assumptions NoiseNum.generation_1.
Print Assumptions NoiseNum.generation_3.
Print Assumptions NoiseNum.generation_5.
Print Assumptions Restore.tw_paper.
Print Assumptions Restore.far_core.
Print Assumptions Restore.wrong_far.
Print Assumptions Restore.claims.
Print Assumptions Restore.claim_stop.
Print Assumptions Restore.restoration.
Print Assumptions FlipLower.P_few.
Print Assumptions FlipLower.flip_fails.
Print Assumptions AmpHost.amp_run.
Print Assumptions AmpHost.amp_selfrep.